Proof Complexity Meets Algebra
We analyse how the standard reductions between constraint satisfaction problems affect their proof complexity. We show that, for the most studied propositional and semi-algebraic proof systems, the classical constructions of pp-interpretability, homomorphic equivalence and addition of constants to a core preserve the proof complexity of the CSP. As a result, for those proof systems, the classes of constraint languages for which small unsatisfiability certificates exist can be characterised algebraically. We illustrate our results by a gap theorem saying that a constraint language either has resolution refutations of bounded width, or does not have bounded-depth Frege refutations of subexponential size. The former holds exactly for the widely studied class of constraint languages of bounded width. This class is also known to coincide with the class of languages with Sums-of-Squares refutations of sublinear degree, a fact for which we provide an alternative proof. We hence ask for the existence of a natural proof system with good behaviour with respect to reductions and simultaneously small size refutations beyond bounded width. We give an example of such a proof system by showing that bounded-degree Lovasz-Schrijver satisfies both requirements.
Constraint Satisfaction Problem
Proof Complexity
Reductions
Gap Theorems
110:1-110:14
Regular Paper
Albert
Atserias
Albert Atserias
Joanna
Ochremiak
Joanna Ochremiak
10.4230/LIPIcs.ICALP.2017.110
M. Ajtai. The complexity of the pigeonhole principle. In 29th Annual IEEE Symposium on Foundations of Computer Science, pages 346-355, 1988.
A. Atserias and V. Dalmau. A combinatorial characterization of resolution width. J. Comput. Syst. Sci., 74(3):323-334, May 2008. A preliminary version appeared in CCC 2003. URL: http://dx.doi.org/10.1016/j.jcss.2007.06.025.
http://dx.doi.org/10.1016/j.jcss.2007.06.025
A. Atserias, Ph. G. Kolaitis, and M. Vardi. Constraint propagation as a proof system. In 10th International Conference on Principles and Practice of Constraint Programming, volume 3258 of Lecture Notes in Computer Science, pages 77-91. Springer-Verlag, 2004.
L. Barto and M. Kozik. Constraint satisfaction problems solvable by local consistency methods. J. ACM, 61(1):3:1-3:19, January 2014. URL: http://dx.doi.org/10.1145/2556646.
http://dx.doi.org/10.1145/2556646
L. Barto, J. Opršal, and M. Pinsker. The wonderland of reflections. CoRR, abs/1510.04521, 2015. URL: http://arxiv.org/abs/1510.04521.
http://arxiv.org/abs/1510.04521
P. Beame, R. Impagliazzo, J. Krajícek, T. Pitassi, P. Pudlák, and A. Woods. Exponential lower bounds for the pigeonhole principle. In 24th Annual ACM Symposium on the Theory of Computing, pages 200-220, 1992.
E. Ben-Sasson. Hard examples for bounded depth frege. In 34th Annual ACM Symposium on the Theory of Computing, pages 563-572, 2002.
A. Bulatov. Bounded relational width. Manuscript, 2009.
A. Bulatov, P. Jeavons, and A. Krokhin. Classifying the complexity of constraints using finite algebras. SIAM Journal on Computing, 34(3):720-742, 2005.
Siu On Chan. Approximation resistance from pairwise-independent subgroups. J. ACM, 63(3):27:1-27:32, August 2016. URL: http://dx.doi.org/10.1145/2873054.
http://dx.doi.org/10.1145/2873054
A. Dawar and P. Wang. Lasserre lower bounds and definability of semidefinite programming. CoRR, abs/1602.05409, 2016. URL: http://arxiv.org/abs/1602.05409.
http://arxiv.org/abs/1602.05409
M. X. Goemans and D. P. Williamson. Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming. J. ACM, 42(6):1115-1145, November 1995. URL: http://dx.doi.org/10.1145/227683.227684.
http://dx.doi.org/10.1145/227683.227684
D. Grigoriev. Linear lower bound on degrees of positivstellensatz calculus proofs for the parity. Theoretical Computer Science, 259(1-2):613-622, 2001.
D. Grigoriev and E. A. Hirsch. Algebraic proof systems over formulas. Theoretical Computer Science, 303(1):83 - 102, 2003.
D. Grigoriev, E. A. Hirsch, and D. V. Pasechnik. Complexity of semi-algebraic proofs. Moscow Mathematical Journal, 4(2):647-679, 2002.
S. Khot, G. Kindler, E. Mossel, and R. O’Donnell. Optimal inapproximability results for max-cut and other 2-variable csps? SIAM Journal on Computing, 37(1):319-357, 2007.
Ph. G. Kolaitis and M. Y. Vardi. A game-theoretic approach to constraint satisfaction. In Proceedings of the Seventeenth National Conference on Artificial Intelligence and Twelfth Conference on Innovative Applications of Artificial Intelligence, pages 175-181. AAAI Press, 2000. URL: http://dl.acm.org/citation.cfm?id=647288.721266.
http://dl.acm.org/citation.cfm?id=647288.721266
J. Krajícek. On the weak pigeonhole principle. Fundamenta Mathematicae, 170(1-3):123-140, 2001.
J. Krajícek, P. Pudlák, and A. Woods. Exponential lower bound to the size of bounded depth Frege proofs of the pigeon hole principle. Random Structures and Algorithms, 7(1):15-39, 1995.
M. Laurent. A comparison of the Sherali-Adams, Lovász-Schrijver and Lasserre relaxations for 0-1 programming. Mathematics of Operations Research, 28:470-496, 2001.
L. Lovász and A. Schrijver. Cones of matrices and set-functions and 0-1 optimization. SIAM Journal on Optimization, 1(2):166-190, 1991.
T. Pitassi. Algebraic propositional proof systems. In N. Immerman and Ph. G. Kolaitis, editors, Descriptive Complexity and Finite Models, volume 31 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 68-96. American Mathematical Society, 1997.
P. Pudlák. On the complexity of the propositional calculus. In Sets and Proofs, Invited Papers from Logic Colloquium '97, pages 197-218. Cambridge University Press, 1999.
J. Thapper and S. Živný. Sherali-adams relaxations for valued csps. In Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, pages 1058-1069, 2015.
J. Thapper and S. Živný. The limits of SDP relaxations for general-valued csps. CoRR, abs/1612.01147, 2016. URL: http://arxiv.org/abs/1612.01147.
http://arxiv.org/abs/1612.01147
M. Tulsiani. CSP gaps and reductions in the Lasserre hierarchy. In 41st Annual ACM Symposium on Theory of Computing (STOC), pages 303-312, 2009.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode