Document Open Access Logo

Proof Complexity Meets Algebra

Authors Albert Atserias, Joanna Ochremiak

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2017.110.pdf
  • Filesize: 481 kB
  • 14 pages

Document Identifiers

Author Details

Albert Atserias
Joanna Ochremiak

Cite AsGet BibTex

Albert Atserias and Joanna Ochremiak. Proof Complexity Meets Algebra. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 110:1-110:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.ICALP.2017.110

Abstract

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.
Keywords
  • Constraint Satisfaction Problem
  • Proof Complexity
  • Reductions
  • Gap Theorems

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. M. Ajtai. The complexity of the pigeonhole principle. In 29th Annual IEEE Symposium on Foundations of Computer Science, pages 346-355, 1988. Google Scholar
  2. 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.
  3. 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. Google Scholar
  4. 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.
  5. L. Barto, J. Opršal, and M. Pinsker. The wonderland of reflections. CoRR, abs/1510.04521, 2015. URL: http://arxiv.org/abs/1510.04521.
  6. 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. Google Scholar
  7. E. Ben-Sasson. Hard examples for bounded depth frege. In 34th Annual ACM Symposium on the Theory of Computing, pages 563-572, 2002. Google Scholar
  8. A. Bulatov. Bounded relational width. Manuscript, 2009. Google Scholar
  9. A. Bulatov, P. Jeavons, and A. Krokhin. Classifying the complexity of constraints using finite algebras. SIAM Journal on Computing, 34(3):720-742, 2005. Google Scholar
  10. 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.
  11. 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.
  12. 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.
  13. D. Grigoriev. Linear lower bound on degrees of positivstellensatz calculus proofs for the parity. Theoretical Computer Science, 259(1-2):613-622, 2001. Google Scholar
  14. D. Grigoriev and E. A. Hirsch. Algebraic proof systems over formulas. Theoretical Computer Science, 303(1):83 - 102, 2003. Google Scholar
  15. D. Grigoriev, E. A. Hirsch, and D. V. Pasechnik. Complexity of semi-algebraic proofs. Moscow Mathematical Journal, 4(2):647-679, 2002. Google Scholar
  16. 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. Google Scholar
  17. 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.
  18. J. Krajícek. On the weak pigeonhole principle. Fundamenta Mathematicae, 170(1-3):123-140, 2001. Google Scholar
  19. 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. Google Scholar
  20. 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. Google Scholar
  21. 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. Google Scholar
  22. 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. Google Scholar
  23. 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. Google Scholar
  24. 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. Google Scholar
  25. 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.
  26. M. Tulsiani. CSP gaps and reductions in the Lasserre hierarchy. In 41st Annual ACM Symposium on Theory of Computing (STOC), pages 303-312, 2009. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact