Downloads provided by UsageCounts
arXiv: 1711.07320
handle: 2117/129930 , 2117/110969
We analyze how the standard reductions between constraint satisfaction problems affect their proof complexity. We show that, for the most studied propositional, algebraic, and semialgebraic 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 characterized algebraically. We illustrate our results by a gap theorem saying that a constraint language either has resolution refutations of constant 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 refutations of sublinear degree in Sums of Squares and Polynomial Calculus over the real field, for which we provide alternative proofs. We then ask for the existence of a natural proof system with good behavior 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 Lovász-Schrijver satisfies both requirements. Finally, building on the known lower bounds, we demonstrate the applicability of the method of reducibilities and construct new explicit hard instances of the graph three-coloring problem for all studied proof systems.
Complexity of proofs, FOS: Computer and information sciences, Computer Science - Logic in Computer Science, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Màquines, Teoria de, Gap theorems, Constraint satisfaction problem, [INFO.INFO-DS] Computer Science [cs]/Data Structures and Algorithms [cs.DS], reductions, Computational Complexity (cs.CC), Polynomials, Gap Theorems, Machine theory, Àrees temàtiques de la UPC::Informàtica::Informàtica teòrica::Algorísmica i teoria de la complexitat, gap theorems, proof complexity, Theorem proving, Complexitat computacional, Àrees temàtiques de la UPC::Informàtica::Informàtica teòrica, 000 Computer science, knowledge, general works, Proof Complexity, 004, :Informàtica::Informàtica teòrica::Algorísmica i teoria de la complexitat [Àrees temàtiques de la UPC], Logic in Computer Science (cs.LO), Computational complexity, Computer Science - Computational Complexity, Algebra, :Informàtica::Informàtica teòrica [Àrees temàtiques de la UPC], Computer Science, Graph colouring, [INFO.INFO-CC] Computer Science [cs]/Computational Complexity [cs.CC], Àlgebra, Proof complexity, Constraint Satisfaction Problem, Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.), constraint satisfaction problem, Reductions
Complexity of proofs, FOS: Computer and information sciences, Computer Science - Logic in Computer Science, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Màquines, Teoria de, Gap theorems, Constraint satisfaction problem, [INFO.INFO-DS] Computer Science [cs]/Data Structures and Algorithms [cs.DS], reductions, Computational Complexity (cs.CC), Polynomials, Gap Theorems, Machine theory, Àrees temàtiques de la UPC::Informàtica::Informàtica teòrica::Algorísmica i teoria de la complexitat, gap theorems, proof complexity, Theorem proving, Complexitat computacional, Àrees temàtiques de la UPC::Informàtica::Informàtica teòrica, 000 Computer science, knowledge, general works, Proof Complexity, 004, :Informàtica::Informàtica teòrica::Algorísmica i teoria de la complexitat [Àrees temàtiques de la UPC], Logic in Computer Science (cs.LO), Computational complexity, Computer Science - Computational Complexity, Algebra, :Informàtica::Informàtica teòrica [Àrees temàtiques de la UPC], Computer Science, Graph colouring, [INFO.INFO-CC] Computer Science [cs]/Computational Complexity [cs.CC], Àlgebra, Proof complexity, Constraint Satisfaction Problem, Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.), constraint satisfaction problem, Reductions
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 10 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Top 10% | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
| views | 60 | |
| downloads | 78 |

Views provided by UsageCounts
Downloads provided by UsageCounts