Complexity, SAT, and SMT

A decision procedure eventually answers every input in its stated domain. That guarantee says nothing by itself about whether the answer arrives within a practical amount of time.

Complexity theory studies this distinction by measuring resources as a function of input size. SAT and SMT show how worst-case difficulty can coexist with powerful practical methods.

From computability to resource bounds

Work by Hartmanis and Stearns, Cobham, Edmonds, and others in the 1960s helped establish systematic approaches to computational complexity and feasible computation.

The class P contains decision problems solvable in deterministic polynomial time. NP contains problems whose positive instances have polynomial-size certificates verifiable in polynomial time, under the standard equivalent machine formulations.

For propositional satisfiability, a certificate is a truth assignment. Given an assignment, evaluating the formula takes polynomial time in its written size.

Finding such an assignment can require a much larger search. The definition of NP does not supply an efficient deterministic method for finding a certificate.

Stephen Cook's 1971 paper proved a foundational completeness result for propositional reasoning. Leonid Levin's independent work, published in 1973, developed universal search problems in a related framework. Richard Karp's 1972 reductions showed how many important combinatorial problems fit the resulting theory.

The publication dates and formulations should be distinguished. The standard modern statement that SAT is NP-complete summarizes this development; it does not imply a single joint 1971 publication.

What NP-completeness establishes

A polynomial reduction translates instances of one problem into instances of another, preserving the answer with only polynomial growth and computational overhead.

SAT's NP-completeness says that every problem in NP has such a reduction to SAT, and SAT itself belongs to NP.

If SAT has a polynomial-time algorithm, then P equals NP. Whether P equals NP remains open. NP-completeness is proved; the conjecture that no polynomial-time SAT algorithm exists is not.

Nor does the open question imply that every imaginable complexity lower bound remains unknown. Many lower bounds are proved for specified models, proof systems, and complexity classes.

Worst-case complexity also does not predict the difficulty of every instance. A large formula with exploitable structure may be easier than a smaller adversarial one.

Proof size and certificates

A satisfying assignment certifies SAT. An unsatisfiability claim needs different evidence.

A resolution refutation can serve as an UNSAT certificate. Each local inference is readily checked, but some formula families require very long refutations in a particular proof system.

Cook and Reckhow's 1979 framework studies propositional proof systems and polynomially bounded proofs. It clarifies a common confusion: efficient checking of each supplied proof does not guarantee that every true statement has a short proof in the system.

Proof complexity therefore connects the size of formal derivations with computational complexity. The choice of proof system matters, just as the choice of representation matters in automated deduction.

From DP to DPLL

The Davis–Putnam procedure of 1960 used clause operations including variable elimination. The 1962 work of Martin Davis, George Logemann, and Donald Loveland developed the branching approach now called DPLL.

Unit propagation forces the remaining literal of a clause when all its other literals are false. If propagation cannot decide the problem, the solver chooses a literal and explores a branch.

A contradiction closes a branch. Backtracking explores alternatives.

This is a complete method for finite propositional formulas when implemented with exhaustive search. Its challenge is the size of the search tree.

A conflict and a learned clause

Consider three clauses:

There are no initial unit clauses. Decide $a$ to be true.

Then $C_1$ forces $b$ true, and $C_2$ forces $c$ true. Clause $C_3$ becomes false. The branch conflicts.

Resolve $C_3$ with $C_1$ on $b$:

Resolve this clause with $C_2$ on $c$:

The learned clause records why the branch failed. It is a consequence of the original clauses, so retaining it preserves the solution set.

After backtracking, the learned unit clause forces $a$ false. Choosing $b$ and $c$ false now satisfies all three original clauses.

The example is intentionally small. In larger instances, conflict analysis can identify a clause involving only some recent decisions and permit nonchronological backtracking, often called backjumping.

The following lab makes these dependencies visible one step at a time. The second preset introduces an earlier decision that the learned clause does not depend on, so a backjump can skip a decision level.

Conflict-driven search as an engineering achievement

João Marques-Silva and Karem Sakallah's GRASP work and Roberto Bayardo and Robert Schrag's work in the 1990s were important contributions to modern conflict-driven solving.

Chaff, described by Moskewicz and collaborators in 2001, demonstrated major gains from carefully engineered propagation, decision heuristics, and data structures.

The GRASP report and Chaff paper make the point concrete: strong solvers depend on managing the cost of repeated operations, not merely adopting one logically powerful rule.

Modern CDCL solvers combine propagation, learning, backjumping, restarts, and clause management. These mechanisms help discover useful structure without eliminating worst-case difficulty.

An UNSAT claim can be accompanied by a checkable certificate in a specified format. Certificate generation and verification are distinct engineering tasks; a solver's unsupported answer and an independently checked derivation provide different evidence.

Beyond propositional atoms

Boolean reasoning treats atoms as independently assignable truth values. Mathematical atoms often constrain one another.

Consider

over the real numbers. The conjunction is inconsistent, although a Boolean abstraction could initially assign all three atoms true.

An arithmetic procedure recognizes that $y\ge x>2$ contradicts $y<1$. It can return a theory conflict corresponding to the clause saying that these three conditions cannot all hold together.

Satisfiability modulo theories, SMT, combines Boolean structure with such background reasoning. The theory may involve arithmetic, arrays, bit-vectors, uninterpreted functions, or other precisely defined objects.

To see what the background theory contributes, begin with the inconsistent real inequalities. Then change a bound, compare integers with reals, or encode a small scheduling problem.

These experiments also show why a solver’s answer must be read together with the declared domain. The next question is which domains admit decision procedures and where their guarantees end.

Decidable theories have boundaries

Presburger's 1929 result establishes decidability for first-order arithmetic with addition in the relevant language. It does not include unrestricted multiplication of variables.

Tarski's work establishes decidability for real closed fields, with effective methods for polynomial equalities and inequalities. It does not decide every statement about arbitrary real functions or transcendental operations.

These boundaries explain why two formulas that both look like arithmetic may belong to very different computational problems.

Even inside a decidable theory, quantifiers and representations can make decision procedures expensive. Practical SMT systems therefore distinguish fragments and may return an inconclusive result outside the guarantees of a selected procedure.

Cooperation between decision procedures

Greg Nelson and Derek Oppen's 1979 work gave a principled method for combining decision procedures through shared equality information.

The standard combination setting includes disjoint nonlogical signatures and stable infiniteness, with additional distinctions governing whether equality exchange requires case splits. Stable infiniteness means that a satisfiable quantifier-free constraint has a model with an infinite domain in the relevant sorts.

These assumptions cannot simply be dropped. Fixed-width bit-vectors, for example, have finite domains and require appropriate alternative treatment.

Later DPLL(T) architectures organize the interaction between a Boolean engine and one or more theory solvers. Theory propagation and conflict explanations allow information to flow back into the Boolean search.

The result is a framework for cooperation, not a universal decision procedure for all combined mathematics.

Leonardo de Moura and Nikolaj Bjørner's 2008 paper introducing Z3 presented an SMT solver for combinations of theories including arithmetic, bit-vectors, arrays, and uninterpreted functions, with applications to software verification and analysis. The lab above uses Z3 to make this distinction practical: the Boolean structure, declared sorts, and theory operations all contribute to the problem being solved.

From solving to programming

SAT and SMT expose logical constraints and search for satisfying interpretations or contradictions. Another tradition uses logical clauses as programs whose proofs compute answers.

Sources and further reading

• Stephen A. Cook, “The Complexity of Theorem-Proving Procedures” (1971); Richard M. Karp, “Reducibility among Combinatorial Problems” (1972).
• Leonid A. Levin, “Universal Sequential Search Problems” (1973).
• Stephen A. Cook and Robert A. Reckhow, “The Relative Efficiency of Propositional Proof Systems” (1979).
• Martin Davis, George Logemann, and Donald Loveland, “A Machine Program for Theorem-Proving” (1962).
• João P. Marques-Silva and Karem A. Sakallah, GRASP technical report (1996); Roberto J. Bayardo Jr. and Robert Schrag, “Using CSP Look-Back Techniques to Solve Real-World SAT Instances” (1997).
• Matthew W. Moskewicz and collaborators, “Chaff: Engineering an Efficient SAT Solver” (2001).
• Greg Nelson and Derek C. Oppen, “Simplification by Cooperating Decision Procedures” (1979).
• Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli, “Solving SAT and SAT Modulo Theories: From an Abstract Davis–Putnam–Logemann–Loveland Procedure to DPLL(T)” (2006).
• Leonardo de Moura and Nikolaj Bjørner, “Z3: An Efficient SMT Solver” (2008).