More Web Proxy on the site http://driver.im/

Article

Resolution and pebbling games

Authors:

Neil ThapenAuthors Info & Claims

SAT'05: Proceedings of the 8th international conference on Theory and Applications of Satisfiability Testing

Pages 76 - 90

https://doi.org/10.1007/11499107_6

Published: 19 June 2005 Publication History

Abstract

We define a collection of Prover-Delayer games to characterise some subsystems of propositional resolution. We give some natural criteria for the games which guarantee lower bounds on the resolution width. By an adaptation of the size-width tradeoff for resolution of [10] this result also gives lower bounds on proof size.

We also use games to give upper bounds on proof size, and in particular describe a good strategy for the Prover in a certain game which yields a short refutation of the Linear Ordering principle.

Using previous ideas we devise a new algorithm to automatically generate resolution refutations. On bounded width formulas, our algorithm is as least as good as the width based algorithm of [10]. Moreover, it finds short proofs of the Linear Ordering principle when the variables respect a given order.

Finally we approach the question of proving that a formula F is hard to refute if and only if is “almost” satisfiable. We prove results in both directions when “almost satisfiable” means that it is hard to distuinguish F from a satisfiable formula using limited pebbling games.

References

[1]

M. Alekhnovich, E. Ben-Sasson, A. Razborov, A. Wigderson. Space complexity in propositional calculus. SIAM J. Comput. 31(4) pp. 1184-1211, 2002.

Digital Library

[2]

M. Alekhnovich, A.A. Razborov. Resolution is not automatizable unless W{P} is not tractable. 42nd IEEE Symposium on Foundations of Computer Science, FOCS 2001, pp. 210-219.

Digital Library

[3]

A. Atserias, V. Dalmau. A combinatorial characterization of Resolution Width 18th IEEE Conference on Computational Complexity (CCC), pp. 239-247, 2003.

[4]

A. Atserias, P. Kolaitis, M. Vardi. Constraint Propagation as a Proof System. In 10th International Conference on Principles and Practice of Constraint Programming (CP), LNCS vol. 3258, pp. 77-91, 2004.

Digital Library

[5]

P. Beame, R.M. Karp, T. Pitassi, M.E. Saks. On the Complexity of Unsatisfiability Proofs for Random k-CNF Formulas. SIAM J. Comput. 31(4) pp. 1048-1075, 2002.

Digital Library

[6]

P. Beame, H. Kautz. A Sabharwal Understanding the power of clause learning Proceedings IJCAI pp. 1194-1201, 2003.

Digital Library

[7]

P. Beame, T. Pitassi. Simplified and Improved Resolution Lower Bounds. 37th IEEE Symposium on Foundations of Computer Science, FOCS 1996, pp. 274-282.

Digital Library

[8]

E. Ben-Sasson, N. Galesi. Space Complexity of Random Formulae in Resolution. 16th IEEE Annual Conference on Computational Complexity, CCC 2001, pp. 42-51.

Digital Library

[9]

E. Ben-Sasson, R. Impagliazzo, A. Wigderson. Near optimal separation of treelike and general Resolution. Electronic Colloquium on Computational Complexity (ECCC) TR00-005, 2000. To appear in Combinatorica.

[10]

E. Ben-Sasson, A. Wigderson. Short Proofs Are Narrow--Resolution Made Simple. J. ACM 48(2) pp. 149-168, 2001.

Digital Library

[11]

M.L. Bonet, N. Galesi. Optimality of Size-Width Tradeoffs for Resolution. Computational Complexity, Vol 10(4) 2001. pp. 261-276.

Digital Library

[12]

J.L. Esteban, N. Galesi, J. Messner. On the Complexity of Resolution with Bounded Conjunctions. Theoretical Computer Science 321(2-3) pp. 347-370, 2004.

Digital Library

[13]

J.L. Esteban, J. Torán. Space bounds for Resolution. Inform. and Comput. 171 (1) pp. 84-97, 2001.

Digital Library

[14]

N. Galesi, N. Thapen. The Complexity of Treelike Systems over λ Local Formuale Proceedings of IEEE Conference on Computational Complexity 2004.

Digital Library

[15]

N. Galesi, N. Thapen. Resolution and Pebbling Games ECCC Technical Report TR04-112. http://www.eccc.uni-trier.de/eccc-reports/2004/TR04-112/index.html

[16]

A. Haken. The Intractability of Resolution. Theoret. Comp. Sci. 39, pp. 297-308, 1985.

[17]

J. Krajíček. Bounded arithmetic, propositional logic, and complexity theory, Encyclopedia of Mathematics and Its Applications, Vol. 60, Cambridge University Press, (1995).

Digital Library

[18]

J. Krajíček. On the weak pigeonhole principle. Fund. Math. 170(1-3) pp. 123-140, 2001. J. Symbolic Logic 59(1) pp. 73-86, 1994.

Digital Library

[19]

P. Pudlak. Proofs as Games. American Math. Monthly, Vol. 2000-2001, pp. 541-550.

[20]

P. Pudlák, R. Impagliazzo. A lower bound for DLL algorithms for k-SAT". Conference Proceeding of Symposium on Distributed Algorithms (2000), pp. 128-136.

Digital Library

[21]

S. Riis. A complexity gap for tree-resolution. Computational Complexity 10(3), pp. 179-209, 2001.

[22]

A. Urquhart. Hard examples for Resolution. J. ACM 34(1) pp. 209-219, 1987.

Digital Library

Cited By

Torán JWörz F(2023)Number of Variables for Graph Differentiation and the Resolution of Graph Isomorphism FormulasACM Transactions on Computational Logic10.1145/358047824:3(1-25)Online publication date: 21-Jan-2023
https://dl.acm.org/doi/10.1145/3580478
Nordström J(2012)On the Relative Strength of Pebbling and ResolutionACM Transactions on Computational Logic (TOCL)10.1145/2159531.215953813:2(1-43)Online publication date: 1-Apr-2012
https://dl.acm.org/doi/10.1145/2159531.2159538
Rhodes M(2008)Resolution Width and Cutting Plane Rank Are IncomparableProceedings of the 33rd international symposium on Mathematical Foundations of Computer Science10.1007/978-3-540-85238-4_47(575-587)Online publication date: 25-Aug-2008
https://dl.acm.org/doi/10.1007/978-3-540-85238-4_47

Index Terms

Resolution and pebbling games

Recommendations

On the Relative Strength of Pebbling and Resolution
CCC '10: Proceedings of the 2010 IEEE 25th Annual Conference on Computational Complexity

The last decade has seen a revival of interest in pebble games in the context of proof complexity. Pebbling has proven to be a useful tool for studying resolution-based proof systems when comparing the strength of different subsystems, showing bounds on ...
On the Relative Strength of Pebbling and Resolution

The last decade has seen a revival of interest in pebble games in the context of proof complexity. Pebbling has proven to be a useful tool for studying resolution-based proof systems when comparing the strength of different subsystems, showing bounds on ...
Clause learning, resolution space, & pebbling

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

SAT'05: Proceedings of the 8th international conference on Theory and Applications of Satisfiability Testing

June 2005

491 pages

ISBN:3540262768

Editors:
Fahiem Bacchus
Department of Computer Science, University of Toronto, Canada
,
Toby Walsh
Dept. of Computer Science, Trinity College, Dublin 2, Canada

Sponsors

INTEL: Intel Corporation
Cadence Design Systems
Microsoft Research: Microsoft Research
Intelligence Information Systems Institute: Intelligence Information Systems Institute
CoLogNet Network of Excellence: CoLogNet Network of Excellence

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 19 June 2005

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 10 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Torán JWörz F(2023)Number of Variables for Graph Differentiation and the Resolution of Graph Isomorphism FormulasACM Transactions on Computational Logic10.1145/358047824:3(1-25)Online publication date: 21-Jan-2023
https://dl.acm.org/doi/10.1145/3580478
Nordström J(2012)On the Relative Strength of Pebbling and ResolutionACM Transactions on Computational Logic (TOCL)10.1145/2159531.215953813:2(1-43)Online publication date: 1-Apr-2012
https://dl.acm.org/doi/10.1145/2159531.2159538
Rhodes M(2008)Resolution Width and Cutting Plane Rank Are IncomparableProceedings of the 33rd international symposium on Mathematical Foundations of Computer Science10.1007/978-3-540-85238-4_47(575-587)Online publication date: 25-Aug-2008
https://dl.acm.org/doi/10.1007/978-3-540-85238-4_47

View Options

View options

Media

Figures

Other

Tables

View Table of Contents