Abstract
We study the resolution complexity of Tseitin formulas over arbitrary rings in terms of combinatorial properties of graphs. We give some evidence that an expansion of a graph is a good characterization of the resolution complexity of Tseitin formulas. We extend the method of Ben-Sasson and Wigderson of proving lower bounds for the size of resolution proofs to constraint satisfaction problems under an arbitrary finite alphabet. For Tseitin formulas under the alphabet of cardinality d we provide a lower bound d e(G) − k for tree-like resolution complexity that is stronger than the one that can be obtained by the Ben-Sasson and Wigderson method. Here k is an upper bound on the degree of the graph and e(G) is the graph expansion that is equal to the minimal cut such that none of its parts is more than twice bigger than the other. We give a formal argument why a large graph expansion is necessary for lower bounds. Let G = 〈V,E 〉 be the dependency graph of the CSP, vertices of G correspond to constraints; two constraints are connected by an edge for every common variable. We prove that the tree-like resolution complexity of the CSP is at most \(d^{e(H) \cdot \log_{\frac{3}{2}} |V|}\) for some subgraph H of G.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alekhnovich, M., Hirsch, E.A., Itsykson, D.: Exponential lower bounds for the running time of DPLL algorithms on satisfiable formulas. J. Autom. Reason. 35(1-3), 51–72 (2005)
Baker, A.B.: Intelligent backtracking on constraint satisfaction problems: Experimental and theoretical results (1995)
Buss, S., Grigoriev, D., Impagliazzo, R., Pitassi, T.: Linear gaps between degrees for the polynomial calculus modulo distinct primes. Journal of Computer and System Sciences, 547–556 (1999)
Ben-Sasson, E., Wigderson, A.: Short proofs are narrow — resolution made simple. Journal of ACM 48(2), 149–169 (2001)
Cook, J., Etesami, O., Miller, R., Trevisan, L.: Goldreich’s one-way function candidate and myopic backtracking algorithms. In: Reingold, O. (ed.) TCC 2009. LNCS, vol. 5444, pp. 521–538. Springer, Heidelberg (2009)
Hwang, C.Y.J.: A Theoretical Comparison of Resolution Proof Systems for CSP Algorithms. Master’s thesis, Simon Fraser University (2004)
Impagliazzo, R., Pudlak, P., Sgall, J.: Lower bounds for the polynomial calculus and the grobner basis algorithm. Computational Complexity 8, 127–144 (1997)
Itsykson, D., Sokolov, D.: The complexity of inversion of explicit Goldreichs function by DPLL algorithms. Zapiski nauchnyh seminarov POMI 399, 88–109 (2012)
Itsykson, D.: Lower bound on average-case complexity of inversion of goldreich’s function by drunken backtracking algorithms. In: Ablayev, F., Mayr, E.W. (eds.) CSR 2010. LNCS, vol. 6072, pp. 204–215. Springer, Heidelberg (2010)
Mitchell, D.G.: The resolution complexity of constraint satisfaction (2002)
Mitchell, D.G.: Resolution complexity of random constraints. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 295–309. Springer, Heidelberg (2002)
Mitchell, D.G.: Resolution and constraint satisfaction. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, pp. 555–569. Springer, Heidelberg (2003)
Tseitin, G.S.: On the complexity of derivation in the propositional calculus. Zapiski Nauchnykh Seminarov LOMI 8, 234–259 (1968); English translation of this volume: Consultants Bureau, N.Y., pp. 115–125 (1970)
Urquhart, A.: Hard examples for resolution. JACM 34(1), 209–219 (1987)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Itsykson, D., Oparin, V. (2013). Graph Expansion, Tseitin Formulas and Resolution Proofs for CSP. In: Bulatov, A.A., Shur, A.M. (eds) Computer Science – Theory and Applications. CSR 2013. Lecture Notes in Computer Science, vol 7913. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38536-0_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-38536-0_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38535-3
Online ISBN: 978-3-642-38536-0
eBook Packages: Computer ScienceComputer Science (R0)