Hostname: page-component-586b7cd67f-dlnhk Total loading time: 0 Render date: 2024-11-23T18:18:17.647Z Has data issue: false hasContentIssue false
  • English
  • Français

The Complexity of Propositional Proofs

Published online by Cambridge University Press:  15 January 2014

Nathan Segerlind
Nathan Segerlind*
Affiliation:
Department of Computer Science, Post Office Box 751, Portland State Univeristy, Portland, OR 97201, USA, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

Propositional proof complexity is the study of the sizes of propositional proofs, and more generally, the resources necessary to certify propositional tautologies. Questions about proof sizes have connections with computational complexity, theories of arithmetic, and satisfiability algorithms. This is article includes a broad survey of the field, and a technical exposition of some recently developed techniques for proving lower bounds on proof sizes.

Type
Articles
Information
Bulletin of Symbolic Logic , Volume 13 , Issue 4 , December 2007 , pp. 417 - 481
Copyright
Copyright © Association for Symbolic Logic 2007

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1] Achlioptas, D., Beame, P., and Molloy, M., Exponential lower bounds for DPLL below the satisfiability threshold, Proceedings of the fifteenth annual ACM-SIAM symposium on discrete algorithms, 2004, pp. 139–140.Google Scholar
[2] Achlioptas, D., A sharp threshold in proof complexity yields lower bounds for satisfiability search, Journal of Computer and System Sciences, vol. 68 (2004), no. 2, pp. 261–276.CrossRefGoogle Scholar
[3] Aguirre, A. and Vardi, M., Random 3-SAT and BDDs: The plot thickens further, Principles and practice of constraint programming, 2001, pp. 121–136.Google Scholar
[4] Aharonov, D. and Naveh, T., Quantum NP- a survey, Technical Report arXiv:quantph/02-210077, arXiv.org, 2002.Google Scholar
[5] Ajtai, M., Parity and the pigeonhole principle, Feasible mathematics (Buss, S. and Scott, P., editors), Progress in Computer Science and Applied Logic, vol. 9, Birkhauser, 1990, pp. 1–24.Google Scholar
[6] Ajtai, M., The complexity of the pigeonhole principle, Combinatorica, vol. 14 (1994), no. 4, pp. 417–433.Google Scholar
[7] Ajtai, M., The independence of the modulo p counting principles, Proceedings of the twenty-sixth annual ACM symposium on the theory of computing, 23–25 May 1994, pp. 402–411.Google Scholar
[8] Alekhnovich, M., Lower bounds for k-DNF resolution on random 3-CNFs, Proceedings of the thirty-seventh annual ACM symposium on the theory of computing, 2005, pp. 251–256.Google Scholar
[9] Alekhnovich, M., Arora, S., and Tourlakis, I., Towards strong nonapproximability results in the Lovász–Schrijver hierarchy, Proceedings of the thirty-seventh annual ACM symposium on theory of computing, 2005, pp. 294–303.Google Scholar
[10] Alekhnovich, M., Ben-Sasson, E., Razborov, A., and Wigderson, A., Space complexity in propositional calculus, SIAM Journal on Computing, vol. 31 (2002), no. 4, pp. 1184–1211.CrossRefGoogle Scholar
[11] Alekhnovich, M., Hirsch, E., and Itsykson, D., Exponential lower bounds for the running times of DPLL algorithms on satisfiable formulas, Journal of Automated Reasoning, vol. 35 (2005), no. 1–3, pp. 51–72.CrossRefGoogle Scholar
[12] Alekhnovich, M. and Razborov, A., Resolution is not automatizable unless W[P] is tractable, Proceedings of the forty-second annual symposium on foundations of computer science, 2001, pp. 210–219.Google Scholar
[13] Alekhnovich, M., Lower bounds for polynomial calculus: non-binomial case, Proceedings of the Steklov Institute of Mathematics, vol. 242 (2003), pp. 18–35.Google Scholar
[14] Aloul, F., Mneimneh, M., and Sakallah, K., ZBDD-based backtrack search SAT solver, Eleventh IEEE/ACM workshop on logic & synthesis, 2002, pp. 131–136.Google Scholar
[15] Aloul, F., Ramani, A., Markov, I., and Sakallah, K., Solving difficult instances of Boolean satisfiability in the presence of symmetry, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 22 (2003), no. 9, pp. 1117–1137.Google Scholar
[16] Aloul, F., Sakallah, K., and Markov, I., Efficient symmetry breaking for boolean satisfiability, IEEE Transactions on Computers, vol. 55 (2006), no. 5, pp. 541–558.Google Scholar
[17] Aloul, F. A., Ramani, A., Markov, I. L., and Sakallah, K. A., PBS: a pseudo-boolean solver and optimizer, Proceedings of the fifth international conference on theory and applications of satisfiability testing, 2002, pp. 346–353.Google Scholar
[18] Atserias, A., Improved bounds on the weak pigeonhole principle and infinitely many primes from weaker axioms, Theoretical Computer Science, vol. 295 (2003), no. 1–3, pp. 27–39.Google Scholar
[19] Atserias, A. and Bonet, M. L., On the automatizability of resolution and related propositional proof systems, Information and Computation, vol. 189 (2004), no. 2, pp. 182–201.Google Scholar
[20] Atserias, A., Bonet, M. L., and Esteban, J. L., Lower bounds for the weak pigeonhole principle beyond resolution, Information and Computation, vol. 176 (2002), pp. 136–152.Google Scholar
[21] Atserias, A. and Dalmau, V., A combinatorial characterization of resolution width, Proceedings of the eighteenth annual IEEE conference on computational complexity, 2003, pp. 239–247.Google Scholar
[22] Atserias, A., Kolaitis, P., and Vardi, M., Constraint propagation as a proof system, Tenth international conference on principles and practice of constraint programming, 2004, pp. 77–91.Google Scholar
[23] Avigad, J., Plausibly hard combinatorial tautologies, Proof complexity and feasible arithmetics, American Mathematical Society, 1997, pp. 1–12.Google Scholar
[24] Bayardo, R. and Schrag, R., Using CSP look-back techniques to solve exceptionally hard SAT instances, Proceedings of the second international conference on principles and practice of constraint programming, 1996, pp. 46–60.Google Scholar
[25] Beame, P., A switching lemma primer, Technical report, Department of Computer Science and Engineering, University of Washington, 1994.Google Scholar
[26] Beame, P., Proof complexity, Computational complexity theory (Rudich, S. and Wigderson, A., editors), IAS/Park City mathematics series, vol. 10, American Mathematical Society, 2004, pp. 199–246.Google Scholar
[27] Beame, P., Impagliazzo, R., Krejíček, J., Pitassi, T., and Pudlák, P., Lower bounds on Hilbert's Nullstellensatz and propositional proofs, Proceedings of the London Mathematical Society, vol. 73 (1996), no. 3, pp. 1–26.Google Scholar
[28] Beame, P., Impagliazzo, R., Pitassi, T., and Segerlind, N., Memoization and DPLL: Formula caching proof systems, Proceedings of the eighteenth IEEE conference on computational complexity, 2003, pp. 225–236.Google Scholar
[29] Beame, P., Karp, R., Pitassi, T., and Saks, M., The efficiency of resolution and davis–putnam procedures, SIAM Journal on Computation, vol. 31 (2002), no. 4, pp. 1048–1075.CrossRefGoogle Scholar
[30] Beame, P., Kautz, H., and Sabharwal, A., Towards understanding and harnessing the potential of clause learning, Journal of Artificial Intelligence Research, vol. 22 (2004), pp. 319–351.CrossRefGoogle Scholar
[31] Beame, P. and Pitassi, T., Propositional proof complexity: Past, present, and future, Current trends in theoretical computer science: Entering the 21st century (Paul, G., Rozenberg, G., and Salomaa, A., editors), World Scientific Publishing, 2001, pp. 42–70.Google Scholar
[32] Beame, P., Pitassi, T., and Segerlind, N., Lower bounds for Lovász–Schrijver systems and beyond follow from multiparty communication complexity, Proceedings of the thirty-second international colloquium on automata, languages, and programming, 2005, pp. 1176–1188.Google Scholar
[33] Beame, P. and Riis, S., More one the relative strength of counting principles, Proof complexity and feasible arithmetics (Beame, Paul and Buss, Sam, editors), American Mathematical Society, 1998, pp. 13–35.Google Scholar
[34] Bellantoni, S., Pitassi, T., and Urquhart, A., Approximation and small depth frege proofs, Proceedings of the sixth annual IEEE conference on structure in complexity theory, 1991, pp. 367–391.Google Scholar
[35] Ben-Sasson, E., Size space trade-offs for resolution, Proceedings of the thirty-fourth annual ACM symposium on theory of computing, 2002, pp. 563–572.Google Scholar
[36] Ben-Sasson, E. and Impagliazzo, R., Random CNFs are hard for the polynomial calculus, Fortieth annual IEEE symposium on foundations of computer science, 1999, pp. 415–421.Google Scholar
[37] Ben-Sasson, E., Impagliazzo, R., and Wigderson, A., Near optimal separation of tree-like and general resolution, Combinatorica, vol. 24 (2004), no. 4, pp. 585–603.CrossRefGoogle Scholar
[38] Ben-Sasson, E. and Wigderson, A., Short proofs are narrow—resolution made simple, Journal of the ACM, vol. 48 (2001), no. 2, pp. 149–169.Google Scholar
[39] Bennett, J. H., On spectra, Ph.D. thesis, Princeton University, 1962.Google Scholar
[40] Bonet, M. and Galesi, N., A study of proof search algorithms for resolution and polynomial calculus, Proceedings of the fortieth annual IEEE symposium on foundations of computer science, 1999, pp. 422–431.Google Scholar
[41] Bonet, M., Pitassi, T., and Raz, R., Lower bounds for cutting planes proofs with small coefficients, The Journal of Symbolic Logic, vol. 62 (1997), no. 3, pp. 708–728.Google Scholar
[42] Bonet, M., On interpolation and automatization for Frege systems, SIAM Journal on Computing, vol. 29 (2000), no. 6, pp. 1939–1967.Google Scholar
[43] Bonet, M. L., Domingo, C., Gavaldà, R., Maciel, A., and Pitassi, T., Non-automatizability of bounded-depth Frege proofs, Computational Complexity, vol. 131 (2004), no. 1–2, pp. 47–68.Google Scholar
[44] Bonet, M. L., Esteban, J. L., Galesi, N., and Johannsen, J., On the relative complexity of resolution refinements and cutting planes proof systems, SIAM Journal on Computation, vol. 30 (2000), no. 5, pp. 1462–1484.Google Scholar
[45] Boppana, R. and Sipser, M., The complexity of finite functions, Handbook of theoretical computer science, volume A, Elsevier and MIT Press, 1990.Google Scholar
[46] Bryant, R., Graph-based algorithms for boolean function manipulation, IEEE Transactions on Computers, vol. C-35 (1986), no. 8, pp. 677–691.Google Scholar
[47] Bryant, R., Symbolic boolean manipulation with ordered binary decision diagrams, ACM Computing Surveys, vol. 24 (1992), no. 3, pp. 293–318.Google Scholar
[48] Buresh-Oppenheim, J., Clegg, M., Impagliazzo, R., and Pitassi, T., Homogenization and the polynomial calculus, Computational Complexity, vol. 11 (2002), no. 3–4, pp. 91–108.Google Scholar
[49] Buresh-Oppenheim, J., Galesi, N., Hoory, S., Magen, A., and Pitassi, T., Rank bounds and integrality gaps for cutting planes procedures, Theory of Computing, vol. 2 (2006), pp. 65–90.Google Scholar
[50] Buss, S., Bounded arithmetic, Studies in Proof Theory, vol. 3, Bibliopolis, 1986.Google Scholar
[51] Buss, S., Polynomial size proofs of the propositional pigeonhole principle, The Journal of Symbolic Logic, vol. 52 (1987), no. 4, pp. 916–927.Google Scholar
[52] Buss, S., Propositional consistency proofs, Annals of Pure and Applied Logic, vol. 52 (1991), no. 1–2, pp. 3–29.Google Scholar
[53] Buss, S., Bounded arithmetic and propositional proof complexity, Logic and computation (Schwichtenberg, H., editor), Springer-Verlag, 1997, pp. 67–122.CrossRefGoogle Scholar
[54] Buss, S., Lower bounds on Nullstellensatz proofs via designs, Proof complexity and feasible arithmetics (Buss, S. and Beame, P., editors), American Mathematical Society, 1998, pp. 59–71.Google Scholar
[55] Buss, S., Bounded arithmetic, proof complexity and two papers of Parikh, Annals of Pure and Applied Logic, vol. 96 (1999), no. 1–3, pp. 43–55.Google Scholar
[56] Buss, S., Grigoriev, D., Impagliazzo, R., and Pitassi, T., Linear gaps between degrees for the polynomial calculus modulo distinct primes, Journal of Computer and System Sciences, vol. 62 (2001), pp. 267–289.Google Scholar
[57] Buss, S., Impagliazzo, R., Krajíček, J., Pudlák, P., Razborov, A., and Sgall, J., Proof complexity in algebraic systems and bounded depth Frege systems with modular counting, Computational Complexity, vol. 6 (1997), pp. 256–298.Google Scholar
[58] Buss, S. and Pitassi, T., Resolution and the weak pigeonhole principle, Proceedings of the eleventh internation workshop on computer science logic, 1997, pp. 149–156.Google Scholar
[59] Buss, S., Good degree bounds on Nullstellensatz refutations of the induction principle, Journal of Computer and System Sciences, vol. 57 (1998), pp. 162–171.Google Scholar
[60] Buss, S. and Turán, G., Resolution proofs of generalized pigeonhole principles, Theoretical Computer Science, vol. 62 (1988), no. 3, pp. 211–217.Google Scholar
[61] Chatalic, P. and Simon, L., Multi-resolution on compressed sets of clauses, Proceedings of the twelfth international conference on tools with artificial intelligence, 2000, pp. 2–10.Google Scholar
[62] Chatalic, P., ZRes: The old Davis–Putnam procedures meets ZBDDs, Proceedings of the seventeenth international conference on automated deduction, 2000, pp. 449–454.Google Scholar
[63] Chvátal, V., Edmonds polytopes and a hierarchy of combinatorial problems, Discrete Mathematics, vol. 306 (2006), no. 10–11, pp. 886–904, First appeared in volume 4 of same journal in 1973.Google Scholar
[64] Chvátal, V. and Szemerédi, E., Many hard examples for resolution, Journal of the ACM, vol. 35 (1988), no. 4, pp. 759–768.Google Scholar
[65] Clarke, E., Grumberg, O., and Peled, D., Model checking, MIT Press, 1999.Google Scholar
[66] Clegg, M., Edmonds, J., and Impagliazzo, R., Using the Groebner basis algorithm to find proofs of unsatisfiability, Proceedings of the twenty-eighth annual ACM symposium on the theory of computing, 1996, pp. 174–183.Google Scholar
[67] Clote, P. and Setzer, A., On PHP, st-connectivity and odd-charged graphs, Proof complexity and feasible mathematics, DIMACS Series in Discrete Mathematics and Computer Science, vol. 39, American Mathematical Society, 1998, pp. 93–118.Google Scholar
[68] Cook, S., Feasibly constructive proofs and the propositional calculus, Proceedings of the seventh annual ACM symposium on the theory of computing, 1975, pp. 107–116.Google Scholar
[69] Cook, S. and Reckhow, R., The relative efficiency of propositional proof systems, The Journal of Symbolic Logic, vol. 44 (1979), no. 1, pp. 36–50.CrossRefGoogle Scholar
[70] Dash, S., An exponential lower bound on the length of some classes of branch-and-cut proofs, Mathematics of Operations Research, vol. 30 (2005), no. 3, pp. 678–700.Google Scholar
[71] Davis, M. and Putnam, H., A computing procedure for quantification theory, Journal of the ACM, vol. 7 (1960), no. 1, pp. 201–215.Google Scholar
[72] Dixon, H. and Ginsberg, M., Combining satisfiability techniques from AI and OR, The Knowledge Engineering Review, vol. 15 (2000), no. 1, pp. 31–45.Google Scholar
[73] Dixon, H., Inference methods for a pseudo-boolean satisfiability solver, Proceedings of the eighteenth national conference on artificial intelligence, 2002, pp. 635–640.Google Scholar
[74] Dixon, H., Ginsberg, M., Hofer, D., Luks, E., and Parkes, A., Generalizing boolean satisfiability III: Implementation, Journal of Artificial Intelligence Research, vol. 23 (2005), pp. 441–531.Google Scholar
[75] Dixon, H., Ginsberg, M., Luks, E., and Parkes, A., Generalizing boolean satisfiability II: Theory, Journal of Artificial Intelligence Research, vol. 22 (2004), pp. 481–534.Google Scholar
[76] Dixon, H., Ginsberg, M., and Parkes, A., Generalizing boolean satisfiability I: Background and survey of existing work, Journal of Artificial Intelligence Research, vol. 21 (2004), pp. 193–243.Google Scholar
[77] Eén, N. and Sörensson, N., An extensible SAT-solver, Proceedings of SAT 2003, 2003.Google Scholar
[78] Esteban, J. L., Galesi, N., and Messner, J., On the complexity of resolution with bounded conjunctions, Theoretical Computer Science, vol. 321 (2004), no. 2.3, pp. 347–370.Google Scholar
[79] Esteban, J. L. and Torán, J., Space bounds for resolution, Information and Computation, vol. 171 (2001), no. 1, pp. 84–97.Google Scholar
[80] Feige, U., Relations between average case complexity and approximation complexity, Proceedings of the thiry-fourth annual ACM symposium on theory of computing, 2002, pp. 534–543.Google Scholar
[81] Friedgut, E., Sharp thresholds of graph properties and the k-SAT problem, Journal of the American Mathematical Society, vol. 12 (1999), pp. 1017–1054.Google Scholar
[82] Galesi, N. and Lauria, M., Extending polynomial calculus to k-DNF resolution, Technical Report 41, Electronic Colloquium on Computational Complexity, 2007.Google Scholar
[83] Goldberg, E. and Novikov, Y., Berkmin: A fast and robust SAT solver, Proceedings of date 2002, 2002.Google Scholar
[84] Goldreich, O. and Zuckerman, D., Another proof the BPP ⊆ PH (and more), Technical Report 45, Electronic Colloquium on Computational Complexity, 1997.Google Scholar
[85] Gomory, R. E., Outline of an algorithm for integer solutions to linear programs, Bulletin of the American Mathematical Society, vol. 64 (1958), pp. 275–278.Google Scholar
[86] Groote, J. F., Hiding propositional constants in BDDs, Formal Methods in System Design: an International Journal, vol. 8 (1996), no. 1, pp. 91–96.Google Scholar
[87] Haken, A., The intractability of resolution, Theoretical Computer Science, vol. 39 (1985), no. 2-3, pp. 297–308.Google Scholar
[88] Håstad, J., Almost optimal lower bounds for small depth circuits, Advances in computing research, vol. 5, JAI Press, 1989, pp. 143–170.Google Scholar
[89] Hertel, P. and Pitassi, T., An exponential time/space speedup for resolution, Technical Report TR07-046, Electronic Colloquium on Computational Complexity, 2007.Google Scholar
[90] Hoory, S., Linial, N., and Wigderson, A., Expander graphs and their applications, Bulletin of the American Mathematical Society, vol. 43 (2006), pp. 439–561.Google Scholar
[91] Huang, J. and Darwiche, A., Toward good elimination ordering for symbolic SAT solving, Proceedings of the sixteenth IEEE conference on tools with artificial intelligence, 2004, pp. 566–573.Google Scholar
[92] Impagliazzo, R., Pitassi, T., and Urquhart, A., Upper and lower bounds for tree-like cutting planes proofs, Ninth annual symposium on logic in computer science, 1994, pp. 220–228.Google Scholar
[93] Impagliazzo, R., Pudlák, P., and Sgall, J., Lower bounds for the polynomial calculus and the Groebner basis algorithm, Computational Complexity, vol. 8 (1999), no. 2, pp. 127–144.Google Scholar
[94] Impagliazzo, R. and Segerlind, N., Counting axioms do not polynomially simulate counting gates (extended abstract), Proceedings of the forty-second annual IEEE symposium on foundations of computer science, 2001, pp. 200–209.Google Scholar
[95] Impagliazzo, R., Constant-depth Frege systems with counting axioms polynomially simulate Nullstellensatz refutations, ACM Transactions on Computational Logic, vol. 7 (2006), no. 2, pp. 199–218.Google Scholar
[96] Itsykson, D. and Kojevnikov, A., Lower bounds on static Lovász–Schrijver calculus proofs for Tseitin tautologies, Zapiski Nauchnyh Seminarov POMI, vol. 340 (2006), pp. 10–32, In Russian. Preliminary version in English appeared in ICALP 2005.Google Scholar
[97] Kabanets, V., Derandomization: A brief overview, Bulletin of the European Association for Theoretical Computer Science, (2002), no. 76, pp. 88–103.Google Scholar
[98] Köbler, J., Messner, J., and Torán, J., Optimal proof systems imply complete sets for promise classes, Information and Computation, vol. 184 (2003), pp. 71–92.Google Scholar
[99] Krajíček, J., Lower bounds to the size of constant-depth propositional proofs, The Journal of Symbolic Logic, vol. 59 (1994), no. 1, pp. 73–86.Google Scholar
[100] Krajíček, J., Bounded arithmetic, propositional logic and complexity theory, Cambridge University Press, 1995.Google Scholar
[101] Krajíček, J., Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic, The Journal of Symbolic Logic, vol. 62 (1997), no. 2, pp. 457–486.Google Scholar
[102] Krajíček, J., On the weak pigeonhole principle, Fudamenta Mathematicae, vol. 170 (2001), pp. 123–140.Google Scholar
[103] Krajíček, J., An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams, Technical Report 7, Electronic Colloquium on Computational Complexity, 2007.Google Scholar
[104] Krajíček, J. and Pudlák, P., Propositional proof systems, the consistency of first-order theories, and the complexity of computations, The Journal of Symbolic Logic, vol. 54 (1989), no. 3, pp. 1063–1079.Google Scholar
[105] Krajíček, J. and Pudlák, P., Some consequences of cryptographical conjectures for and EF, Information and Computation, vol. 140 (1998), no. 1, pp. 82–94.Google Scholar
[106] Krajíček, J., Pudlák, P., and Woods, A., An exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle, Random Structures and Algorithms, vol. 7 (1995), no. 1, pp. 15–40.Google Scholar
[107] Lipton, R., Model theoretic aspects of computational complexity, Proceedings of the nineteenth annual IEEE symposium on foundations of computer science, 1978, pp. 193–200. Google Scholar
[108] Lovász, L. and Schrijver, A., Cones ofmatrics and set-functions and 0-1 optimization, SIAM Journal on Optimization, vol. 1 (1991), no. 2, pp. 166–190.Google Scholar
[109] Lynce, I. and Silva, J. Marques, An overview of backtrack search satisfiability algorithms, Annals of Mathematics and Artificial Intelligence, vol. 37 (2003), no. 3, pp. 307–326.Google Scholar
[110] Maciel, A., Pitassi, T., and Woods, A., A new proof of the weak pigeonhole principle, Journal of Computer and System Sciences, vol. 64 (2002), no. 3, pp. 843–872.Google Scholar
[111] Marques-Silva, J. and Sakallah, K., GRASP a new search algorithm for satisfiability, Proceedings of IEEE/ACM internation conference on computer-aided design, 1996.Google Scholar
[112] Martin, D., Logemann, G., and Loveland, D., A machine program for theorem proving, Communications of the ACM, vol. 5 (1962), no. 7, pp. 394–397.Google Scholar
[113] McDiarmid, C., Concentration, Probabilistic methods for algorithmic discrete mathematics (Habib, M., McDiarmid, C., Ramirez-Alfonsin, J., and Reed, B., editors), Algorithms and Combinatorics, vol. 16, Springer, 1998, pp. 195–248.Google Scholar
[114] McMillan, K., Symbolic model checking, Ph.D. thesis, Carnegie Mellon, 1992.Google Scholar
[115] McMillan, K., Interpolation and SAT-based model checking, Proceedings of fifteenth internation conference on computer aided verification, 2003, pp. 1–13.Google Scholar
[116] McMillan, K., Applications of Craig interpolants in model checking, Proceedings of eleventh international conference on tools and algorithms for construction and analysis of systems, 2005, pp. 1–12.Google Scholar
[117] Meinel, C. and Theobald, T., Algorithms and data structures in VLSI design, Springer-Verlag, 1998.Google Scholar
[118] Mitchell, D., Selman, B., and Levesque, H., Hard and easy distributions for SAT problems, Proceedings of the tenth national conference on artificial intelligence, 1992, pp. 459–465.Google Scholar
[119] Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., and Malik, S., Chaff: Engineering an efficient SAT solver, Proceedings of the thirty-eighth design automation conference, 2001, pp. 530–535.Google Scholar
[120] Motter, D. and Markov, I., A compressed breadth-first search for satisfiability, Fourth international workshop on algorithms engineering and experiments (ALENEX), 2002, pp. 29–42.Google Scholar
[121] Motter, D., Overcoming resolution-based lower bounds for SAT solvers, Eleventh IEEE/ACM workshop on logic and synthesis, 2002, pp. 373–378.Google Scholar
[122] Motter, D., Roy, J., and Markov, I., Resolution cannot polynomially simulate compressed-BFS, Annals of Mathematics and Artificial Intelligence, vol. 44 (2005), no. 1–2, pp. 121–156.Google Scholar
[123] Mundici, D., A lower bound for the complexity of Craig's interpolants in sentential logic, Archiv fur Math. Logik, vol. 23 (1983), pp. 27–36.Google Scholar
[124] Nordström, J., Narrow proofs may be spacious: Separating space and width in resolution, Proceedings of the thirty-eighth annual ACM symposium on theory of computing, 2006, pp. 507–516.Google Scholar
[125] Pan, G. and Vardi, M., Search vs. symbolic techniques in satisfiability solving, The seventh international conference on theory and applications of satisfiability testing, 2004.Google Scholar
[126] Parikh, R., Existence and feasibility in arithmetic, The Journal of Symbolic Logic, vol. 36 (1971), no. 3, pp. 494–508.Google Scholar
[127] Paris, J. and Wilkie, A., Counting problems in bounded arithmetic, Methods in mathematical logic, Lecture Notes in Mathematics, no. 1130, Springer-Verlag, 1985, pp. 317–340.Google Scholar
[128] Paris, J., Wilkie, A., and Woods, A., Provability of the pigeonhole principle and the existence of infinitely many primes, The Journal of Symbolic Logic, vol. 53 (1988), no. 4, pp. 1235–1244.CrossRefGoogle Scholar
[129] Pitassi, T., Algebraic propositional proof systems, Descriptive complexity and finite models (Immerman, Neil and Kolaitis, Phokion G., editors), DIMACS: Series in Discrete Mathematics and Theoretical Computer Science, vol. 31, American Mathematical Society, 1997.Google Scholar
[130] Pitassi, T., Beame, P., and Impagliazzo, R., Exponential lower bounds for the pigeonhole principle, Computational Complexity, vol. 3 (1993), pp. 97–140.Google Scholar
[131] Pitassi, T. and Raz, R., Regular resolution bounds for the weak pigeonhole principle, Combinatorica, vol. 24 (2004), no. 3, pp. 503–524.Google Scholar
[132] Pudlák, P., Lower bounds for resolution and cutting planes proofs and monotone computations, The Journal of Symbolic Logic, vol. 62 (1997), no. 3, pp. 981–998.Google Scholar
[133] Pudlák, P., On the complexity of propositional calculus, Sets and proofs: Invited papers from logic colloquium '97 (Cooper, S. Barry and Truss, J., editors), London Mathematical Society Lecture Note Series, vol. 258, Cambridge University Press, 1997, pp. 197–218.Google Scholar
[134] Pudlák, P. and Hajék, P., Metamathematics of first-order arithmetic, ASL Perspectives in Logic, Springer-Verlag, 1993.Google Scholar
[135] Pudlák, P. and Sgall, J., Algebraic models of computation and interpolation for algebraic proof systems, Proof complexity and feasible arithmetics (Buss, S. and Beame, P., editors), DIMACS Series in Discrete Mathematics, vol. 39, American Mathematical Society, 1998, pp. 279–295.Google Scholar
[136] Ragde, P. and Wigderson, A., Linear-size constant-depth polylog-threshold circuits, Information Processing Letters, vol. 39 (1991), no. 3, pp. 143–146.Google Scholar
[137] Raz, R., Resolution lower bounds for the weak pigeonhole principle, Journal of the ACM, vol. 51 (2004), no. 2, pp. 115–138.Google Scholar
[138] Razborov, A., On the method of approximations, Proceedings of the twenty first annual ACM symposium on theory of computing, 1989, pp. 167–176.Google Scholar
[139] Razborov, A., On provably disjoint NP pairs, Technical Report 6, Electronic Colloquium on Computational Complexity, 1994.Google Scholar
[140] Razborov, A., Unprovability of lower bounds on the circuit size in certain fragments of bounded arithmetic, Izvestiya of the Russian Academy of Science and Mathematics, vol. 59 (1995), no. 1, pp. 201–224.Google Scholar
[141] Razborov, A., Lower bounds for the polynomial calculus, Computational Complexity, vol. 7 (1998), no. 4, pp. 291–324.Google Scholar
[142] Razborov, A., Improved resolution lower bounds for theweak functional pigeonhole principle, Theoretical Computer Science, vol. 303 (2001), no. 1, pp. 233–243.Google Scholar
[143] Razborov, A., Improved resolution lower bounds for theweak pigeonhole principle, Technical Report 55, Electronic Colloquium on Computational Complexity, 2001.Google Scholar
[144] Razborov, A., Proof complexity of pigeonhole principles, Proceedings of the the fifth international conference on developments in language theory, Lecture Notes in Computer Science, no. 2295, 2001, pp. 100–116.Google Scholar
[145] Razborov, A., Pseudorandom generators hard for k-DNF resolution and polynomial calculus resolution, Submitted to the Journal of Glacial Refereeing. Manuscript available at http://genesis.mi.ras.ru/~razborov/, 2003.Google Scholar
[146] Razborov, A., Resolution lower bounds for perfectmatching principles, Journal of Computer and System Sciences, vol. 69 (2004), no. 1, pp. 3–27.Google Scholar
[147] Riis, S., Count(q) does not imply Count(p), Annals of Pure and Applied Logic, vol. 90 (1997), no. 1–3, pp. 1–56.CrossRefGoogle Scholar
[148] Sadowski, Z., On an optimal quantified propositional proof system and a complete language for NP⋂coNP, Proceedings of the eleventh international symposium on fundamentals of computing theory, 1997, pp. 423–428.Google Scholar
[149] Segerlind, N., New separations in propositional proof complexity, Ph.D. thesis, University of California, San Diego, August 2003.Google Scholar
[150] Segerlind, N., An exponential separation between Res(k) and Res(k + 1) for k ≤ ϵ log n, Information Processing Letters, vol. 93 (2005), no. 4, pp. 185–190.Google Scholar
[151] Segerlind, N., Nearly-exponential size lower bounds for symbolic quantifier elimination algorithms and OBDD-based proofs of unsatisfiability, Technical Report 9, Electronic Colloquium on Computational Complexity, 2007.Google Scholar
[152] Segerlind, N., Buss, S., and Impagliazzo, R., A switching lemma for small restrictions and lower bounds for k-DNF resolution, SIAM Journal of Computing, vol. 33 (2004), no. 5, pp. 1171–1200.Google Scholar
[153] Simpson, S., Subsystems of second-order arithmetic, Perspectives in Mathematical Logic, Springer-Verlag, 1999.Google Scholar
[154] Sinz, C. and Biere, A., Extended resolution proofs for conjoining BDDs, First international computer science symposium in Russia, 2006, pp. 600–611.Google Scholar
[155] Smolensky, R., Algebraic methods in the theory of lower bounds for Boolean circuit complexity, Proceedings of the nineteenth annual ACM symposium on theory of computing, 1987, pp. 77–82.Google Scholar
[156] Soltys, M. and Cook, S., The proof complexity of linear algebra, Annals of Pure and Applied Logic, vol. 130 (2004), no. 1–3, pp. 277–323.Google Scholar
[157] Stallman, R. M. and Sussman, G. J., Forward reasoning and dependency-directd backtracking in a system for computer-aided circuit analysis, Artificial Intelligence, vol. 9 (1977), pp. 135–196.Google Scholar
[158] Torán, J., Space and width in propositional resolution, Bulletin of the European Association of Theoretical Computer Science, vol. 83 (2004), pp. 86–104.Google Scholar
[159] Urquhart, A., The complexity of propositional proofs, this Bulletin, vol. 1 (1995), no. 4, pp. 425–467.Google Scholar
[160] Woods, A., Some problems in logic and number theory, and their connections, Ph.D. thesis, University of Manchester, 1981.Google Scholar
[161] Wrathall, C., Rudimentary predicates and relative computation, SIAM Journal on Computing, vol. 7 (1978), no. 2, pp. 149–209.Google Scholar