Small Stone in Pool
Samuel R. Buss (Univ. of California, San Diego), Leszek Aleksander, Kolodziejczyk (University of Warsaw)
TL;DR
This paper demonstrates that Stone tautologies have polynomial size proofs in pool resolution and regRTI, showing they do not separate resolution from DPLL with clause learning, contrasting previous exponential lower bounds.
Contribution
It proves polynomial size proofs for Stone tautologies in pool resolution and regRTI, extending understanding of their proof complexity.
Findings
Stone tautologies have polynomial size proofs in pool resolution.
Stone tautologies have polynomial size proofs in regRTI.
They do not separate resolution from DPLL with clause learning.
Abstract
The Stone tautologies are known to have polynomial size resolution refutations and require exponential size regular refutations. We prove that the Stone tautologies also have polynomial size proofs in both pool resolution and the proof system of regular tree-like resolution with input lemmas (regRTI). Therefore, the Stone tautologies do not separate resolution from DPLL with clause learning.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.