×

A finite-model-theoretic view on propositional proof complexity. (English) Zbl 1451.03023

Summary: We establish new, and surprisingly tight, connections between propositional proof complexity and finite model theory. Specifically, we show that the power of several propositional proof systems, such as Horn resolution, bounded-width resolution, and the polynomial calculus of bounded degree, can be characterised in a precise sense by variants of fixed-point logics that are of fundamental importance in descriptive complexity theory. Our main results are that Horn resolution has the same expressive power as least fixed-point logic, that bounded-width resolution captures existential least fixed-point logic, and that the polynomial calculus with bounded degree over the rationals solves precisely the problems definable in fixed-point logic with counting. By exploring these connections further, we establish finite-model-theoretic tools for proving lower bounds for the polynomial calculus over the rationals and over finite fields.

MSC:

03C13 Model theory of finite structures
03F20 Complexity of proofs
68Q19 Descriptive complexity and finite models
PDFBibTeX XMLCite
Full Text: arXiv

References:

[1] M. Anderson and A. Dawar. On symmetric circuits and fixed-point logics. Theory Comput. Syst., 60(3):521-551, 2017. · Zbl 1366.68047
[2] A. Atserias. On sufficient conditions for unsatisfiability of random formulas. J. ACM, 51(2):281-311, 2004. · Zbl 1316.68055
[3] A. Atserias, A. Bulatov, and A. Dawar. Affine systems of equations and counting infinitary logic. Theoretical Computer Science, 410:1666-1683, 2009. · Zbl 1168.68040
[4] A. Atserias and V. Dalmau. A combinatorial characterization of resolution width. Journal of Computer and System Sciences, 74(3):323-334, 2008. · Zbl 1133.03034
[5] A. Atserias and E. N. Maneva. Sherali-adams relaxations and indistinguishability in counting logics. In Innovations in Theoretical Computer Science 2012, Cambridge, MA, USA, January 8-10, 2012, pages 367-379. ACM, 2012. · Zbl 1347.68175
[6] A. Atserias and J. Ochremiak. Proof complexity meets algebra. In 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, volume 80 of LIPIcs, pages 110:1-110:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. · Zbl 1407.03070
[7] A. Atserias and J. Ochremiak. Definable ellipsoid method, sums-of-squares proofs, and the isomorphism problem. In Proceedings of LICS 2018, 2018.
[8] L. Barto and M. Kozik. Constraint satisfaction problems solvable by local consistency methods. J. ACM, · Zbl 1295.68126
[9] P. Beame and T. Pitassi. Propositional proof complexity: Past, present, and future. Current Trends in TCS: Entering the 21st Century, pages 42-70, 2001. · Zbl 1049.03040
[10] C. Berkholz and M. Grohe. Limitations of algebraic approaches to graph isomorphism testing. In Proceedings of ICALP 2015, pages 155-166, 2015. · Zbl 1410.68152
[11] C. Berkholz and M. Grohe. Linear diophantine equations, group CSPs, and graph isomorphism. In Proceedings of SODA 2017, pages 327-339, 2017. · Zbl 1410.68153
[12] A. A. Bulatov. A dichotomy theorem for nonuniform CSPs. In Proceedings of FOCS 2017, pages 319-330. IEEE Computer Society, 2017.
[13] J. Cai, M. F¨urer, and N. Immerman. An optimal lower bound on the number of variables for graph identification. Combinatorica, 12(4):389-410, 1992. · Zbl 0785.68043
[14] M. Clegg, J. Edmonds, and R. Impagliazzo. Using the Groebner Basis Algorithm to find Proofs of Unsatisfiability. In STOC 1996, pages 174-183, 1996. · Zbl 0938.68825
[15] S. Cook and R. Reckhow. The relative efficiency of propositional proof systems. J. Symbolic Logic, 44:36-50, 1979. · Zbl 0408.03044
[16] E. Dahlhaus. Skolem normal forms concerning the least fixpoint. In Computation Theory and Logic, In Memory of Dieter R¨odding, volume 270 of Lecture Notes in Computer Science, pages 101-106. Springer, 1987. · Zbl 0636.03033
[17] A. Dawar. The nature and power of fixed-point logic with counting. ACM SIGLOG News, 2(1):8-21, 2015.
[18] A. Dawar, M. Grohe, B. Holm, and B. Laubner. Logics with rank operators. In Proceedings of LICS 2009, pages 113-122, 2009.
[19] A. Dawar and P. Wang. A definability dichotomy for finite valued CSPs. In Proceedings of CSL 2015, volume 41 of LIPIcs, pages 60-77. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. · Zbl 1373.68264
[20] A. Dawar and P. Wang. Lasserre lower bounds and definability of semidefinite programming. CoRR, abs/1602.05409, 2016.
[21] A. Dawar and P. Wang. Definability of semidefinite programming and lasserre lower bounds for CSPs. In Proceedings of LICS 2017, pages 1-12. IEEE Computer Society, 2017.
[22] H.-D. Ebbinghaus and J. Flum. Finite Model Theory. 2nd edition, 1999. · Zbl 0932.03032
[23] T. Feder and M. Y. Vardi. The computational structure of monotone monadic SNP and constraint satisfaction: A study through datalog and group theory. SIAM J. Comput., 28(1):57-104, 1998. · Zbl 0914.68075
[24] E. Gr¨adel and S. Hegselmann. Counting in Team Semantics. In Proceedings of CSL 2016, 2016. · Zbl 1370.03044
[25] E. Gr¨adel, P. Kolaitis, L. Libkin, M. Marx, J. Spencer, M. Vardi, Y. Venema, and S. Weinstein. Finite Model Theory and Its Applications. 2007. · Zbl 1133.03001
[26] E. Gr¨adel and G. McColm. Hierarchies in Transitive Closure Logic, Stratified Datalog and Infinitary Logic. Annals of Pure and Applied Logic, 77:166-199, 1996. · Zbl 0856.03026
[27] E. Gr¨adel, B. Pago, and W. Pakusa. The model-theoretic expressiveness of propositional proof systems. In Proceedings of CSL 2017, volume 82 of LIPIcs, pages 27:1-27:18. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017.
[28] E. Gr¨adel and W. Pakusa. Rank logic is dead, long live rank logic! In Proceedings of CSL 2015, Leibniz International Proceedings in Informatics (LIPIcs), 2015. · Zbl 1373.03047
[29] M. Grohe and M. Otto. Pebble games and linear equations. J. Symb. Log., 80(3):797-844, 2015. · Zbl 1353.03018
[30] M. Grohe and W. Pakusa. Descriptive complexity of linear equation systems and applications to propositional proof complexity. In Proceedings of LICS 2017, pages 1-12. IEEE Computer Society, 2017.
[31] B. Holm. Descriptive Complexity of Linear Algebra. PhD thesis, University of Cambridge, 2010.
[32] S. Hoory, N. Linial, and A. Wigderson. Expander graphs and their applications. Bulletin of the American Mathematical Society, 43(4):439-561, 2006. · Zbl 1147.68608
[33] N. Immerman. Descriptive complexity. Graduate texts in computer science. Springer, 1999.
[34] R. Impagliazzo, P. Pudl´ak, and J. Sgall. Lower bounds for the polynomial calculus and the gr¨obner basis algorithm. Computational Complexity, 8(2):127-144, 1999. · Zbl 0946.68129
[35] P. G. Kolaitis. The expressive power of stratified programs. Inf. Comput., 90(1):50-66, 1991. · Zbl 0727.68016
[36] L. Libkin. Elements of Finite Model Theory. 2004. · Zbl 1060.03002
[37] P. N. Malkin. Sherali-adams relaxations of graph isomorphism polytopes. Discrete Optimization, 12:73-97, 2014. · Zbl 1308.90210
[38] W. Pakusa. Linear Equation Systems and the Search for a Logical Characterisation of Polynomial Time. PhD thesis, RWTH Aachen University, 2016.
[39] N. Segerlind. The Complexity of Propositional Proofs. Bulletin of Symbolic Logic, 13(04):417-481, 2007. · Zbl 1133.03037
[40] J. Tor´an. On the resolution complexity of graph non-isomorphism. In Proceedings of SAT 2013, volume 7962 of LNCS, pages 52-66, 2013.
[41] D. Zhuk. A proof of CSP dichotomy conjecture. In Proceedings of FOCS 2017, pages 331-342. IEEE Computer Society, 2017.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.