{{Short description|Field in logic and theoretical computer science}} In logic and theoretical computer science, and specifically proof theory and computational complexity theory, '''proof complexity''' is the field aiming to understand and analyse the computational resources that are required to prove or refute statements. Research in proof complexity is predominantly concerned with proving proof-length lower and upper bounds in various propositional proof systems. For example, among the major challenges of proof complexity is showing that the Frege system, the usual propositional calculus, does not admit polynomial-size proofs of all tautologies. Here the size of the proof is simply the number of symbols in it, and a proof is said to be of polynomial size if it is polynomial in the size of the tautology it proves.
Systematic study of proof complexity began with the work of Stephen Cook and Robert Reckhow (1979), who provided the basic definition of a propositional proof system from the perspective of computational complexity. Specifically, Cook and Reckhow observed that proving proof size lower bounds on stronger and stronger propositional proof systems can be viewed as a step towards separating NP from co-NP (and thus P from NP), since the existence of a propositional proof system that admits polynomial size proofs for all tautologies is equivalent to NP = co-NP.
Contemporary proof complexity research draws ideas and methods from many areas in computational complexity, algorithms and mathematics. Since many important algorithms and algorithmic techniques can be cast as proof search algorithms for certain proof systems, proving lower bounds on proof sizes in these systems implies run-time lower bounds on the corresponding algorithms. This connects proof complexity to more applied areas such as SAT solving.
Mathematical logic can also serve as a framework to study propositional proof sizes. First-order theories and, in particular, weak fragments of Peano arithmetic, which come under the name of bounded arithmetic, serve as uniform versions of propositional proof systems and provide further background for interpreting short propositional proofs in terms of various levels of feasible reasoning.
== Main concepts ==
=== Conventions === By default, proof theory discussed proof systems for classical propositional logic, using the '''language''' of propositional logic with the connectives <math>\and, \or, \neg, \to</math>, and countably many propositional variables <math>\{p_{i} : i \in 2^*\}</math>. Here, <math>2^*</math> is the set of finite binary strings.
A '''proof system''' is denoted with capital letters: <math>P, Q, R, \dots</math>. A '''proof''' is denoted with lowercase letters <math>x, y, z, \dots</math>.
A '''formula''' is denoted with lower Greek letters: <math>\phi, \psi, \sigma, \dots</math>. The '''length''' of a formula <math>\phi</math> is <math>|\phi|</math>. TAUT a formal language, consisting of the tautological formulas of propositional logic. Similarly, the length of a proof <math>x</math> is <math>|x|</math>.
Big-O and big-Omega notation are used in the same way as in computational complexity theory.
===Proof systems=== {{Main|Propositional proof system}} A proof system is an algorithm <math>P</math> that takes two inputs: a formula <math>\phi</math>, and a purported proof <math>x</math>. The proof system must satisfy:
* <math>P(\phi, x)</math> runs in time <math>\mathsf{poly}(|\phi|, |x|)</math>. * <math>\phi \in \mathsf{TAUT}</math> if and only if there exists some <math>x</math>, such that <math>P(\phi, x)</math> accepts.
Examples of propositional proof systems include sequent calculus, resolution, cutting planes and Frege systems. Strong mathematical theories such as ZFC induce propositional proof systems as well: a proof of a tautology <math>\tau</math> in a propositional interpretation of ZFC is a ZFC-proof of a formalized statement '<math>\tau</math> is a tautology'.
A proof system can be thought of as a nondeterministic polynomial-time algorithm for proving non-satisfiability. That is, given a formula <math>\phi</math>, <math>\phi</math> is unsatisfiable if and only if there exists some <math>x</math>, such that <math>P(\neg\phi, x)</math> accepts. This shows its close relationship with the co-NP class.
=== Complexity === Ordinary proof theory does not care about what formulas a certain proof system ''can and cannot'' prove. Proof complexity is not satisfied with what ''can'' be done, but ''how efficiently'' it can be done, i.e. the computational complexity of the proof system. In order to measure efficiency, what efficiency is for a proof system must be defined.
In ordinary complexity theory, efficiency can be measured by how many steps are required (time complexity), how much working space is required (space complexity), size of a Boolean circuit needed to implement a boolean function (circuit complexity), etc. In proof complexity theory, there are also more than one way to measure of efficiency.
The '''size complexity''' of a proof system denotes the minimal size of proofs possible in the system for a given tautology. In detail, a proof system has (upper bound) size complexity <math>O(F(n))</math> iff given any tautology <math>\phi</math> of length <math>n</math>, there is a proof of <math>\phi</math> in this proof system that uses <math>\lesssim F(n)</math> steps. It has (lower bound) size complexity <math>\Omega(F(n))</math> iff given any length <math>n</math>, there exists a tautology <math>\phi</math> of length <math>n</math>, such that any proof of <math>\phi</math> in the proof system needs <math>\gtrsim F(n)</math> steps.
The '''space complexity''' of a proof system denotes the memory usage during a proof. A common way to measure "memory usage" is '''clause complexity''': the maximum number of clauses that can appear simultaneously during a resolution proof. Other ways to measure space complexity include:
* The number of symbols of a proof. * The number of lines of a proof. * The maximal complexity of formulas that appears in a proof. The complexity of a formula may be its length, or its number of variables, or its number of quantifiers, etc. * The depth of a proof-tree (in the case of natural deduction or sequent calculus). * The memory complexity of a proof. One can imagine a proof system as having a memory bank, such that at any point in the proof, only formulas in the bank, or axioms, may be used. A formula may be removed from the memory bank, but if that formula needs to be used again, it must be re-proven. Then, the memory complexity of the proof is the minimal number of memory locations necessary for the proof to go through.
The '''search complexity''' of a proof system denotes the computational complexity of a prover, that is, an algorithm for finding a proof of a tautology within a proof system. A proof system with a polynomial-time prover is '''automatable'''.
== Proof size complexity ==
=== p-boundedness === A proof system <math>P</math> is polynomially bounded ('''p-bounded''') iff for any <math>\phi</math>, if there exists some <math>x</math> such that <math>P(\phi, x)</math> is true, then there exists some <math>x</math> such that <math>P(\phi, x)</math> is true, and <math>|x| = \mathsf{poly}(|\phi|) </math>. In other words, anything that the system can prove at all, has a polynomially-short proof.
Most nontrivial proof systems are believed to be not p-bounded. To acquire intuition about why this is the case, one consider the following examples.
==== Graph coloring ==== Given a graph <math>G = (V, E)</math>, if there exists a 3-coloring, then this can be proven by simply giving the coloring. Thus, the proof of 3-colorability has length <math>|V|</math>. It can be checked in polynomial time. In contrast, if there does ''not'' exist a 3-coloring, then there is no obvious way to prove it succinctly. The naive way to prove it is to explicitly enumerate all <math>3^{|V|}</math> possible 3-colorings, and showing that in each case, there are two vertices of the same color sharing an edge. However, such a proof is exponentially large compared to the input size.
The Hajós construction is a sound and complete proof system for graph non-3-colorability: A graph is non-3-colorable if and only if it has a Hajós 4-construction. However, such a construction may require superpolynomially steps.
==== Polynomial ==== Given a system of polynomials <math>f_1(x_{1}, \dots, x_n), \dots, f_m(x_{1}, \dots, x_n) </math> in a finite field <math>\mathbb F </math>, if there exists a root, then this can be proven by simply giving the values for the variables <math>x_1, \dots, x_n </math>. The proof size is linear in input size. It can be checked in polynomial time.
However, if there is no root, then there is no obvious way to prove it succinctly. The naive way to prove it is to explicitly enumerate all <math>|\mathbb F|^{n}</math> possible values. By Hilbert's Nullstellensatz, there is a sound and complete proof system for non-solvability: There exists some polynomials <math>g_1, \dots, g_m</math> such that <math>\sum_{i=1}^m g_i f_i = 1</math>, if and only if the polynomial system is non-solvable. However, the polynomials <math>g_1, \dots, g_m</math> may contain superpolynomially many terms.
==== Tautology ==== Given a formula <math>\phi</math> in classical propositional logic with propositional variables <math>p_1, \dots, p_n</math>, if it is not a tautology, then this can be proven by simply giving the truth-values for the propositional variables <math>p_1, \dots, p_n</math>, such that <math>\phi</math> evaluates to False. The proof size is linear in input size. However, if it is a tautology, then there is no obvious way to prove it succinctly. The naive way to prove it is to explicitly enumerate the truth table, which has <math>2^n</math> rows.
There are many sound and complete proof systems for proving tautologies of classical propositional logic, but there is no guarantee that any system can prove all tautologies with proof size <math>\mathsf{poly}(|\phi|)</math>.
=== Main results === {{unsolved|computer science|Does there exist a p-bounded proof system for classical propositional tautologies?}} Because <math>\phi</math> is not a tautology if and only if <math>\neg \phi</math> is satisfiable, <math>\mathsf{TAUT}</math> is co-NP-complete. Thus, if there exists a proof system for <math>\mathsf{TAUT}</math> that is p-bounded, then NP = co-NP. Conversely, if NP = co-NP, then <math>\mathsf{TAUT}</math>, being co-NP, would also be NP, and thus there is a p-bounded proof system for proving tautologies. This was first proven by Cook and Reckhow (1979).<ref name="cr2">{{cite journal|first1=Stephen|last1=Cook|author-link1=Stephen Cook|first2=Robert A.|last2=Reckhow|title=The Relative Efficiency of Propositional Proof Systems|journal=Journal of Symbolic Logic|volume=44|number=1|year=1979|pages=36–50|doi=10.2307/2273702|jstor=2273702|s2cid=2187041}}</ref> This results in an equivalent formulation of the NP = coNP problem:<blockquote>Does there exist a p-bounded proof system for classical propositional tautologies?</blockquote>
== Proof system strength == Proof complexity compares the strength of proof systems using the notion of ''efficient simulation''. Efficiency is the operative concept here, since proof complexity theory studies not merely whether something can be proven, but in the efficiency of the proof.
=== Definitions === Given two proof systems <math>P, Q</math>, <math>P</math> '''simulates''' <math>Q</math>, written as <math>P \leq Q</math>, if and only if there is an algorithm that:
* given as input, a ''Q''-proof of a tautology, outputs a ''P''-proof of the same tautology, * and the size of the ''P''-proof is polynomial in the size of the ''Q''-proof.
We say that <math>P</math> '''p-simulates''' <math>Q</math>, written as <math>P \leq_p Q</math> if and only if there is an algorithm that:
* given as input, a ''Q''-proof of a tautology, outputs a ''P''-proof of the same tautology, * and runs in polynomial time polynomial in the size of the ''Q''-proof.
Since a polynomial-time algorithm can only produce a polynomial-size output, p-simulation implies simulation. The converse may not hold, i.e. two proof systems <math>P, Q</math> may exist such that <math>P</math> simulates <math>Q</math>, but <math>P</math> does not p-simulate <math>Q</math>.
Both simulation and p-simulation relations are reflexive and transitive, thus they are preorders, and induces equivalence relations. If <math>P, Q</math> (p-)simulate each other, then they are '''(p-)equivalent'''. A proof system is '''(p-)optimal''' if it (p-)simulates all other proof systems.
=== Results === Any nonempty set in NP has an optimal proof system. No set outside of NP is known to have an optimal proof system. Any coNE-hard sets and even all coNQP-hard sets is known to have no optimal proof systems.<ref>{{Citation |last=Dose |first=Titus |title=NP-Completeness, Proof Systems, and Disjoint NP-Pairs |date=2019-04-02 |url=https://eccc.weizmann.ac.il/report/2019/050/ |publisher=Electronic Colloquium on Computational Complexity |language=en |id=TR19-050 |last2=Glaßer |first2=Christian}}</ref>
Sequent calculus is p-equivalent to (every) Frege system.<ref name="Rec2">{{cite thesis|first1=Robert A.|last1=Reckhow|title=On the lengths of proofs in the propositional calculus|type=PhD Thesis|publisher=University of Toronto|year=1976}}</ref>
Every propositional proof system ''P'' can be simulated by Extended Frege extended with axioms postulating soundness of ''P''.<ref name="Kpc2">{{cite book|first1=Jan|last1=Krajíček|title=Proof complexity|publisher=Cambridge University Press|year=2019}}</ref> {{unsolved|computer science|Does there exist a p-optimal or optimal propositional proof system?}} An optimal or p-optimal propositional proof system would be ideal in a sense, since it would produce the shortest (up to a polynomial factor) possible proofs for all tautologies. Unfortunately, this question is open.
It is known that:<ref name="KP12">{{cite journal|first1=Jan|last1=Krajíček|first2=Pavel|last2=Pudlák|author-link2=Pavel Pudlak|title=Propositional proof systems, the consistency of first-order theories and the complexity of computations|journal=Journal of Symbolic Logic|volume=54|number=3|year=1989|pages=1063–1079|doi=10.2307/2274765|jstor=2274765|s2cid=15093234}}</ref>
* If E = NE, then there exists of an optimal proof system. * If NE = co-NE, then there exists of an optimal proof system.
It has been proven that many weak proof systems cannot simulate certain stronger systems (see below). However, the question remains open if the notion of simulation is relaxed. For example, it is open whether Resolution ''effectively polynomially simulates'' Extended Frege.<ref name="PS2">{{cite journal|first1=Toniann|last1=Pitassi|author-link1=Toniann Pitassi|first2=Rahul|last2=Santhanam|author-link2=Rahul Santhanam|title=Effectively polynomial simulations|url=https://www.cs.toronto.edu/~toni/Papers/effsimulation.pdf|journal=ICS|year=2010|pages=370–382}}</ref>
== Automatability == The search complexity of proof systems asks:<ref name="BPR2">{{cite journal|first1=M.L.|last1=Bonet|author-link1=M.L. Bonet|first2=Toniann|last2=Pitassi|author-link2=Toniann Pitassi|first3=Ran|last3=Raz|author-link3=Ran Raz|title=On Interpolation and Automatization for Frege Proof System|journal=SIAM Journal on Computing|volume=29|number=6|year=2000|pages=1939–1967|doi=10.1137/S0097539798353230}}</ref><blockquote>Given a proof system, is there an efficient prover of tautologies in this system?</blockquote>A proof system ''<math>P</math>'' is '''automatable''' if there is an algorithm <math>T</math>, called the '''prover''', such that:
* If <math>\tau</math> is a tautology, then <math>P(\tau, T(\tau))</math> is true. That is, the algorithm outputs a ''P''-proof of <math>\tau</math>. Note that there is no requirement for what the algorithm should do when <math>\tau</math> is not a tautology. * <math>T(\tau)</math> is computable in time <math>\mathsf{poly}(|\tau|, |x|)</math>, where <math>x</math> is the shortest ''P''-proof of <math>\tau</math>.
The second requirement incorporates the proviso of "the shortest ''P''-proof of <math>\tau</math>", so that even if P is not polynomially bounded, it can still be automatable. That is, there may be tautologies such that the proof system ''P'' is forced to prove with proofs that are growing super-polynomially. Nevertheless, the prover does the best it could out of a bad situation.
More generally, a proof system <math>P</math> is '''weakly automatable''' if there is another proof system ''<math>R</math>'', and a prover <math>T</math>, such that:
* If <math>\tau</math> is a tautology, then <math>R(\tau, T(\tau))</math> is true. That is, the algorithm outputs an ''R''-proof of <math>\tau</math>. * <math>T(\tau)</math> is computable in time <math>\mathsf{poly}(|\tau|, |x|)</math>, where <math>x</math> is the shortest ''P''-proof of <math>\tau</math>.
=== Results === Many proof systems of interest are believed to be non-automatable. However, currently only conditional negative results are known.
* Krajíček and Pudlák (1998) proved that Extended Frege is not weakly automatable unless RSA is not secure against P/poly.<ref name="KP2">{{cite journal|first1=Jan|last1=Krajíček|first2=Pavel|last2=Pudlák|author-link2=Pavel Pudlak|title=Some consequences of cryptographical conjectures for <math>S^1_2</math> and EF|journal=Information and Computation|volume=140|number=1|year=1998|pages=82–94|doi=10.1006/inco.1997.2674|doi-access=free}}</ref> * Bonet, Pitassi and Raz (2000) proved that the <math>TC^0</math>-Frege system is not weakly automatable unless the Diffie–Hellman scheme is not secure against P/poly.<ref name="BPRc2">{{cite journal|first1=M.L.|last1=Bonet|author-link1=María Luisa Bonet|first2=Toniann|last2=Pitassi|author-link2=Toniann Pitassi|first3=Ran|last3=Raz|author-link3=Ran Raz|title=On Interpolation and Automatization for Frege Proof System|journal=SIAM Journal on Computing|volume=29|number=6|year=2000|pages=1939–1967|doi=10.1137/S0097539798353230}}</ref> This was extended by Bonet, Domingo, Gavaldá, Maciel and Pitassi (2004) who proved that constant-depth Frege systems of depth at least 2 are not weakly automatable unless the Diffie–Hellman scheme is not secure against nonuniform adversaries working in subexponential time.<ref name="BDGMP2">{{cite journal|first1=M.L.|last1=Bonet|author-link1=M.L. Bonet|first2=C.|last2=Domingo|first3=R.|last3=Gavaldá|first4=A.|last4=Maciel|first5=Toniann|last5=Pitassi|s2cid=1360759|author-link5=Toniann Pitassi|title=Non-automatizability of Bounded-depth Frege Proofs|journal=Computational Complexity|volume=13|year=2004|issue=1–2|pages=47–68|doi=10.1007/s00037-004-0183-5}}</ref> * Alekhnovich and Razborov (2008) proved that tree-like Resolution and Resolution are not automatable unless [[Parameterized complexity|FPT=W[P]]].<ref name="AleRaz2">{{cite journal|first1=Michael|last1=Alekhnovich|first2=Alexander|last2=Razborov|title=Resolution is not automatizable unless W[P] is tractable|journal=SIAM Journal on Computing|year=2018|volume=38|issue=4|pages=1347–1363|doi=10.1137/06066850X}}</ref> This was extended by Galesi and Lauria (2010) who proved that Nullstellensatz and Polynomial Calculus are not automatable unless the fixed-parameter hierarchy collapses.<ref name="GaLa2">{{cite journal|first1=Nicola|last1=Galesi|first2=Massimo|last2=Lauria|s2cid=11602606|title=On the automatizability of polynomial calculus|journal=Theory of Computing Systems|year=2010|volume=47|issue=2|pages=491–506|doi=10.1007/s00224-009-9195-5}}</ref> Mertz, Pitassi and Wei (2019) proved that tree-like Resolution and Resolution are not automatable even in certain quasi-polynomial time assuming the exponential time hypothesis.<ref name="MPW2">{{cite journal|first1=Ian|last1=Mertz|first2=Toniann|last2=Pitassi|first3=Yuanhao|last3=Wei|title=Short proofs are hard to find|journal=ICALP|year=2019}}</ref> * Atserias and Müller (2019) proved that Resolution is not automatable unless P=NP.<ref name="AM2">{{cite book|first1=Albert|last1=Atserias|author-link1=Albert Atserias|first2=Moritz|last2=Müller|chapter=Automating resolution is NP-hard|title=Proceedings of the 60th Symposium on Foundations of Computer Science|year=2019|pages=498–509}}</ref> This was extended by de Rezende, Göös, Nordström, Pitassi, Robere and Sokolov (2020) to NP-hardness of automating Nullstellensatz and Polynomial Calculus;<ref name="RGNPRS2">{{cite journal|first1=Susanna|last1=de Rezende|first2=Mika|last2=Göös|first3=Jakob|last3=Nordström|first4=Tonnian|last4=Pitassi|first5=Robert|last5=Robere|first6=Dmitry|last6=Sokolov|title=Automating algebraic proof systems is NP-hard|journal=ECCC|year=2020}}</ref> by Göös, Koroth, Mertz and Pitassi (2020) to NP-hardness of automating Cutting Planes;<ref name="GKMP2">{{cite book|first1=Mika|last1=Göös|first2=Sajin|last2=Koroth|first3=Ian|last3=Mertz|first4=Tonnian|last4=Pitassi|title=Proceedings of the 52nd Annual ACM SIGACT Symposium on Theory of Computing|chapter=Automating cutting planes is NP-hard|s2cid=215814356|year=2020|pages=68–77|doi=10.1145/3357713.3384248|arxiv=2004.08037|isbn=9781450369794}}</ref> and by Garlík (2020) to NP-hardness of automating ''k''-DNF Resolution.<ref name="Gar2">{{cite journal|first1=Michal|last1=Garlík|title=Failure of feasible disjunction property for ''k''-DNF Resolution and NP-hardness of automating it|journal=ECCC|year=2020|arxiv=2003.10230}}</ref>
It is not known if the weak automatability of Resolution would break any standard complexity-theoretic hardness assumptions.
On the positive side,
* Beame and Pitassi (1996) showed that tree-like Resolution is automatable in quasi-polynomial time and Resolution is automatable on formulas of small width in weakly subexponential time.<ref name="BP2">{{cite journal|first1=Paul|last1=Beame|author-link1=Paul Beame|first2=Toniann|last2=Pitassi|author-link2=Toniann Pitassi|title=Simplified and improved resolution lower bounds|journal=37th Annual Symposium on Foundations of Computer Science|year=1996|pages=274–282}}</ref><ref name="BW2">{{cite book|first1=Eli|last1=Ben-Sasson|author-link1=Eli Ben-Sasson|first2=Avi|last2=Wigderson|author-link2=Avi Wigderson|chapter=Short proofs are narrow - resolution made simple|title=Proceedings of the 31st ACM Symposium on Theory of Computing|year=1999|pages=517–526}}</ref>
==Bounded arithmetic== {{Main|Bounded arithmetic}}
Propositional proof systems can be interpreted as nonuniform equivalents of theories of higher order. The equivalence is most often studied in the context of theories of bounded arithmetic. For example, the Extended Frege system corresponds to Cook's theory <math>\mathrm {PV}_1</math> formalizing polynomial-time reasoning and the Frege system corresponds to the theory <math>\mathrm {VNC}^1</math> formalizing <math>\mathsf{NC}^1</math> reasoning.
The correspondence was introduced by Stephen Cook (1975), who showed that coNP theorems, formally <math>\Pi^b_1</math> formulas, of the theory <math>\mathrm {PV}_1</math> translate to sequences of tautologies with polynomial-size proofs in Extended Frege. Moreover, Extended Frege is the weakest such system: if another proof system ''P'' has this property, then ''P'' simulates Extended Frege.<ref name="cook">{{cite book|first1=Stephen|last1=Cook|author-link1=Stephen Cook|chapter=Feasibly constructive proofs and the propositiona calculus|title=Proceedings of the 7th Annual ACM Symposium on Theory of Computing|year=1975|pages=83–97}}</ref>
An alternative translation between second-order statements and propositional formulas given by Jeff Paris and Alex Wilkie (1985) has been more practical for capturing subsystems of Extended Frege such as Frege or constant-depth Frege.<ref name="PW">{{cite book|first1=Jeff|last1=Paris|author-link1=Jeff Paris (mathematician)|first2=Alex|last2=Wilkie|chapter=Counting problems in bounded arithmetic |author-link2=Alex Wilkie|title=Methods in Mathematical Logic|series=Lecture Notes in Mathematics|volume=1130|year=1985|pages=317–340|doi=10.1007/BFb0075316|isbn=978-3-540-15236-1}}</ref><ref name="CN">{{cite book|last1 = Cook | first1 = Stephen | author1-link = Stephen Cook | last2 = Nguyen | first2 = Phuong| doi = 10.1017/CBO9780511676277 | isbn = 978-0-521-51729-4 | location = Cambridge | mr = 2589550 | publisher = Cambridge University Press | series = Perspectives in Logic | title = Logical Foundations of Proof Complexity | year = 2010}} ([http://www.cs.toronto.edu/~sacook/homepage/book draft from 2008])</ref>
While the above-mentioned correspondence says that proofs in a theory translate to sequences of short proofs in the corresponding proof system, a form of the opposite implication holds as well. It is possible to derive lower bounds on size of proofs in a proof system ''P'' by constructing suitable models of a theory ''T'' corresponding to the system ''P''. This allows to prove complexity lower bounds via model-theoretic constructions, an approach known as Ajtai's method.<ref name="Ajt">{{cite book|first1=M.|last1=Ajtai|author-link1=Miklós Ajtai|chapter=The complexity of the pigeonhole principle|title=Proceedings of the IEEE 29th Annual Symposium on Foundation of Computer Science|year=1988|pages=346–355}}</ref>
==SAT solvers== {{See also|SAT solver}} Propositional proof systems can be interpreted as nondeterministic algorithms for recognizing tautologies. Proving a superpolynomial lower bound on a proof system ''P'' thus rules out the existence of a polynomial-time algorithm for SAT based on ''P''. For example, runs of the DPLL algorithm on unsatisfiable instances correspond to tree-like Resolution refutations. Therefore, exponential lower bounds for tree-like Resolution (see below) rule out the existence of efficient DPLL algorithms for SAT. Similarly, exponential Resolution lower bounds imply that SAT solvers based on Resolution, such as CDCL algorithms cannot solve SAT efficiently (in worst-case).
==Lower bounds== Proving lower bounds on lengths of propositional proofs is generally very difficult. Nevertheless, several methods for proving lower bounds for weak proof systems have been discovered.
* Haken (1985) proved an exponential lower bound for Resolution and the pigeonhole principle.<ref name="Hak12">{{cite journal|first1=A.|last1=Haken|author-link1=A. Haken|title=The intractability of resolution|journal=Theoretical Computer Science|volume=39|year=1985|pages=297–308|doi=10.1016/0304-3975(85)90144-6|doi-access=}}</ref> * Ajtai (1988) proved a superpolynomial lower bound for the constant-depth Frege system and the pigeonhole principle.<ref name="Ajtb2">{{cite book|first1=M.|last1=Ajtai|author-link1=M. Ajtai|chapter=The complexity of the pigeonhole principle|title=Proceedings of the IEEE 29th Annual Symposium on Foundation of Computer Science|year=1988|pages=346–355}}</ref> This was strengthened to an exponential lower bound by Krajíček, Pudlák and Woods<ref name="KPW2">{{cite journal|first1=Jan|last1=Krajíček|first2=Pavel|last2=Pudlák|author-link2=Pavel Pudlak|first3=Alan|last3=Woods|author-link3=Alan Woods (mathematician)|title=An Exponential Lower Bound to the Size of Bounded Depth Frege Proofs of the Pigeonhole principle|journal=Random Structures and Algorithms|volume=7|number=1|year=1995|pages=15–39|doi=10.1002/rsa.3240070103}}</ref> and by Pitassi, Beame and Impagliazzo.<ref name="PBI2">{{cite journal|first1=Toniann|last1=Pitassi|author-link1=Toniann Pitassi|first2=Paul|last2=Beame|author-link2=Paul Beame|first3=Russell|last3=Impagliazzo|s2cid=1046674|author-link3=Russell Impagliazzo|title=Exponential lower bounds for the pigeonhole principle|journal=Computational Complexity|volume=3|year=1993|issue=2|pages=97–308|doi=10.1007/BF01200117}}</ref> Ajtai's lower bound uses the method of random restrictions, which was used also to derive AC<sup>0</sup> lower bounds in circuit complexity. * Krajíček (1994)<ref name="Kr12">{{cite journal|first1=Jan|last1=Krajíček|title=Lower bounds to the size of constant-depth propositional proofs|journal=Journal of Symbolic Logic|volume=59|number=1|year=1994|pages=73–86|doi=10.2307/2275250|jstor=2275250|s2cid=44670202}}</ref> formulated a method of feasible interpolation and later used it to derive new lower bounds for Resolution and other proof systems.<ref name="Kr22">{{cite journal|first1=Jan|last1=Krajíček|title=Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic|journal=Journal of Symbolic Logic|volume=62|number=2|year=1997|pages=69–83|doi=10.2307/2275541|jstor=2275541|s2cid=28517300}}</ref> * Pudlák (1997) proved exponential lower bounds for cutting planes via feasible interpolation.<ref name="Pu12">{{cite journal|first1=Pavel|last1=Pudlák|author-link1=Pavel Pudlak|title=Lower bounds for resolution and cutting planes proofs and monotone computations|journal=Journal of Symbolic Logic|volume=62|number=3|year=1997|pages=981–998|doi=10.2307/2275583|jstor=2275583|s2cid=8450089}}</ref> * Ben-Sasson and Wigderson (1999) provided a proof method reducing lower bounds on size of Resolution refutations to lower bounds on width of Resolution refutations, which captured many generalizations of Haken's lower bound.<ref name="BW2" />
It is a long-standing open problem to derive a nontrivial lower bound for the Frege system.
==Feasible interpolation== Consider a tautology of the form <math>A(x,y) \rightarrow B(y,z) </math>. The tautology is true for every choice of <math>y</math>, and after fixing <math>y</math> the evaluation of <math>A</math> and <math>B</math> are independent because they are defined on disjoint sets of variables. This means that it is possible to define an ''interpolant'' circuit <math>C(y)</math>, such that both <math>A(x,y) \rightarrow C(y)</math> and <math>C(y) \rightarrow B(y,z)</math> hold. The interpolant circuit decides either if <math>A(x,y)</math> is false or if <math>B(y,z)</math> is true, by only considering <math>y</math>. The nature of the interpolant circuit can be arbitrary. Nevertheless, it is possible to use a proof of the initial tautology <math>A(x,y) \rightarrow B(y,z) </math> as a hint on how to construct <math>C</math>. A proof systems ''P'' is said to have ''feasible interpolation'' if the interpolant <math>C(y)</math> is efficiently computable from any proof of the tautology <math>A(x,y) \rightarrow B(y,z)</math> in ''P''. The efficiency is measured with respect to the length of the proof: it is easier to compute interpolants for longer proofs, so this property seems to be anti-monotone in the strength of the proof system.
The following three statements cannot be simultaneously true: (a) <math>A(x,y) \rightarrow B(y,z)</math> has a short proof in a some proof system; (b) such proof system has feasible interpolation; (c) the interpolant circuit solves a computationally hard problem. It is clear that (a) and (b) imply that there is a small interpolant circuit, which is in contradiction with (c). Such relation allows the conversion of proof length upper bounds into lower bounds on computations, and dually to turn efficient interpolation algorithms into lower bounds on proof length.
Some proof systems such as Resolution and Cutting Planes admit feasible interpolation or its variants.<ref name="Kr22" /><ref name="Pu12" />
Feasible interpolation can be seen as a weak form of automatability. In fact, for many proof systems, such as Extended Frege, feasible interpolation is equivalent to weak automatability. Specifically, many proof systems ''P'' are able to prove their own soundness, which is a tautology <math>\mathrm{Ref}_P(\pi,\phi,x)</math> stating that `if <math>\pi</math> is a ''P''-proof of a formula <math>\phi(x)</math> then <math>\phi(x)</math> holds'. Here, <math>\pi,\phi,x</math> are encoded by free variables. Moreover, it is possible to generate ''P''-proofs of <math>\mathrm{Ref}_P(\pi,\phi,x)</math> in polynomial-time given the length of <math>\pi</math> and <math>\phi</math>. Therefore, an efficient interpolant resulting from short ''P''-proofs of soundness of ''P'' would decide whether a given formula <math>\phi</math> admits a short ''P''-proof <math>\pi</math>. Such an interpolant can be used to define a proof system ''R'' witnessing that ''P'' is weakly automatable.<ref name="PuNPpairs2">{{cite journal|first1=Pavel|last1=Pudlák|author-link1=Pavel Pudlak|title=On reducibility and symmetry of disjoint NP-pairs|journal=Theoretical Computer Science|volume=295|year=2003|pages=323–339|doi=10.2307/2275583|jstor=2275583|s2cid=8450089}}</ref> On the other hand, weak automatability of a proof system ''P'' implies that ''P'' admits feasible interpolation. However, if a proof system ''P'' does not prove efficiently its own soundness, then it might not be weakly automatable even if it admits feasible interpolation.
Many non-automatability results provide evidence against feasible interpolation in the respective systems.
* Krajíček and Pudlák (1998) proved that Extended Frege does not admit feasible interpolation unless RSA is not secure against P/poly.<ref name="KPb2">{{cite journal|first1=Jan|last1=Krajíček|first2=Pavel|last2=Pudlák|author-link2=Pavel Pudlak|title=Some consequences of cryptographical conjectures for <math>S^1_2</math> and EF|journal=Information and Computation|volume=140|number=1|year=1998|pages=82–94|doi=10.1006/inco.1997.2674|doi-access=free}}</ref> * Bonet, Pitassi and Raz (2000) proved that the <math>TC^0</math>-Frege system does not admit feasible interpolation unless the Diffie–Helman scheme is not secure against P/poly.<ref name="BPRb2">{{cite journal |last1=Bonet |first1=M.L. |author-link1=M.L. Bonet |last2=Pitassi |first2=Toniann |author-link2=Toniann Pitassi |last3=Raz |first3=Ran |author-link3=Ran Raz |year=2000 |title=On Interpolation and Automatization for Frege Proof System |journal=SIAM Journal on Computing |volume=29 |pages=1939–1967 |doi=10.1137/S0097539798353230 |number=6}}</ref> * Bonet, Domingo, Gavaldá, Maciel, Pitassi (2004) proved that constant-depth Frege systems of do not admit feasible interpolation unless the Diffie–Helman scheme is not secure against nonuniform adversaries working in subexponential time.<ref name="BDGMPb2">{{cite journal |last1=Bonet |first1=M.L. |author-link1=M.L. Bonet |last2=Domingo |first2=C. |last3=Gavaldá |first3=R. |last4=Maciel |first4=A. |last5=Pitassi |first5=Toniann |author-link5=Toniann Pitassi |year=2004 |title=Non-automatizability of Bounded-depth Frege Proofs |journal=Computational Complexity |volume=13 |issue=1–2 |pages=47–68 |doi=10.1007/s00037-004-0183-5 |s2cid=1360759}}</ref>
==Non-classical logics== Many of these questions can be asked about propositional non-classical logics too, such as intuitionistic, modal, and non-monotonic logics.
Hrubeš (2007–2009) proved exponential lower bounds on size of proofs in the Extended Frege system in some modal logics and in intuitionistic logic using a version of monotone feasible interpolation.<ref name="Hr12">{{cite journal |last1=Hrubeš |first1=Pavel |author-link1=Pavel Hrubeš |year=2007 |title=Lower bounds for modal logics |journal=Journal of Symbolic Logic |volume=72 |pages=941–958 |doi=10.2178/jsl/1191333849 |s2cid=1743011 |number=3}}</ref><ref name="Hr22">{{cite journal |last1=Hrubeš |first1=Pavel |author-link1=Pavel Hrubeš |year=2007 |title=A lower bound for intuitionistic logic |journal=Annals of Pure and Applied Logic |volume=146 |pages=72–90 |doi=10.1016/j.apal.2007.01.001 |doi-access= |number=1}}</ref><ref name="Hr32">{{cite journal |last1=Hrubeš |first1=Pavel |author-link1=Pavel Hrubeš |year=2009 |title=On lengths of proofs in non-classical logics |journal=Annals of Pure and Applied Logic |volume=157 |pages=194–205 |doi=10.1016/j.apal.2008.09.013 |doi-access=free |number=2–3}}</ref>
==See also==
* Computational complexity * Circuit complexity * Communication complexity * Mathematical logic * Proof theory * Complexity classes * NP (complexity) * coNP
==References== <references responsive="1"></references>
==Further reading==
* {{citation |last1=Beame |first1=Paul |title=Propositional proof complexity: past, present, and future |journal=Bulletin of the European Association for Theoretical Computer Science |volume=65 |pages=66–89 |year=1998 |mr=1650939 |id={{ECCC|1998|98|067}} |last2=Pitassi |first2=Toniann |author2-link=Toniann Pitassi}} * {{citation |last1=Cook |first1=Stephen |title=Logical Foundations of Proof Complexity |year=2010 |series=Perspectives in Logic |location=Cambridge |publisher=Cambridge University Press |doi=10.1017/CBO9780511676277 |isbn=978-0-521-51729-4 |mr=2589550 |last2=Nguyen |first2=Phuong |author1-link=Stephen Cook}} ([http://www.cs.toronto.edu/~sacook/homepage/book draft from 2008]) * {{citation |last=Pudlák |first=Pavel |title=Handbook of Proof Theory |volume=137 |pages=547–637 |year=1998 |editor-last=Buss |editor-first=S. R. |series=Studies in Logic and the Foundations of Mathematics |contribution=The lengths of proofs |location=Amsterdam |publisher=North-Holland |doi=10.1016/S0049-237X(98)80023-2 |isbn=978-0-444-89840-1 |mr=1640332}} * {{Cite book |last=Krajíček |first=Jan |title=Bounded arithmetic, propositional logic, and complexity theory |date=1995 |publisher=Cambridge University Press |isbn=978-0-521-45205-2 |series=Encyclopedia of mathematics and its applications |location=Cambridge [England] ; New York, NY, USA}} * {{citation |last=Krajíček |first=Jan |title=Proceedings of the 4th European Congress of Mathematics |pages=221–231 |year=2005 |editor-last=Laptev |editor-first=A. |contribution=Proof complexity |contribution-url=http://www.karlin.mff.cuni.cz/~krajicek/ecm.pdf |location=Zürich |publisher=European Mathematical Society |mr=2185746}} * {{Cite book |last=Krajíček |first=Jan |url=https://www.cambridge.org/core/books/proof-complexity/80BDF46F373753B475550D04F58098A3 |title=Proof Complexity |date=2019 |publisher=Cambridge University Press |isbn=978-1-108-41684-9 |series=Encyclopedia of Mathematics and its Applications |location=Cambridge}}
==External links==
* [https://www.cs.cmu.edu/afs/cs/project/jair/pub/volume21/dixon04a-html/node9.html Proof Complexity] * [http://list.math.cas.cz/listinfo/proof-complexity Proof complexity mailing list.]
*
Category:Computational complexity theory Category:Logic in computer science Category:Automated theorem proving