Proof complexity

From Wikipedia, the free encyclopedia
Jump to navigation Jump to search

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 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 coNP (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=coNP.

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 Bounded Arithmetic theories, 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.

Proof systems[edit]

A propositional proof system is given as a proof-verification algorithm P(A,x) with two inputs. If P accepts the pair (A,x) we say that x is a P-proof of A. P is required to run in polynomial time, and moreover, it must hold that A has a P-proof if and only if it is a tautology.

Examples of propositional proof systems include Sequent calculus, Resolution, Cutting Planes and Frege system. Strong mathematical theories such as ZFC induce propositional proof systems as well: a proof of a tautology in a propositional interpretation of ZFC is a ZFC-proof of a formalized statement ' is a tautology'.

Proofs of polynomial size and the NP versus coNP problem[edit]

Proof complexity measures the efficiency of the proof system usually in terms of the minimal size of proofs possible in the system for a given tautology. The size of a proof (resp. formula) is the number of symbols needed to represent the proof (resp. formula). A propositional proof system P is polynomially bounded if there exists a constant such that every tautology of size has a P-proof of size . A central question of proof complexity is to understand if tautologies admit polynomial-size proofs. Formally,

Problem (NP vs. coNP)

Does there exist a polynomially bounded propositional proof system?

Cook and Reckhow (1979) observed that there exists a polynomially bounded proof system if and only if NP=coNP. Therefore, proving that specific proof systems do not admit polynomial size proofs can be seen as a partial progress towards separating NP and coNP (and thus P and NP).[1]

Optimality and simulations between proof systems[edit]

Proof complexity compares the strength of proof systems using the notion of simulation. A proof system P p-simulates a proof system Q if there is a polynomial-time function which given a Q-proof outputs a P-proof of the same tautology. If P p-simulates Q and Q p-simulates P, the proof systems P and Q are p-equivalent. There is also a weaker notion of simulation: a proof system P simulates a proof system Q if there is a polynomial p such that for every Q-proof x of a tautology A, there is a P-proof y of A such that the length of y, |y| is at most p(|x|).

For example, sequent calculus is p-equivalent to (every) Frege system.[2]

A proof system is p-optimal if it p-simulates all other proof systems, and it is optimal if it simulates all other proof systems. It is an open problem whether such proof systems exist:

Problem (Optimality)

Does there exist a p-optimal or optimal propositional proof system?

Every propositional proof system P can be simulated by Extended Frege extended with axioms postulating soundness of P.[3] The existence of optimal (resp. p-optimal) proof system is known to follow from the assumption that NE=coNE (resp. E=NE).[4]

For many weak proof systems it is known that they do not 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.[5]

Automatability of proof search[edit]

An important question in proof complexity is to understand the complexity of searching for proofs in proof systems.

Problem (Automatability)

Are there efficient algorithms searching for proofs in standard proof systems such as Resolution or Frege system?

The question can be formalized by the notion of automatability (a.k.a. automatizability).[6]

A proof system P is automatable if there is an algorithm which given a tautology outputs a P-proof of in time polynomial in the size of and the length of the shortest P-proof of . Note that if a proof system is not polynomially bounded, it can still be automatable. A proof system P is weakly automatable if there is a proof system R and an algorithm which given a tautology outputs an R-proof of in time polynomial in the size of and the length of the shortest P-proof of .

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.[7]
  • Bonet, Pitassi and Raz (2000) proved that -Frege system is not weakly automatable unless the Diffie-Helman scheme is not secure against P/poly.[6] 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 Diffie-Helman scheme is not secure against nonuniform adversaries working in subexponential time.[8]
  • Alekhnovich and Razborov (2008) proved that tree-like Resolution and Resolution are not automatable unless FPT=W[P].[9] This was extended by Galesi and Lauria (2010) who proved that Nullstellensatz and Polynomial Calculus are not automatable unless the fixed parameter hierarchy collapses.[10] 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.[11]
  • Atserias and Müller (2019) proved that Resolution is not automatable unless P=NP.[12] This was extended by de Rezende, Göös, Nordström, Pitassi, Robere and Sokolov (2020) to NP-hardness of automating Nullstellensatz, Polynomial Calculus, Sherali-Adams;[13] by Göös, Koroth, Mertz and Pitassi (2020) to NP-hardness of automating Cutting Planes;[14] and by Garlík (2020) to NP-hardness of automating k-DNF Resolution.[15]

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.[16][17]

Bounded arithmetic[edit]

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, Extended Frege system corresponds to Cook's theory formalizing polynomial-time reasoning and Frege system corresponds to the theory formalizing reasoning.

The correspondence has been introduced by Stephen Cook (1975), who showed that coNP theorems, formally formulas, of the theory 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.[18]

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.[19] [20]

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.[21]

SAT solvers[edit]

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 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[edit]

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.[22]
  • Ajtai (1988) proved a superpolynomial lower bound for constant-depth Frege system and the pigeonhole principle.[21] This was strengthened to an exponential lower bound by Krajíček, Pudlák and Woods[23] and by Pitassi, Beame and Impagliazzo.[24] Ajtai's lower bound uses the method of random restrictions which was used also to derive AC0 lower bounds in circuit complexity.
  • Krajíček (1994)[25] formulated a method of feasible interpolation and later used it derive new lower bounds for Resolution and other proof systems.[26]
  • Pudlák (1997) proved exponential lower bounds for cutting planes via feasible interpolation.[27]
  • 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.[17]

It is a long-standing open problem to derive a nontrivial lower bound for Frege system.

Feasible interpolation[edit]

Consider a tautology of the form . The tautology is true for every choice of , and after fixing the evaluation of and are independent because they are defined on disjoint sets of variables. This means that it is possible to define an interpolant circuit , such that both and hold. The interpolant circuit decides either if is false or if is true, by only considering . The nature of the interpolant circuit can be arbitrary. Nevertheless, it is possible to use a proof of the initial tautology as a hint on how to construct . A proof systems P is said to have feasible interpolation if the interpolant is efficiently computable from any proof of the tautology 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) 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 to turn 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.[26][27]

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 stating that `if is a P-proof of a formula then holds'. Here, are encoded by free variables. Moreover, it is possible to generate P-proofs of in polynomial-time given the length of and . Therefore, an efficient interpolant resulting from short P-proofs of soundness of P would decide whether a given formula admits a short P-proof . Such an interpolant can be used to define a proof system R witnessing that P is weakly automatable.[28] 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 actually an 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.[7]
  • Bonet, Pitassi and Raz (2000) proved that -Frege system does not admit feasible interpolation unless the Diffie-Helman scheme is not secure against P/poly.[6]
  • Bonet, Domingo, Gavaldá, Maciel, Pitassi (2004) proved that constant-depth Frege systems of do not admit feasible interpolation unless Diffie-Helman scheme is not secure against nonuniform adversaries working in subexponential time.[8]

Non-classical logics[edit]

The idea of comparing the size of proofs can be used for any automated reasoning procedure that generates a proof. Some research has been done about the size of proofs for propositional non-classical logics, in particular, intuitionistic, modal, and non-monotonic logics.

Hrubeš (2007-2009) proved exponential lower bounds on size of proofs in Extended Frege system in some modal logics and intuitionistic logic using a version of monotone feasible interpolation.[29][30][31]

See also[edit]

References[edit]

  1. ^ Cook, Stephen; Reckhow, Robert A. (1979). "The Relative Efficiency of Propositional Proof Systems". Journal of Symbolic Logic. 44 (1): 36–50. doi:10.2307/2273702. JSTOR 2273702.
  2. ^ Reckhow, Robert A. (1976). On the lengths of proofs in the propositional calculus (PhD Thesis). University of Toronto.
  3. ^ Krajíček, Jan (2019). "Proof complexity". Cambridge University Press.
  4. ^ Krajíček, Jan; Pudlák, Pavel (1989). "Propositional proof systems, the consistency of first-order theories and the complexity of computations". Journal of Symbolic Logic. 54 (3): 1063–1079. doi:10.2307/2274765. JSTOR 2274765.
  5. ^ Pitassi, Toniann; Santhanam, Rahul (2010). "Effectively polynomial simulations" (PDF). ICS: 370–382.
  6. ^ a b c Bonet, M.L.; Pitassi, Toniann; Raz, Ran (2000). "On Interpolation and Automatization for Frege Proof System". SIAM Journal on Computing. 29 (6): 1939–1967. doi:10.1137/S0097539798353230.
  7. ^ a b Krajíček, Jan; Pudlák, Pavel (1998). "Some consequences of cryptographical conjectures for and EF". Information and Computation. 140 (1): 82–94. doi:10.1006/inco.1997.2674.
  8. ^ a b Bonet, M.L.; Domingo, C.; Gavaldá, R.; Maciel, A.; Pitassi, Toniann (2004). "Non-automatizability of Bounded-depth Frege Proofs". Computational Complexity. 13 (1–2): 47–68. doi:10.1007/s00037-004-0183-5. S2CID 1360759.
  9. ^ Alekhnovich, Michael; Razborov, Alexander (2018). "Resolution is not automatizable unless W[P] is tractable". SIAM Journal on Computing. 38 (4): 1347–1363. doi:10.1137/06066850X.
  10. ^ Galesi, Nicola; Lauria, Massimo (2010). "On the automatizability of polynomial calculus". Theory of Computing Systems. 47 (2): 491–506. doi:10.1007/s00224-009-9195-5. S2CID 11602606.
  11. ^ Mertz, Ian; Pitassi, Toniann; Wei, Yuanhao (2019). "Short proofs are hard to find". ICALP.
  12. ^ Atserias, Albert; Müller, Moritz (2019). "Automating resolution is NP-hard". Proceedings of the 60th Symposium on Foundations of Computer Science. pp. 498–509.
  13. ^ de Rezende, Susanna; Göös, Mika; Nordström, Jakob; Pitassi, Tonnian; Robere, Robert; Sokolov, Dmitry (2020). "Automating algebraic proof systems is NP-hard". CCC.
  14. ^ Göös, Mika; Koroth, Sajin; Mertz, Ian; Pitassi, Tonnian (2020). "Automating cutting planes is NP-hard". STOC: 68–77. arXiv:2004.08037. doi:10.1145/3357713.3384248. ISBN 9781450369794. S2CID 215814356.
  15. ^ Garlík, Michal (2020). "Failure of feasible disjunction property for k-DNF Resolution and NP-hardness of automating it". ECCC. arXiv:2003.10230.
  16. ^ Beame, Paul; Pitassi, Toniann (1996). "Simplified and improved resolution lower bounds". 37th Annual Symposium on Foundations of Computer Science: 274–282.
  17. ^ a b Ben-Sasson, Eli; Wigderson, Avi (1999). "Short proofs are narrow - resolution made simple". Proceedings of the 31st ACM Symposium on Theory of Computing. pp. 517–526.
  18. ^ Cook, Stephen (1975). "Feasibly constructive proofs and the propositiona calculus". Proceedings of the 7th Annual ACM Symposium on Theory of Computing. pp. 83–97.
  19. ^ Paris, Jeff; Wilkie, Alex (1985). "Counting problems in bounded arithmetic". Methods in Mathematical Logic. Lecture Notes in Mathematics. 1130: 317–340. doi:10.1007/BFb0075316. ISBN 978-3-540-15236-1.
  20. ^ Cook, Stephen; Nguyen, Phuong (2010). Logical Foundations of Proof Complexity. Perspectives in Logic. Cambridge: Cambridge University Press. doi:10.1017/CBO9780511676277. ISBN 978-0-521-51729-4. MR 2589550. (draft from 2008)
  21. ^ a b Ajtai, M. (1988). "The complexity of the pigeonhole principle". Proceedings of the IEEE 29th Annual Symposium on Foundation of Computer Science. pp. 346–355.
  22. ^ Haken, A. (1985). "The intractability of resolution". Theoretical Computer Science. 39: 297–308. doi:10.1016/0304-3975(85)90144-6.
  23. ^ Krajíček, Jan; Pudlák, Pavel; Woods, Alan (1995). "An Exponential Lower Bound to the Size of Bounded Depth Frege Proofs of the Pigeonhole principle". Random Structures and Algorithms. 7 (1): 15–39. doi:10.1002/rsa.3240070103.
  24. ^ Pitassi, Toniann; Beame, Paul; Impagliazzo, Russell (1993). "Exponential lower bounds for the pigeonhole principle". Computational Complexity. 3 (2): 97–308. doi:10.1007/BF01200117. S2CID 1046674.
  25. ^ Krajíček, Jan (1994). "Lower bounds to the size of constant-depth propositional proofs". Journal of Symbolic Logic. 59 (1): 73–86. doi:10.2307/2275250. JSTOR 2275250.
  26. ^ a b Krajíček, Jan (1997). "Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic". Journal of Symbolic Logic. 62 (2): 69–83. doi:10.2307/2275541. JSTOR 2275541.
  27. ^ a b Pudlák, Pavel (1997). "Lower bounds for resolution and cutting planes proofs and monotone computations". Journal of Symbolic Logic. 62 (3): 981–998. doi:10.2307/2275583. JSTOR 2275583.
  28. ^ Pudlák, Pavel (2003). "On reducibility and symmetry of disjoint NP-pairs". Theor. Comput. Science. 295: 323–339. doi:10.2307/2275583. JSTOR 2275583.
  29. ^ Hrubeš, Pavel (2007). "Lower bounds for modal logics". Journal of Symbolic Logic. 72 (3): 941–958. doi:10.2178/jsl/1191333849.
  30. ^ Hrubeš, Pavel (2007). "A lower bound for intuitionistic logic". Annals of Pure and Applied Logic. 146 (1): 72–90. doi:10.1016/j.apal.2007.01.001.
  31. ^ Hrubeš, Pavel (2009). "On lengths of proofs in non-classical logics". Annals of Pure and Applied Logic. 157 (2–3): 194–205. doi:10.1016/j.apal.2008.09.013.

Further reading[edit]

External links[edit]