SAT — Boolean satisfiability (the famous decidable-but-hard one)

Parent: logic

SAT

Given a propositional formula over Boolean variables (built from ∧, ∨, ¬; usually CNF = a conjunction of clauses), is there an assignment making it true?

Unlike FOL validity, SAT is decidable — finitely many assignments — but it's the canonical hard problem.

Cook–Levin: the first NP-complete problem

Cook–Levin (1971)

SAT is NP-complete — it's in NP, and every problem in NP reduces to it in polynomial time. (3-SAT already is.)

So SAT is where P vs NP lives: a polynomial SAT algorithm would collapse NP to P. It's the hub through which thousands of problems are proven NP-hard (by reduction from SAT).

The ∀∃ ladder — SAT → QBF → FOL

• SAT (propositional, no quantifiers): NP-complete (decidable).
• QBF (quantified Boolean formulas — ∀/∃ over booleans): PSPACE-complete (still decidable, harder).
• FOL validity (quantifiers over an infinite domain): undecidable. The quantifier over an infinite domain is exactly what tips logic from "hard but decidable" to "undecidable."

The solvers are the engine we reused

Practical SAT is run by DPLL → CDCL (conflict-driven clause learning); SMT = SAT modulo theories (DPLL(T)) adds arithmetic/arrays. The recursive-harness lifts exactly this machinery to agents:

• csp-formalization — the harness as a dynamic CSP (collapse = propagation);
• conflict-learning-and-backjumping — CDCL no-good learning + non-chronological backjump;
• llm-as-fallible-theory-solver — DPLL(T) with the LLM as a (fallible) theory solver.

That's where "we already used SAT."