Proof complexity

Proof complexity is the study of the computational resources required to certify that a propositional formula is a tautology, or equivalently that a propositional formula has no satisfying assignment. It treats proofs as finite combinatorial objects whose length, depth, width, and algebraic degree can be measured. The field connects computational complexity theory with mathematical logic, Boolean circuit complexity, and the analysis of Boolean satisfiability.

The principal structural question asks whether every tautology possesses a proof of polynomial length in a fixed proof system. For sufficiently general systems, an affirmative answer is equivalent to the equality ( \mathsf{NP}=\mathsf{coNP} ). Because that equality remains unresolved, research concentrates on lower bounds for restricted systems, simulations between systems, and relationships between proof search and algorithmic computation.

Abstract proof systems

The standard semantic definition was introduced by Stephen Cook and Robert Reckhow in 1979. A Cook–Reckhow propositional proof system is a polynomial-time computable surjective function

[ P:{0,1}^{*}\longrightarrow \mathrm{TAUT}, ]

where (\mathrm{TAUT}) denotes the set of encoded propositional tautologies. A string (\pi) satisfying (P(\pi)=\varphi) is a (P)-proof of (\varphi). Polynomial-time computability expresses efficient verification, while surjectivity expresses completeness by requiring every tautology to have at least one proof.

A proof system is polynomially bounded when every tautology (\varphi) has a proof whose length is bounded by a polynomial in (|\varphi|). A polynomially bounded Cook–Reckhow system exists exactly when

[ \mathsf{NP}=\mathsf{coNP}. ]

The equivalence follows because proofs provide nondeterministically verifiable certificates for membership in (\mathrm{TAUT}), which is complete for (\mathsf{coNP}). Conversely, if (\mathrm{TAUT}) belongs to (\mathsf{NP}), its polynomially bounded certificates can be organized into a Cook–Reckhow proof system.

Proof systems are compared using polynomial simulation. A system (P) polynomially simulates a system (Q) when every (Q)-proof can be transformed in polynomial time into a (P)-proof of the same tautology, with at most polynomial growth in length. Two systems are polynomially equivalent when each polynomially simulates the other. This relation suppresses inessential differences in notation while retaining distinctions that affect asymptotic proof size.

In 1988, You Watanabe established a comparison theorem for finitely presented Frege systems based on different functionally complete sets of Boolean connectives. The theorem showed that these systems polynomially simulate one another under standard tree encodings of formulas, thereby formalizing the invariance of Frege proof length under changes of propositional vocabulary. The result does not extend automatically to changes that introduce shared subformulas or extension variables, because those devices alter the representation of intermediate formulas rather than merely replacing one finite connective basis with another.

Resolution and combinatorial lower bounds

Resolution is a refutation system for formulas represented in conjunctive normal form. From clauses (C\lor x) and (D\lor\neg x), the resolution rule derives the clause (C\lor D). A refutation begins with the clauses of an unsatisfiable formula and ends with the empty clause, which represents contradiction.

The size of a resolution refutation is commonly measured by its number of derived clauses. Its width is the maximum number of literals occurring in any clause of the refutation. Restrictions on the reuse and ordering of clauses define variants such as tree-like resolution and regular resolution, but unrestricted dag-like resolution is the conventional reference system.

Armin Haken proved an exponential resolution lower bound for the pigeonhole principle in 1985. The associated formulas state that (n+1) pigeons can be injected into (n) holes while encoding the conditions propositionally. They are unsatisfiable, yet every resolution refutation requires exponentially many clauses.

A general connection between width and size was later developed by Eli Ben-Sasson and Avi Wigderson. Their size–width relation implies that a formula requiring substantially wider clauses than its initial clauses also requires a large resolution refutation. This method yields exponential lower bounds for several families of formulas, including suitable random conjunctive formulas and formulas derived from combinatorial expansion.

Resolution lower bounds have an algorithmic interpretation because many conflict-driven clause learning procedures construct clauses corresponding to resolution inferences. The precise simulation depends on the restart policy, clause retention policy, and permitted branching behavior. Consequently, a resolution lower bound measures limitations of an abstract refutation language rather than the running time of every implementation associated with clause learning.

Frege and extended Frege systems

A Frege system formalizes ordinary propositional reasoning through a finite collection of axiom schemes and inference rules. Standard Hilbert calculi, sequent formulations, and natural-deduction formulations become polynomially equivalent after their encodings and proof representations are fixed in compatible ways. Frege systems are substantially stronger than resolution because intermediate proof lines may contain arbitrary propositional formulas rather than clauses alone.

No superpolynomial lower bound is known for unrestricted Frege systems. Existing techniques can establish lower bounds only after additional syntactic restrictions are imposed. In bounded-depth Frege systems, proof lines are represented by circuits of bounded logical depth, usually with unbounded fan-in conjunction and disjunction gates. Lower bounds for these systems were developed through work by Miklós Ajtai, Jan Krajíček, Pavel Pudlák, and Alexander Razborov, using restrictions and circuit-complexity arguments adapted to proof lines.

Extended Frege augments Frege reasoning with extension variables that abbreviate previously constructed formulas. An extension axiom has the form

[ e \leftrightarrow \theta, ]

where the new variable (e) names the formula (\theta). Repeated abbreviations permit proofs to represent Boolean circuits without expanding them into trees, which can prevent exponential duplication of shared subexpressions. Extended Frege polynomially simulates many familiar propositional proof systems, but no superpolynomial lower bound is known for it.

The distinction between Frege and extended Frege illustrates the role of representation in proof complexity. Replacing a fixed Boolean connective by an equivalent constant-size formula produces only polynomial overhead, as in Watanabe’s comparison theorem. Naming a repeatedly used formula with an extension variable can instead convert a tree representation into a directed acyclic graph, changing the amount of syntactic sharing available throughout the proof.

Algebraic proof systems

Algebraic proof systems translate Boolean formulas into polynomial equations over a field. A Boolean variable (x) is constrained by the equation

[ x^{2}-x=0, ]

which restricts its values to (0) and (1). Clauses are represented by polynomials that vanish exactly when the corresponding clause is satisfied under a Boolean assignment.

In the polynomial calculus, new polynomials are derived by taking linear combinations and by multiplying an existing polynomial by a variable. A refutation derives the constant polynomial (1), demonstrating that the original equations have no common Boolean solution. The principal measures are the number of monomials, the total written size, and the maximum degree reached during the derivation.

Degree plays a role analogous to width in resolution. Degree lower bounds often imply size lower bounds because a short derivation can be transformed into one of controlled degree under appropriate conditions. Polynomial calculus also exhibits dependence on the underlying field, since algebraic identities and coefficient cancellation can vary with the field characteristic.

The Nullstellensatz proof system represents a refutation as a single algebraic identity certifying that the encoded equations have no common root. Sum-of-squares proofs extend the algebraic viewpoint to polynomial inequalities and semialgebraic reasoning. Their proof-complexity measures correspond to levels of convex optimization hierarchies used in combinatorial optimization.

Interpolation and circuit lower bounds

Feasible interpolation converts short proofs into small circuits under a suitable separation structure. Consider an unsatisfiable formula of the form

[ A(x,y)\land B(x,z), ]

where the variables (y) occur only in (A), the variables (z) occur only in (B), and the variables (x) are shared. An interpolant is a Boolean function of (x) that separates assignments extendable to models of (A) from assignments extendable to models of (B).

When a proof system has feasible interpolation, a short refutation yields a small circuit computing such a separator. A circuit lower bound for the separator then implies a proof-size lower bound for the original refutation. Monotone feasible interpolation imposes an additional monotonicity condition and connects proof lower bounds with monotone circuit complexity.

This framework accounts for several lower bounds in resolution, cutting-plane systems under specified restrictions, and bounded-depth systems. It does not directly yield unrestricted Frege or extended Frege lower bounds because the corresponding interpolation circuits are not known to satisfy a circuit restriction for which adequate lower bounds are available.

Proof search and automatizability

Proof length and proof search are distinct complexity measures. A formula can possess a short proof even when locating such a proof is computationally difficult. A proof system is automatizable when an algorithm, given a tautology or unsatisfiable formula, finds a proof in time polynomial in the input length and the length of the shortest proof in that system. Quasipolynomial automatizability replaces this polynomial bound with a quasipolynomial one.

Automatizability connects proof complexity with parameterized complexity, learning algorithms, and satisfiability solving. Conditional non-automatizability results show that efficient search for near-shortest proofs in several systems would produce algorithms for problems regarded as computationally intractable under standard complexity assumptions. These results concern the relation between optimal proof length and search time rather than the correctness or completeness of the systems.

Proof search can also be formulated as a total search problem associated with a bounded consistency or reflection principle. This formulation links propositional proof systems with classes in total function complexity, where the existence of a solution follows from a combinatorial or logical principle even though the solution may be difficult to compute.

Bounded arithmetic and reflection

Proof complexity has a translation into bounded arithmetic, whose theories formalize reasoning about polynomial-time and related computational classes. Propositional translations of bounded-arithmetic statements produce families of tautologies, while proofs in an arithmetic theory can yield uniformly generated propositional proofs.

A reflection principle for a proof system asserts that every formula proved by the system is true. Finite propositional forms of reflection express the soundness of proofs up to a bounded length. The ability of one system to prove reflection principles for another is closely related to polynomial simulation between the corresponding systems.

This relationship shifts attention from individual hard tautologies to the capacity of a theory to formalize soundness arguments. Strong lower bounds for major proof systems would therefore imply limitations on formalized reasoning in associated arithmetic theories, rather than merely demonstrating inefficient derivations for isolated formulas.