1110:
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,
1752:
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
800:
is not secure against P/poly. 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
239:
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 (respectively formula) is the number of symbols needed to represent the proof (respectively formula). A propositional proof
1130:
Ajtai (1988) proved a superpolynomial lower bound for the constant-depth Frege system and the pigeonhole principle. This was strengthened to an exponential lower bound by KrajĂÄŤek, Pudlák and Woods and by
Pitassi, Beame and Impagliazzo. Ajtai's lower bound uses the method of random restrictions,
824:
Atserias and MĂĽller (2019) proved that
Resolution is not automatable unless P=NP. This was extended by de Rezende, Göös, Nordström, Pitassi, Robere and Sokolov (2020) to NP-hardness of automating Nullstellensatz and Polynomial Calculus; by Göös, Koroth, Mertz and Pitassi (2020) to NP-hardness of
79:
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
60:(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
345:
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).
1059:
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
36:
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
2149:
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
49:, 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.
511:
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
1759:
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
1148:
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
1693:. 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.
812:
and
Polynomial Calculus are not automatable unless the fixed-parameter hierarchy collapses. Mertz, Pitassi and Wei (2019) proved that tree-like Resolution and Resolution are not automatable even in certain
2178:
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.
1992:
1818:
3551:
2554:
2159:
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
1123:
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.
844:
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.
102:, 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.
1750:
1687:
1574:
1215:
1428:
1378:
963:
928:
1031:
893:
3028:
1932:
999:
859:
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
3324:
2472:
329:
1900:
1871:
2144:
1498:
1463:
794:
2060:
2032:
1753:
conversion of proof length upper bounds into lower bounds on computations, and dually to turn efficient interpolation algorithms into lower bounds on proof length.
735:
711:
691:
667:
635:
611:
591:
567:
229:
209:
2084:
2012:
1838:
1631:
1328:
1098:
Propositional proof systems can be interpreted as nondeterministic algorithms for recognizing tautologies. Proving a superpolynomial lower bound on a proof system
1033:
translate to sequences of tautologies with polynomial-size proofs in Extended Frege. Moreover, Extended Frege is the weakest such system: if another proof system
1594:
1518:
1295:
1275:
1255:
1235:
286:
266:
2688:
de Rezende, Susanna; Göös, Mika; Nordström, Jakob; Pitassi, Tonnian; Robere, Robert; Sokolov, Dmitry (2020). "Automating algebraic proof systems is NP-hard".
3568:
2776:
2690:
2670:
2371:
3505:
3475:
3437:
2826:
57:
1142:
KrajĂÄŤek (1994) formulated a method of feasible interpolation and later used it to derive new lower bounds for Resolution and other proof systems.
3289:
3242:
3196:
3024:
2437:
2321:
72:
from NP), since the existence of a propositional proof system that admits polynomial size proofs for all tautologies is equivalent to NP=coNP.
3395:
3357:
3062:
2801:
2545:
2396:
3005:
2973:
500:. The existence of an optimal (respectively p-optimal) proof system is known to follow from the assumption that NE=coNE (respectively
2113:
KrajĂÄŤek and Pudlák (1998) proved that Extended Frege does not admit feasible interpolation unless RSA is not secure against P/poly.
3712:
740:
Many proof systems of interest are believed to be non-automatable. However, currently only conditional negative results are known.
3150:
KrajĂÄŤek, Jan (1997). "Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic".
1520:. The nature of the interpolant circuit can be arbitrary. Nevertheless, it is possible to use a proof of the initial tautology
2106:
does not prove efficiently its own soundness, then it might not be weakly automatable even if it admits feasible interpolation.
2978:
3599:
2926:
2890:
837:
It is not known if the weak automatability of Resolution would break any standard complexity-theoretic hardness assumptions.
3722:
3717:
534:
Are there efficient algorithms searching for proofs in standard proof systems such as Resolution or the Frege system?
1941:
1767:
2756:
2732:
1297:
are independent because they are defined on disjoint sets of variables. This means that it is possible to define an
524:
An important question in proof complexity is to understand the complexity of searching for proofs in proof systems.
3692:
3639:
2324:(1989). "Propositional proof systems, the consistency of first-order theories and the complexity of computations".
3666:, Studies in Logic and the Foundations of Mathematics, vol. 137, Amsterdam: North-Holland, pp. 547–637,
2187:
2146:-Frege system does not admit feasible interpolation unless the Diffie–Helman scheme is not secure against P/poly.
1112:
1056:(1985) has been more practical for capturing subsystems of Extended Frege such as Frege or constant-depth Frege.
331:. A central question of proof complexity is to understand if tautologies admit polynomial-size proofs. Formally,
29:
1699:
1636:
1523:
1164:
3031:(1995). "An Exponential Lower Bound to the Size of Bounded Depth Frege Proofs of the Pigeonhole principle".
1383:
1333:
75:
Contemporary proof complexity research draws ideas and methods from many areas in computational complexity,
2589:
Alekhnovich, Michael; Razborov, Alexander (2018). "Resolution is not automatizable unless W is tractable".
2109:
Many non-automatability results provide evidence against feasible interpolation in the respective systems.
804:
Alekhnovich and Razborov (2008) proved that tree-like Resolution and Resolution are not automatable unless
21:
2618:
2478:
818:
188:
2705:
Göös, Mika; Koroth, Sajin; Mertz, Ian; Pitassi, Tonnian (2020). "Automating cutting planes is NP-hard".
934:
898:
2866:
1756:
Some proof systems such as Resolution and Cutting Planes admit feasible interpolation or its variants.
1049:
1004:
866:
637:. Note that if a proof system is not polynomially bounded, it can still be automatable. A proof system
354:
Proof complexity compares the strength of proof systems using the notion of simulation. A proof system
111:
38:
2409:
2247:
2197:
805:
1905:
972:
969:
The correspondence was introduced by Stephen Cook (1975), who showed that coNP theorems, formally
931:
830:
538:
The question can be formalized by the notion of automatability (also known as automatizability).
493:
474:
if it simulates all other proof systems. It is an open problem whether such proof systems exist:
3297:
2445:
295:
46:
1876:
1847:
814:
2375:
2119:
1468:
1433:
1153:
It is a long-standing open problem to derive a nontrivial lower bound for the Frege system.
1145:
Pudlák (1997) proved exponential lower bounds for cutting planes via feasible interpolation.
769:
3679:
3648:
3609:
3564:
3199:(1997). "Lower bounds for resolution and cutting planes proofs and monotone computations".
2936:
2164:
2045:
2017:
1127:
Haken (1985) proved an exponential lower bound for Resolution and the pigeonhole principle.
720:
696:
676:
652:
620:
596:
576:
552:
214:
194:
180:
91:
2616:
Galesi, Nicola; Lauria, Massimo (2010). "On the automatizability of polynomial calculus".
2507:
2069:
1997:
1823:
1607:
1304:
755:
8:
3104:
KrajĂÄŤek, Jan (1994). "Lower bounds to the size of constant-depth propositional proofs".
3066:
2172:
2160:
3655:
3457:
3419:
3270:
3262:
3224:
3216:
3175:
3167:
3129:
3121:
3086:
2781:
2750:
2738:
2710:
2635:
2571:
2349:
2341:
2272:
2264:
2245:; Reckhow, Robert A. (1979). "The Relative Efficiency of Propositional Proof Systems".
2212:
2202:
2192:
1579:
1503:
1280:
1260:
1240:
1220:
1136:
1045:
860:
854:
744:
KrajĂÄŤek and Pudlák (1998) proved that Extended Frege is not weakly automatable unless
271:
251:
176:
99:
87:
3671:
3595:
2991:
2922:
2886:
2742:
2728:
895:
formalizing polynomial-time reasoning and the Frege system corresponds to the theory
3697:
3179:
3133:
2653:
Mertz, Ian; Pitassi, Toniann; Wei, Yuanhao (2019). "Short proofs are hard to find".
2639:
2353:
3667:
3587:
3521:
3487:
3461:
3449:
3423:
3411:
3377:
3337:
3274:
3254:
3228:
3208:
3159:
3113:
3090:
3078:
3040:
2987:
2914:
2878:
2720:
2627:
2598:
2575:
2563:
2527:
2487:
2418:
2333:
2276:
2256:
211:
in a propositional interpretation of ZFC is a ZFC-proof of a formalized statement '
172:
95:
3631:
3614:
2942:
41:. For example, among the major challenges of proof complexity is showing that the
3675:
3644:
3605:
3560:
3546:
3399:
3361:
3058:
2932:
2805:
2549:
2511:
2400:
2367:
2217:
1077:
809:
759:
505:
61:
2955:
2094:
is weakly automatable. On the other hand, weak automatability of a proof system
1081:
3572:
3526:
3509:
3491:
3010:
Proceedings of the IEEE 29th Annual Symposium on Foundation of Computer Science
2960:
Proceedings of the IEEE 29th Annual Symposium on Foundation of Computer Science
1107:
745:
501:
69:
3415:
3381:
2631:
2567:
2531:
2422:
3706:
3591:
3453:
2918:
2830:
1102:
thus rules out the existence of a polynomial-time algorithm for SAT based on
1065:
825:
automating Cutting Planes; and by GarlĂk (2020) to NP-hardness of automating
2724:
3579:
3342:
3293:
3044:
2906:
2848:
2492:
2441:
2242:
2207:
797:
234:
184:
53:
42:
25:
2707:
Proceedings of the 52nd Annual ACM SIGACT Symposium on Theory of Computing
2870:
2168:
1053:
116:
A propositional proof system is given as a proof-verification algorithm
3266:
3220:
3171:
3125:
3082:
2882:
2345:
2268:
1093:
459:
For example, sequent calculus is p-equivalent to (every) Frege system.
156:
is required to run in polynomial time, and moreover, it must hold that
81:
3368:(2000). "On Interpolation and Automatization for Frege Proof System".
2851:(1975). "Feasibly constructive proofs and the propositiona calculus".
2602:
2518:(2000). "On Interpolation and Automatization for Frege Proof System".
2407:(2000). "On Interpolation and Automatization for Frege Proof System".
863:. For example, the Extended Frege system corresponds to Cook's theory
3662:
Pudlák, Pavel (1998), "The lengths of proofs", in Buss, S. R. (ed.),
3552:
Bulletin of the European Association for Theoretical Computer Science
3549:(1998), "Propositional proof complexity: past, present, and future",
2770:
GarlĂk, Michal (2020). "Failure of feasible disjunction property for
76:
3258:
3212:
3163:
3117:
2675:
Proceedings of the 60th Symposium on Foundations of Computer Science
2337:
2260:
1934:
are encoded by free variables. Moreover, it is possible to generate
484:
Does there exist a p-optimal or optimal propositional proof system?
341:
Does there exist a polynomially bounded propositional proof system?
2786:
2715:
349:
191:
induce propositional proof systems as well: a proof of a tautology
2877:. Lecture Notes in Mathematics. Vol. 1130. pp. 317–340.
2853:
Proceedings of the 7th Annual ACM Symposium on Theory of Computing
1696:
The following three statements cannot be simultaneously true: (a)
90:
can also serve as a framework to study propositional proof sizes.
3365:
3069:(1993). "Exponential lower bounds for the pigeonhole principle".
2515:
2404:
763:
3586:, Perspectives in Logic, Cambridge: Cambridge University Press,
2913:. Perspectives in Logic. Cambridge: Cambridge University Press.
808:. This was extended by Galesi and Lauria (2010) who proved that
749:
3623:
Bounded arithmetic, propositional logic, and complexity theory
3402:(2004). "Non-automatizability of Bounded-depth Frege Proofs".
2687:
2552:(2004). "Non-automatizability of Bounded-depth Frege Proofs".
401:. There is also a weaker notion of simulation: a proof system
3245:(2003). "On reducibility and symmetry of disjoint NP-pairs".
2673:; MĂĽller, Moritz (2019). "Automating resolution is NP-hard".
2655:
17:
2835:
Proceedings of the 31st ACM Symposium on Theory of Computing
2833:(1999). "Short proofs are narrow - resolution made simple".
1764:
are able to prove their own soundness, which is a tautology
52:
Systematic study of proof complexity began with the work of
3643:, Zürich: European Mathematical Society, pp. 221–231,
2808:(1996). "Simplified and improved resolution lower bounds".
2222:
2086:. Such an interpolant can be used to define a proof system
2034:. Therefore, an efficient interpolant resulting from short
65:
2102:
admits feasible interpolation. However, if a proof system
1633:
is efficiently computable from any proof of the tautology
3394:
2544:
1132:
1115:
algorithms cannot solve SAT efficiently (in worst-case).
2810:
37th Annual Symposium on Foundations of Computer Science
235:
Proofs of polynomial size and the NP versus coNP problem
3640:
Proceedings of the 4th European Congress of Mathematics
3057:
3294:"Some consequences of cryptographical conjectures for
3008:(1988). "The complexity of the pigeonhole principle".
2958:(1988). "The complexity of the pigeonhole principle".
2704:
2442:"Some consequences of cryptographical conjectures for
2292:
On the lengths of proofs in the propositional calculus
3300:
2448:
2122:
2072:
2048:
2020:
2000:
1944:
1908:
1879:
1850:
1826:
1770:
1702:
1639:
1610:
1582:
1526:
1506:
1471:
1436:
1386:
1336:
1307:
1283:
1263:
1243:
1223:
1167:
1007:
975:
937:
901:
869:
772:
723:
699:
679:
655:
623:
599:
579:
555:
298:
274:
254:
217:
197:
365:
if there is a polynomial-time function that given a
3022:
2873:(1985). "Counting problems in bounded arithmetic".
2825:
2774:-DNF Resolution and NP-hardness of automating it".
2588:
1076:. This allows to prove complexity lower bounds via
796:-Frege system is not weakly automatable unless the
3478:(2007). "A lower bound for intuitionistic logic".
3318:
2466:
2138:
2078:
2054:
2026:
2006:
1986:
1926:
1894:
1865:
1832:
1812:
1744:
1681:
1625:
1588:
1568:
1512:
1492:
1457:
1422:
1372:
1322:
1289:
1269:
1249:
1229:
1209:
1025:
993:
957:
922:
887:
788:
729:
705:
685:
661:
629:
605:
585:
561:
323:
280:
260:
223:
203:
1430:hold. The interpolant circuit decides either if
519:
3704:
2366:
1987:{\displaystyle \mathrm {Ref} _{P}(\pi ,\phi ,x)}
1813:{\displaystyle \mathrm {Ref} _{P}(\pi ,\phi ,x)}
549:if there is an algorithm that given a tautology
350:Optimality and simulations between proof systems
171:Examples of propositional proof systems include
3356:
2652:
2506:
2395:
1048:statements and propositional formulas given by
3510:"On lengths of proofs in non-classical logics"
3287:
2669:
2435:
2319:
2116:Bonet, Pitassi and Raz (2000) proved that the
496:extended with axioms postulating soundness of
470:-simulates all other proof systems, and it is
1217:. The tautology is true for every choice of
3544:
2976:(1985). "The intractability of resolution".
2800:
2615:
2865:
2241:
3578:
2905:
3525:
3440:(2007). "Lower bounds for modal logics".
3341:
3235:
2785:
2714:
2491:
1156:
3629:
3620:
3398:; Domingo, C.; Gavaldá, R.; Maciel, A.;
3149:
3103:
2548:; Domingo, C.; Gavaldá, R.; Maciel, A.;
2304:
1745:{\displaystyle A(x,y)\rightarrow B(y,z)}
1682:{\displaystyle A(x,y)\rightarrow B(y,z)}
1569:{\displaystyle A(x,y)\rightarrow B(y,z)}
1210:{\displaystyle A(x,y)\rightarrow B(y,z)}
649:and an algorithm that given a tautology
3584:Logical Foundations of Proof Complexity
2911:Logical Foundations of Proof Complexity
2289:
2154:
1994:in polynomial-time given the length of
187:. Strong mathematical theories such as
3705:
3661:
3504:
3474:
3436:
3388:
3241:
3195:
3191:
3189:
3145:
3143:
2769:
2681:
2582:
1423:{\displaystyle C(y)\rightarrow B(y,z)}
1373:{\displaystyle A(x,y)\rightarrow C(y)}
944:
941:
94:and, in particular, weak fragments of
3004:
2972:
2954:
2821:
2819:
2042:would decide whether a given formula
848:
3350:
2998:
2966:
2847:
2841:
2698:
2609:
2538:
2376:"Effectively polynomial simulations"
2294:(PhD Thesis). University of Toronto.
1080:constructions, an approach known as
3658:, Cambridge University Press, 2019.
3498:
3468:
3430:
3281:
3186:
3140:
3097:
3051:
3016:
2948:
2763:
2646:
2500:
1044:An alternative translation between
13:
3538:
2899:
2859:
2816:
2794:
2663:
2389:
2313:
2298:
2283:
1953:
1950:
1947:
1779:
1776:
1773:
1013:
1010:
977:
958:{\displaystyle {\mathsf {NC}}^{1}}
923:{\displaystyle \mathrm {VNC} ^{1}}
910:
907:
904:
875:
872:
693:in time polynomial in the size of
593:in time polynomial in the size of
514:effectively polynomially simulates
268:such that every tautology of size
14:
3734:
3686:
2429:
2360:
2235:
1161:Consider a tautology of the form
1026:{\displaystyle \mathrm {PV} _{1}}
888:{\displaystyle \mathrm {PV} _{1}}
488:Every propositional proof system
373:-proof of the same tautology. If
3514:Annals of Pure and Applied Logic
3480:Annals of Pure and Applied Logic
3033:Random Structures and Algorithms
369:-proof of a tautology outputs a
105:
3713:Computational complexity theory
1118:
713:and the length of the shortest
613:and the length of the shortest
98:, which come under the name of
30:computational complexity theory
3698:Proof complexity mailing list.
1981:
1963:
1889:
1883:
1860:
1854:
1807:
1789:
1739:
1727:
1721:
1718:
1706:
1676:
1664:
1658:
1655:
1643:
1620:
1614:
1576:as a hint on how to construct
1563:
1551:
1545:
1542:
1530:
1487:
1475:
1452:
1440:
1417:
1405:
1399:
1396:
1390:
1367:
1361:
1355:
1352:
1340:
1317:
1311:
1204:
1192:
1186:
1183:
1171:
1131:which was used also to derive
1087:
520:Automatability of proof search
312:
299:
1:
3672:10.1016/S0049-237X(98)80023-2
2875:Methods in Mathematical Logic
2755:: CS1 maint: date and year (
2309:. Cambridge University Press.
2228:
1500:is true, by only considering
3625:, Cambridge University Press
3247:Theoretical Computer Science
2992:10.1016/0304-3975(85)90144-6
2979:Theoretical Computer Science
1927:{\displaystyle \pi ,\phi ,x}
1072:corresponding to the system
994:{\displaystyle \Pi _{1}^{b}}
22:theoretical computer science
7:
3330:Information and Computation
2619:Theory of Computing Systems
2479:Information and Computation
2290:Reckhow, Robert A. (1976).
2181:
1106:. For example, runs of the
819:exponential time hypothesis
645:if there is a proof system
248:if there exists a constant
39:propositional proof systems
10:
3739:
3527:10.1016/j.apal.2008.09.013
3492:10.1016/j.apal.2007.01.001
1091:
1041:simulates Extended Frege.
852:
112:propositional proof system
109:
3723:Automated theorem proving
3718:Logic in computer science
3582:; Nguyen, Phuong (2010),
3442:Journal of Symbolic Logic
3416:10.1007/s00037-004-0183-5
3382:10.1137/S0097539798353230
3370:SIAM Journal on Computing
3319:{\displaystyle S_{2}^{1}}
3201:Journal of Symbolic Logic
3152:Journal of Symbolic Logic
3106:Journal of Symbolic Logic
2909:; Nguyen, Phuong (2010).
2632:10.1007/s00224-009-9195-5
2591:SIAM Journal on Computing
2568:10.1007/s00037-004-0183-5
2532:10.1137/S0097539798353230
2520:SIAM Journal on Computing
2467:{\displaystyle S_{2}^{1}}
2423:10.1137/S0097539798353230
2410:SIAM Journal on Computing
2326:Journal of Symbolic Logic
2248:Journal of Symbolic Logic
1064:by constructing suitable
412:if there is a polynomial
324:{\displaystyle (n+c)^{c}}
3664:Handbook of Proof Theory
3592:10.1017/CBO9780511676277
3404:Computational Complexity
3071:Computational Complexity
2919:10.1017/CBO9780511676277
2555:Computational Complexity
2198:Communication complexity
2188:Computational complexity
2038:-proofs of soundness of
1895:{\displaystyle \phi (x)}
1866:{\displaystyle \phi (x)}
1037:has this property, then
1001:formulas, of the theory
440:such that the length of
3637:, in Laptev, A. (ed.),
2725:10.1145/3357713.3384248
766:(2000) proved that the
128:) with two inputs. If
3630:KrajĂÄŤek, Jan (2005),
3621:KrajĂÄŤek, Jan (1995),
3454:10.2178/jsl/1191333849
3343:10.1006/inco.1997.2674
3320:
3045:10.1002/rsa.3240070103
2493:10.1006/inco.1997.2674
2468:
2305:KrajĂÄŤek, Jan (2019).
2140:
2139:{\displaystyle TC^{0}}
2080:
2056:
2028:
2008:
1988:
1928:
1896:
1867:
1834:
1814:
1746:
1683:
1627:
1602:feasible interpolation
1590:
1570:
1514:
1494:
1493:{\displaystyle B(y,z)}
1459:
1458:{\displaystyle A(x,y)}
1424:
1374:
1324:
1291:
1271:
1251:
1231:
1211:
1157:Feasible interpolation
1027:
995:
959:
924:
889:
840:On the positive side,
790:
789:{\displaystyle TC^{0}}
748:is not secure against
731:
707:
687:
663:
631:
607:
587:
563:
536:
486:
343:
325:
282:
262:
225:
205:
164:-proof if and only if
80:applied areas such as
47:propositional calculus
3321:
2469:
2141:
2081:
2057:
2055:{\displaystyle \phi }
2029:
2027:{\displaystyle \phi }
2009:
1989:
1929:
1897:
1868:
1835:
1815:
1747:
1684:
1628:
1591:
1571:
1515:
1495:
1460:
1425:
1375:
1325:
1292:
1272:
1252:
1232:
1212:
1028:
996:
960:
925:
890:
815:quasi-polynomial time
798:Diffie–Hellman scheme
791:
732:
730:{\displaystyle \tau }
708:
706:{\displaystyle \tau }
688:
686:{\displaystyle \tau }
664:
662:{\displaystyle \tau }
632:
630:{\displaystyle \tau }
608:
606:{\displaystyle \tau }
588:
586:{\displaystyle \tau }
564:
562:{\displaystyle \tau }
526:
476:
333:
326:
283:
263:
226:
224:{\displaystyle \tau }
206:
204:{\displaystyle \tau }
3298:
3067:Impagliazzo, Russell
2446:
2173:non-monotonic logics
2161:non-classical logics
2155:Non-classical logics
2120:
2079:{\displaystyle \pi }
2070:
2046:
2018:
2007:{\displaystyle \pi }
1998:
1942:
1906:
1877:
1848:
1844:-proof of a formula
1833:{\displaystyle \pi }
1824:
1768:
1700:
1637:
1626:{\displaystyle C(y)}
1608:
1580:
1524:
1504:
1469:
1434:
1384:
1334:
1323:{\displaystyle C(y)}
1305:
1281:
1261:
1241:
1221:
1165:
1005:
973:
935:
899:
867:
770:
721:
697:
677:
653:
621:
597:
577:
553:
492:can be simulated by
416:such that for every
389:, the proof systems
296:
272:
252:
246:polynomially bounded
215:
195:
92:First-order theories
3315:
3012:. pp. 346–355.
2962:. pp. 346–355.
2837:. pp. 517–526.
2677:. pp. 498–509.
2463:
1604:if the interpolant
1596:. A proof systems
1237:, and after fixing
990:
24:, and specifically
3632:"Proof complexity"
3316:
3301:
3083:10.1007/BF01200117
2883:10.1007/BFb0075316
2709:. pp. 68–77.
2464:
2449:
2213:Complexity classes
2203:Mathematical logic
2193:Circuit complexity
2136:
2076:
2052:
2024:
2004:
1984:
1924:
1892:
1863:
1830:
1810:
1742:
1679:
1623:
1586:
1566:
1510:
1490:
1455:
1420:
1370:
1320:
1287:
1267:
1257:the evaluation of
1247:
1227:
1207:
1137:circuit complexity
1023:
991:
976:
955:
920:
885:
861:bounded arithmetic
855:Bounded arithmetic
849:Bounded arithmetic
786:
727:
703:
683:
659:
643:weakly automatable
627:
603:
583:
559:
531:(Automatability)
462:A proof system is
321:
278:
258:
221:
201:
132:accepts the pair (
100:bounded arithmetic
88:Mathematical logic
3601:978-0-521-51729-4
2928:978-0-521-51729-4
2892:978-3-540-15236-1
2855:. pp. 83–97.
2603:10.1137/06066850X
2163:, in particular,
1820:stating that `if
1589:{\displaystyle C}
1513:{\displaystyle y}
1330:, such that both
1290:{\displaystyle B}
1270:{\displaystyle A}
1250:{\displaystyle y}
1230:{\displaystyle y}
281:{\displaystyle n}
261:{\displaystyle c}
231:is a tautology'.
3730:
3693:Proof Complexity
3682:
3656:Proof Complexity
3651:
3636:
3626:
3612:
3575:
3547:Pitassi, Toniann
3532:
3531:
3529:
3520:(2–3): 194–205.
3502:
3496:
3495:
3472:
3466:
3465:
3434:
3428:
3427:
3400:Pitassi, Toniann
3392:
3386:
3385:
3376:(6): 1939–1967.
3362:Pitassi, Toniann
3354:
3348:
3347:
3345:
3325:
3323:
3322:
3317:
3314:
3309:
3285:
3279:
3278:
3239:
3233:
3232:
3193:
3184:
3183:
3147:
3138:
3137:
3101:
3095:
3094:
3059:Pitassi, Toniann
3055:
3049:
3048:
3020:
3014:
3013:
3002:
2996:
2995:
2970:
2964:
2963:
2952:
2946:
2940:
2903:
2897:
2896:
2863:
2857:
2856:
2845:
2839:
2838:
2823:
2814:
2813:
2806:Pitassi, Toniann
2798:
2792:
2791:
2789:
2767:
2761:
2760:
2754:
2746:
2718:
2702:
2696:
2695:
2685:
2679:
2678:
2671:Atserias, Albert
2667:
2661:
2660:
2650:
2644:
2643:
2613:
2607:
2606:
2597:(4): 1347–1363.
2586:
2580:
2579:
2550:Pitassi, Toniann
2542:
2536:
2535:
2526:(6): 1939–1967.
2512:Pitassi, Toniann
2504:
2498:
2497:
2495:
2473:
2471:
2470:
2465:
2462:
2457:
2433:
2427:
2426:
2417:(6): 1939–1967.
2401:Pitassi, Toniann
2393:
2387:
2386:
2380:
2372:Santhanam, Rahul
2368:Pitassi, Toniann
2364:
2358:
2357:
2332:(3): 1063–1079.
2317:
2311:
2310:
2307:Proof complexity
2302:
2296:
2295:
2287:
2281:
2280:
2239:
2145:
2143:
2142:
2137:
2135:
2134:
2090:witnessing that
2085:
2083:
2082:
2077:
2061:
2059:
2058:
2053:
2033:
2031:
2030:
2025:
2013:
2011:
2010:
2005:
1993:
1991:
1990:
1985:
1962:
1961:
1956:
1933:
1931:
1930:
1925:
1901:
1899:
1898:
1893:
1872:
1870:
1869:
1864:
1839:
1837:
1836:
1831:
1819:
1817:
1816:
1811:
1788:
1787:
1782:
1751:
1749:
1748:
1743:
1688:
1686:
1685:
1680:
1632:
1630:
1629:
1624:
1600:is said to have
1595:
1593:
1592:
1587:
1575:
1573:
1572:
1567:
1519:
1517:
1516:
1511:
1499:
1497:
1496:
1491:
1464:
1462:
1461:
1456:
1429:
1427:
1426:
1421:
1379:
1377:
1376:
1371:
1329:
1327:
1326:
1321:
1296:
1294:
1293:
1288:
1276:
1274:
1273:
1268:
1256:
1254:
1253:
1248:
1236:
1234:
1233:
1228:
1216:
1214:
1213:
1208:
1135:lower bounds in
1032:
1030:
1029:
1024:
1022:
1021:
1016:
1000:
998:
997:
992:
989:
984:
964:
962:
961:
956:
954:
953:
948:
947:
929:
927:
926:
921:
919:
918:
913:
894:
892:
891:
886:
884:
883:
878:
795:
793:
792:
787:
785:
784:
736:
734:
733:
728:
712:
710:
709:
704:
692:
690:
689:
684:
668:
666:
665:
660:
636:
634:
633:
628:
612:
610:
609:
604:
592:
590:
589:
584:
568:
566:
565:
560:
516:Extended Frege.
330:
328:
327:
322:
320:
319:
287:
285:
284:
279:
267:
265:
264:
259:
230:
228:
227:
222:
210:
208:
207:
202:
173:sequent calculus
168:is a tautology.
96:Peano arithmetic
34:proof complexity
3738:
3737:
3733:
3732:
3731:
3729:
3728:
3727:
3703:
3702:
3689:
3654:KrajĂÄŤek, Jan,
3634:
3615:draft from 2008
3602:
3541:
3539:Further reading
3536:
3535:
3503:
3499:
3473:
3469:
3435:
3431:
3393:
3389:
3355:
3351:
3310:
3305:
3299:
3296:
3295:
3288:KrajĂÄŤek, Jan;
3286:
3282:
3259:10.2307/2275583
3240:
3236:
3213:10.2307/2275583
3194:
3187:
3164:10.2307/2275541
3148:
3141:
3118:10.2307/2275250
3102:
3098:
3056:
3052:
3023:KrajĂÄŤek, Jan;
3021:
3017:
3003:
2999:
2971:
2967:
2953:
2949:
2943:draft from 2008
2929:
2904:
2900:
2893:
2864:
2860:
2846:
2842:
2827:Ben-Sasson, Eli
2824:
2817:
2799:
2795:
2768:
2764:
2748:
2747:
2735:
2703:
2699:
2686:
2682:
2668:
2664:
2651:
2647:
2614:
2610:
2587:
2583:
2543:
2539:
2505:
2501:
2458:
2453:
2447:
2444:
2443:
2436:KrajĂÄŤek, Jan;
2434:
2430:
2394:
2390:
2378:
2365:
2361:
2338:10.2307/2274765
2320:KrajĂÄŤek, Jan;
2318:
2314:
2303:
2299:
2288:
2284:
2261:10.2307/2273702
2240:
2236:
2231:
2218:NP (complexity)
2184:
2157:
2130:
2126:
2121:
2118:
2117:
2071:
2068:
2067:
2062:admits a short
2047:
2044:
2043:
2019:
2016:
2015:
1999:
1996:
1995:
1957:
1946:
1945:
1943:
1940:
1939:
1907:
1904:
1903:
1878:
1875:
1874:
1849:
1846:
1845:
1825:
1822:
1821:
1783:
1772:
1771:
1769:
1766:
1765:
1701:
1698:
1697:
1638:
1635:
1634:
1609:
1606:
1605:
1581:
1578:
1577:
1525:
1522:
1521:
1505:
1502:
1501:
1470:
1467:
1466:
1465:is false or if
1435:
1432:
1431:
1385:
1382:
1381:
1335:
1332:
1331:
1306:
1303:
1302:
1282:
1279:
1278:
1262:
1259:
1258:
1242:
1239:
1238:
1222:
1219:
1218:
1166:
1163:
1162:
1159:
1121:
1096:
1090:
1078:model-theoretic
1017:
1009:
1008:
1006:
1003:
1002:
985:
980:
974:
971:
970:
949:
940:
939:
938:
936:
933:
932:
914:
903:
902:
900:
897:
896:
879:
871:
870:
868:
865:
864:
857:
851:
810:Nullstellensatz
780:
776:
771:
768:
767:
722:
719:
718:
698:
695:
694:
678:
675:
674:
654:
651:
650:
622:
619:
618:
598:
595:
594:
578:
575:
574:
554:
551:
550:
541:A proof system
522:
424:of a tautology
408:a proof system
361:a proof system
352:
338:(NP vs. coNP)
315:
311:
297:
294:
293:
292:-proof of size
273:
270:
269:
253:
250:
249:
237:
216:
213:
212:
196:
193:
192:
114:
108:
12:
11:
5:
3736:
3726:
3725:
3720:
3715:
3701:
3700:
3695:
3688:
3687:External links
3685:
3684:
3683:
3659:
3652:
3627:
3618:
3600:
3576:
3540:
3537:
3534:
3533:
3497:
3467:
3448:(3): 941–958.
3429:
3410:(1–2): 47–68.
3387:
3349:
3313:
3308:
3304:
3280:
3234:
3207:(3): 981–998.
3185:
3139:
3096:
3050:
3015:
2997:
2965:
2947:
2927:
2898:
2891:
2858:
2840:
2831:Wigderson, Avi
2815:
2793:
2762:
2733:
2697:
2680:
2662:
2645:
2626:(2): 491–506.
2608:
2581:
2562:(1–2): 47–68.
2537:
2499:
2461:
2456:
2452:
2428:
2388:
2359:
2312:
2297:
2282:
2233:
2232:
2230:
2227:
2226:
2225:
2220:
2215:
2210:
2205:
2200:
2195:
2190:
2183:
2180:
2165:intuitionistic
2156:
2153:
2152:
2151:
2147:
2133:
2129:
2125:
2114:
2075:
2051:
2023:
2003:
1983:
1980:
1977:
1974:
1971:
1968:
1965:
1960:
1955:
1952:
1949:
1923:
1920:
1917:
1914:
1911:
1902:holds'. Here,
1891:
1888:
1885:
1882:
1862:
1859:
1856:
1853:
1829:
1809:
1806:
1803:
1800:
1797:
1794:
1791:
1786:
1781:
1778:
1775:
1741:
1738:
1735:
1732:
1729:
1726:
1723:
1720:
1717:
1714:
1711:
1708:
1705:
1678:
1675:
1672:
1669:
1666:
1663:
1660:
1657:
1654:
1651:
1648:
1645:
1642:
1622:
1619:
1616:
1613:
1585:
1565:
1562:
1559:
1556:
1553:
1550:
1547:
1544:
1541:
1538:
1535:
1532:
1529:
1509:
1489:
1486:
1483:
1480:
1477:
1474:
1454:
1451:
1448:
1445:
1442:
1439:
1419:
1416:
1413:
1410:
1407:
1404:
1401:
1398:
1395:
1392:
1389:
1369:
1366:
1363:
1360:
1357:
1354:
1351:
1348:
1345:
1342:
1339:
1319:
1316:
1313:
1310:
1286:
1266:
1246:
1226:
1206:
1203:
1200:
1197:
1194:
1191:
1188:
1185:
1182:
1179:
1176:
1173:
1170:
1158:
1155:
1151:
1150:
1146:
1143:
1140:
1128:
1120:
1117:
1108:DPLL algorithm
1089:
1086:
1020:
1015:
1012:
988:
983:
979:
952:
946:
943:
917:
912:
909:
906:
882:
877:
874:
853:Main article:
850:
847:
846:
845:
835:
834:
822:
802:
783:
779:
775:
753:
726:
702:
682:
658:
626:
602:
582:
558:
521:
518:
494:Extended Frege
481:(Optimality)
351:
348:
318:
314:
310:
307:
304:
301:
277:
257:
236:
233:
220:
200:
181:cutting planes
140:) we say that
110:Main article:
107:
104:
58:Robert Reckhow
9:
6:
4:
3:
2:
3735:
3724:
3721:
3719:
3716:
3714:
3711:
3710:
3708:
3699:
3696:
3694:
3691:
3690:
3681:
3677:
3673:
3669:
3665:
3660:
3657:
3653:
3650:
3646:
3642:
3641:
3633:
3628:
3624:
3619:
3616:
3611:
3607:
3603:
3597:
3593:
3589:
3585:
3581:
3580:Cook, Stephen
3577:
3574:
3570:
3566:
3562:
3558:
3554:
3553:
3548:
3545:Beame, Paul;
3543:
3542:
3528:
3523:
3519:
3515:
3511:
3507:
3506:Hrubeš, Pavel
3501:
3493:
3489:
3485:
3481:
3477:
3476:Hrubeš, Pavel
3471:
3463:
3459:
3455:
3451:
3447:
3443:
3439:
3438:Hrubeš, Pavel
3433:
3425:
3421:
3417:
3413:
3409:
3405:
3401:
3397:
3391:
3383:
3379:
3375:
3371:
3367:
3363:
3359:
3353:
3344:
3339:
3335:
3331:
3327:
3311:
3306:
3302:
3291:
3290:Pudlák, Pavel
3284:
3276:
3272:
3268:
3264:
3260:
3256:
3252:
3248:
3244:
3243:Pudlák, Pavel
3238:
3230:
3226:
3222:
3218:
3214:
3210:
3206:
3202:
3198:
3197:Pudlák, Pavel
3192:
3190:
3181:
3177:
3173:
3169:
3165:
3161:
3157:
3153:
3146:
3144:
3135:
3131:
3127:
3123:
3119:
3115:
3111:
3107:
3100:
3092:
3088:
3084:
3080:
3077:(2): 97–308.
3076:
3072:
3068:
3064:
3060:
3054:
3046:
3042:
3038:
3034:
3030:
3026:
3025:Pudlák, Pavel
3019:
3011:
3007:
3001:
2993:
2989:
2985:
2981:
2980:
2975:
2969:
2961:
2957:
2951:
2944:
2938:
2934:
2930:
2924:
2920:
2916:
2912:
2908:
2907:Cook, Stephen
2902:
2894:
2888:
2884:
2880:
2876:
2872:
2868:
2862:
2854:
2850:
2849:Cook, Stephen
2844:
2836:
2832:
2828:
2822:
2820:
2811:
2807:
2803:
2797:
2788:
2783:
2779:
2778:
2773:
2766:
2758:
2752:
2744:
2740:
2736:
2734:9781450369794
2730:
2726:
2722:
2717:
2712:
2708:
2701:
2693:
2692:
2684:
2676:
2672:
2666:
2658:
2657:
2649:
2641:
2637:
2633:
2629:
2625:
2621:
2620:
2612:
2604:
2600:
2596:
2592:
2585:
2577:
2573:
2569:
2565:
2561:
2557:
2556:
2551:
2547:
2541:
2533:
2529:
2525:
2521:
2517:
2513:
2509:
2503:
2494:
2489:
2485:
2481:
2480:
2475:
2459:
2454:
2450:
2439:
2438:Pudlák, Pavel
2432:
2424:
2420:
2416:
2412:
2411:
2406:
2402:
2398:
2392:
2384:
2377:
2373:
2369:
2363:
2355:
2351:
2347:
2343:
2339:
2335:
2331:
2327:
2323:
2322:Pudlák, Pavel
2316:
2308:
2301:
2293:
2286:
2278:
2274:
2270:
2266:
2262:
2258:
2254:
2250:
2249:
2244:
2243:Cook, Stephen
2238:
2234:
2224:
2221:
2219:
2216:
2214:
2211:
2209:
2206:
2204:
2201:
2199:
2196:
2194:
2191:
2189:
2186:
2185:
2179:
2176:
2174:
2170:
2166:
2162:
2148:
2131:
2127:
2123:
2115:
2112:
2111:
2110:
2107:
2105:
2101:
2098:implies that
2097:
2093:
2089:
2073:
2065:
2049:
2041:
2037:
2021:
2001:
1978:
1975:
1972:
1969:
1966:
1958:
1937:
1921:
1918:
1915:
1912:
1909:
1886:
1880:
1857:
1851:
1843:
1827:
1804:
1801:
1798:
1795:
1792:
1784:
1763:
1757:
1754:
1736:
1733:
1730:
1724:
1715:
1712:
1709:
1703:
1694:
1692:
1673:
1670:
1667:
1661:
1652:
1649:
1646:
1640:
1617:
1611:
1603:
1599:
1583:
1560:
1557:
1554:
1548:
1539:
1536:
1533:
1527:
1507:
1484:
1481:
1478:
1472:
1449:
1446:
1443:
1437:
1414:
1411:
1408:
1402:
1393:
1387:
1364:
1358:
1349:
1346:
1343:
1337:
1314:
1308:
1300:
1284:
1264:
1244:
1224:
1201:
1198:
1195:
1189:
1180:
1177:
1174:
1168:
1154:
1147:
1144:
1141:
1138:
1134:
1129:
1126:
1125:
1124:
1116:
1114:
1109:
1105:
1101:
1095:
1085:
1083:
1079:
1075:
1071:
1067:
1063:
1057:
1055:
1051:
1047:
1042:
1040:
1036:
1018:
986:
981:
967:
965:
950:
915:
880:
862:
856:
843:
842:
841:
838:
832:
828:
823:
820:
817:assuming the
816:
811:
807:
803:
799:
781:
777:
773:
765:
761:
757:
754:
751:
747:
743:
742:
741:
738:
724:
716:
700:
680:
672:
656:
648:
644:
640:
624:
616:
600:
580:
572:
556:
548:
544:
539:
535:
532:
530:
525:
517:
515:
509:
507:
503:
499:
495:
491:
485:
482:
480:
475:
473:
469:
465:
460:
457:
455:
451:
448:| is at most
447:
443:
439:
435:
431:
428:, there is a
427:
423:
419:
415:
411:
407:
404:
400:
396:
392:
388:
384:
380:
376:
372:
368:
364:
360:
357:
347:
342:
339:
337:
332:
316:
308:
305:
302:
291:
275:
255:
247:
243:
232:
218:
198:
190:
186:
185:Frege systems
182:
178:
174:
169:
167:
163:
159:
155:
151:
147:
143:
139:
135:
131:
127:
123:
119:
113:
106:Proof systems
103:
101:
97:
93:
89:
85:
83:
78:
73:
71:
67:
63:
59:
55:
50:
48:
44:
40:
35:
31:
27:
23:
19:
3663:
3638:
3622:
3583:
3556:
3550:
3517:
3513:
3500:
3486:(1): 72–90.
3483:
3479:
3470:
3445:
3441:
3432:
3407:
3403:
3390:
3373:
3369:
3352:
3336:(1): 82–94.
3333:
3329:
3283:
3250:
3246:
3237:
3204:
3200:
3158:(2): 69–83.
3155:
3151:
3112:(1): 73–86.
3109:
3105:
3099:
3074:
3070:
3053:
3039:(1): 15–39.
3036:
3032:
3018:
3009:
3000:
2983:
2977:
2968:
2959:
2950:
2910:
2901:
2874:
2871:Wilkie, Alex
2861:
2852:
2843:
2834:
2809:
2796:
2775:
2771:
2765:
2706:
2700:
2689:
2683:
2674:
2665:
2654:
2648:
2623:
2617:
2611:
2594:
2590:
2584:
2559:
2553:
2540:
2523:
2519:
2502:
2486:(1): 82–94.
2483:
2477:
2431:
2414:
2408:
2391:
2382:
2362:
2329:
2325:
2315:
2306:
2300:
2291:
2285:
2255:(1): 36–50.
2252:
2246:
2237:
2208:Proof theory
2177:
2158:
2108:
2103:
2099:
2095:
2091:
2087:
2063:
2039:
2035:
1935:
1841:
1761:
1758:
1755:
1695:
1690:
1601:
1597:
1298:
1160:
1152:
1122:
1119:Lower bounds
1103:
1099:
1097:
1073:
1069:
1068:of a theory
1061:
1058:
1046:second-order
1043:
1038:
1034:
968:
930:formalizing
858:
839:
836:
826:
739:
714:
670:
646:
642:
638:
614:
570:
546:
542:
540:
537:
533:
528:
527:
523:
513:
510:
497:
489:
487:
483:
478:
477:
471:
467:
463:
461:
458:
453:
449:
445:
441:
437:
433:
429:
425:
421:
417:
413:
409:
405:
402:
399:p-equivalent
398:
394:
390:
386:
385:p-simulates
382:
378:
377:p-simulates
374:
370:
366:
362:
358:
355:
353:
344:
340:
335:
334:
289:
245:
241:
238:
170:
165:
161:
157:
153:
149:
145:
141:
137:
133:
129:
125:
121:
117:
115:
86:
74:
54:Stephen Cook
51:
45:, the usual
43:Frege system
33:
26:proof theory
15:
3396:Bonet, M.L.
3358:Bonet, M.L.
3253:: 323–339.
3063:Beame, Paul
3029:Woods, Alan
2986:: 297–308.
2867:Paris, Jeff
2802:Beame, Paul
2546:Bonet, M.L.
2508:Bonet, M.L.
2397:Bonet, M.L.
1938:-proofs of
1299:interpolant
1088:SAT solvers
1084:'s method.
1054:Alex Wilkie
966:reasoning.
833:Resolution.
669:outputs an
547:automatable
359:p-simulates
82:SAT solving
3707:Categories
2812:: 274–282.
2787:2003.10230
2716:2004.08037
2385:: 370–382.
2229:References
1094:SAT solver
1092:See also:
1050:Jeff Paris
717:-proof of
673:-proof of
617:-proof of
573:-proof of
569:outputs a
177:resolution
148:-proof of
77:algorithms
68:(and thus
3559:: 66–89,
3006:Ajtai, M.
2974:Haken, A.
2956:Ajtai, M.
2751:cite book
2743:215814356
2074:π
2050:ϕ
2022:ϕ
2002:π
1973:ϕ
1967:π
1916:ϕ
1910:π
1881:ϕ
1852:ϕ
1828:π
1799:ϕ
1793:π
1722:→
1659:→
1546:→
1400:→
1356:→
1187:→
978:Π
725:τ
701:τ
681:τ
657:τ
625:τ
601:τ
581:τ
557:τ
464:p-optimal
406:simulates
219:τ
199:τ
3573:TR98-067
3508:(2009).
3366:Raz, Ran
3292:(1998).
3180:28517300
3134:44670202
2640:11602606
2516:Raz, Ran
2440:(1998).
2405:Raz, Ran
2374:(2010).
2354:15093234
2182:See also
1301:circuit
1111:such as
3680:1640332
3649:2185746
3610:2589550
3565:1650939
3462:1743011
3424:1360759
3326:and EF"
3275:8450089
3267:2275583
3229:8450089
3221:2275583
3172:2275541
3126:2275250
3091:1046674
2937:2589550
2576:1360759
2474:and EF"
2346:2274765
2277:2187041
2269:2273702
2066:-proof
760:Pitassi
529:Problem
479:Problem
472:optimal
432:-proof
420:-proof
336:Problem
240:system
3678:
3647:
3608:
3598:
3571:
3563:
3460:
3422:
3273:
3265:
3227:
3219:
3178:
3170:
3132:
3124:
3089:
2935:
2925:
2889:
2741:
2731:
2638:
2574:
2352:
2344:
2275:
2267:
2171:, and
1149:bound.
1066:models
750:P/poly
466:if it
288:has a
160:has a
3635:(PDF)
3458:S2CID
3420:S2CID
3271:S2CID
3263:JSTOR
3225:S2CID
3217:JSTOR
3176:S2CID
3168:JSTOR
3130:S2CID
3122:JSTOR
3087:S2CID
2782:arXiv
2739:S2CID
2711:arXiv
2656:ICALP
2636:S2CID
2572:S2CID
2379:(PDF)
2350:S2CID
2342:JSTOR
2273:S2CID
2265:JSTOR
2169:modal
2150:time.
1873:then
1840:is a
1082:Ajtai
806:FPT=W
801:time.
756:Bonet
144:is a
64:from
18:logic
3596:ISBN
3569:ECCC
2923:ISBN
2887:ISBN
2777:ECCC
2757:link
2729:ISBN
2691:ECCC
2223:coNP
2014:and
1380:and
1277:and
1113:CDCL
1052:and
762:and
456:|).
397:are
393:and
381:and
183:and
66:coNP
56:and
28:and
20:and
3668:doi
3588:doi
3522:doi
3518:157
3488:doi
3484:146
3450:doi
3412:doi
3378:doi
3338:doi
3334:140
3255:doi
3251:295
3209:doi
3160:doi
3114:doi
3079:doi
3041:doi
2988:doi
2915:doi
2879:doi
2721:doi
2628:doi
2599:doi
2564:doi
2528:doi
2488:doi
2484:140
2419:doi
2383:ICS
2334:doi
2257:doi
1689:in
831:DNF
764:Raz
746:RSA
641:is
545:is
508:).
444:, |
436:of
244:is
189:ZFC
16:In
3709::
3676:MR
3674:,
3645:MR
3606:MR
3604:,
3594:,
3567:,
3561:MR
3557:65
3555:,
3516:.
3512:.
3482:.
3456:.
3446:72
3444:.
3418:.
3408:13
3406:.
3374:29
3372:.
3364:;
3360:;
3332:.
3328:.
3269:.
3261:.
3249:.
3223:.
3215:.
3205:62
3203:.
3188:^
3174:.
3166:.
3156:62
3154:.
3142:^
3128:.
3120:.
3110:59
3108:.
3085:.
3073:.
3065:;
3061:;
3035:.
3027:;
2984:39
2982:.
2933:MR
2931:.
2921:.
2885:.
2869:;
2829:;
2818:^
2804:;
2780:.
2753:}}
2749:{{
2737:.
2727:.
2719:.
2634:.
2624:47
2622:.
2595:38
2593:.
2570:.
2560:13
2558:.
2524:29
2522:.
2514:;
2510:;
2482:.
2476:.
2415:29
2413:.
2403:;
2399:;
2381:.
2370:;
2348:.
2340:.
2330:54
2328:.
2271:.
2263:.
2253:44
2251:.
2175:.
2167:,
1133:AC
758:,
737:.
506:NE
452:(|
179:,
175:,
152:.
84:.
62:NP
32:,
3670::
3617:)
3613:(
3590::
3530:.
3524::
3494:.
3490::
3464:.
3452::
3426:.
3414::
3384:.
3380::
3346:.
3340::
3312:1
3307:2
3303:S
3277:.
3257::
3231:.
3211::
3182:.
3162::
3136:.
3116::
3093:.
3081::
3075:3
3047:.
3043::
3037:7
2994:.
2990::
2945:)
2941:(
2939:.
2917::
2895:.
2881::
2790:.
2784::
2772:k
2759:)
2745:.
2723::
2713::
2694:.
2659:.
2642:.
2630::
2605:.
2601::
2578:.
2566::
2534:.
2530::
2496:.
2490::
2460:1
2455:2
2451:S
2425:.
2421::
2356:.
2336::
2279:.
2259::
2132:0
2128:C
2124:T
2104:P
2100:P
2096:P
2092:P
2088:R
2064:P
2040:P
2036:P
1982:)
1979:x
1976:,
1970:,
1964:(
1959:P
1954:f
1951:e
1948:R
1936:P
1922:x
1919:,
1913:,
1890:)
1887:x
1884:(
1861:)
1858:x
1855:(
1842:P
1808:)
1805:x
1802:,
1796:,
1790:(
1785:P
1780:f
1777:e
1774:R
1762:P
1740:)
1737:z
1734:,
1731:y
1728:(
1725:B
1719:)
1716:y
1713:,
1710:x
1707:(
1704:A
1691:P
1677:)
1674:z
1671:,
1668:y
1665:(
1662:B
1656:)
1653:y
1650:,
1647:x
1644:(
1641:A
1621:)
1618:y
1615:(
1612:C
1598:P
1584:C
1564:)
1561:z
1558:,
1555:y
1552:(
1549:B
1543:)
1540:y
1537:,
1534:x
1531:(
1528:A
1508:y
1488:)
1485:z
1482:,
1479:y
1476:(
1473:B
1453:)
1450:y
1447:,
1444:x
1441:(
1438:A
1418:)
1415:z
1412:,
1409:y
1406:(
1403:B
1397:)
1394:y
1391:(
1388:C
1368:)
1365:y
1362:(
1359:C
1353:)
1350:y
1347:,
1344:x
1341:(
1338:A
1318:)
1315:y
1312:(
1309:C
1285:B
1265:A
1245:y
1225:y
1205:)
1202:z
1199:,
1196:y
1193:(
1190:B
1184:)
1181:y
1178:,
1175:x
1172:(
1169:A
1139:.
1104:P
1100:P
1074:P
1070:T
1062:P
1039:P
1035:P
1019:1
1014:V
1011:P
987:b
982:1
951:1
945:C
942:N
916:1
911:C
908:N
905:V
881:1
876:V
873:P
829:-
827:k
821:.
782:0
778:C
774:T
752:.
715:P
671:R
647:R
639:P
615:P
571:P
543:P
504:=
502:E
498:P
490:P
468:p
454:x
450:p
446:y
442:y
438:A
434:y
430:P
426:A
422:x
418:Q
414:p
410:Q
403:P
395:Q
391:P
387:P
383:Q
379:Q
375:P
371:P
367:Q
363:Q
356:P
317:c
313:)
309:c
306:+
303:n
300:(
290:P
276:n
256:c
242:P
166:A
162:P
158:A
154:P
150:A
146:P
142:x
138:x
136:,
134:A
130:P
126:x
124:,
122:A
120:(
118:P
70:P
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.