LIPIcs.CCC.2017.1.pdf
- Filesize: 0.51 MB
- 10 pages
Document
Random Resolution Refutations
Authors
-
Part of:
Volume:
32nd Computational Complexity Conference (CCC 2017)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computational Complexity Conference (CCC) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2017-08-01
Cite AsGet BibTex
Pavel Pudlák and Neil Thapen. Random Resolution Refutations. In 32nd Computational Complexity Conference (CCC 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 79, pp. 1:1-1:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.CCC.2017.1
https://doi.org/10.4230/LIPIcs.CCC.2017.1
Abstract
We study the random resolution refutation system definedin [Buss et al. 2014]. This attempts to capture the notion of a resolution refutation that may make mistakes but is correct most of the time. By proving the equivalence of several different definitions, we show that this concept is robust. On the other hand, if P does not equal NP, then random resolution cannot be polynomially simulated by any proof system in which correctness of proofs is checkable in polynomial time.
We prove several upper and lower bounds on the width and size of random resolution refutations of explicit and random unsatisfiable CNF formulas. Our main result is a separation between polylogarithmic width random resolution and quasipolynomial size resolution, which solves the problem stated in [Buss et al. 2014]. We also prove exponential size lower bounds on random resolution refutations of the pigeonhole principle CNFs, and of a family of CNFs which have polynomial size refutations in constant depth Frege.
Keywords
- proof complexity
- random
- resolution
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Sanjeev Arora and Boaz Barak. Computational Complexity: A Modern Approach. Cambridge University Press, 2009. URL: http://dx.doi.org/10.1017/CBO9780511804090.
- Albert Atserias and Neil Thapen. The ordering principle in a fragment of approximate counting. ACM Trans. Comput. Logic, 15(4):29:1-11, 2014. URL: http://dx.doi.org/10.1145/2629555.
- Samuel R. Buss, Leszek Aleksander Kołodziejczyk, and Neil Thapen. Fragments of approximate counting. The Journal of Symbolic Logic, 79(2):496-525, 2014. URL: http://dx.doi.org/10.1017/jsl.2013.37.
- Mario Chiari and Jan Krajíček. Witnessing functions in bounded arithmetic and search problems. The Journal of Symbolic Logic, 63(03):1095-1115, 1998. URL: http://dx.doi.org/10.2307/2586729.
- Vašek Chvátal and Endre Szemerédi. Many hard examples for resolution. Journal of the ACM, 35(4):759-768, 1988. URL: http://dx.doi.org/10.1145/48014.48016.
- Stephen Cook and Robert Reckhow. The relative efficiency of propositional proof systems. The Journal of Symbolic Logic, 44(1):36-50, 1979. URL: http://dx.doi.org/10.2307/2273702.
- Russell Impagliazzo and Jan Krajíček. A note on conservativity relations among bounded arithmetic theories. Mathematical Logic Quarterly, 48(3):375-377, 2002. URL: http://dx.doi.org/10.1002/1521-3870(200204)48:3<375::AID-MALQ375>3.0.CO;2-L.
- Emil Jeřábek. On independence of variants of the weak pigeonhole principle. Journal of Logic and Computation, 17(3):587-604, 2007. URL: http://dx.doi.org/10.1093/logcom/exm017.
- Jan Krajíček. Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. The Journal of Symbolic Logic, 62(02):457-486, 1997. URL: http://dx.doi.org/10.2307/2275541.
- Jan Krajíček. On the weak pigeonhole principle. Fundamenta Mathematicae, 170:123-140, 2001. URL: http://dx.doi.org/10.4064/fm170-1-8.
- Jan Krajíček. A feasible interpolation for random resolution, 2016. Preprint arXiv:1604.06560. URL: http://arxiv.org/abs/1604.06560.
- Jan Krajíček, Alan Skelley, and Neil Thapen. NP search problems in low fragments of bounded arithmetic. The Journal of Symbolic Logic, 72(2):649-672, 2007. URL: http://dx.doi.org/10.2178/jsl/1185803628.
- Pavel Pudlák and Neil Thapen. Random resolution refutations, 2016. Electronic Colloquium on Computational Complexity, TR16-175. URL: https://eccc.weizmann.ac.il/report/2016/175/.
- Alexander Razborov. Pseudorandom generators hard for k-DNF resolution and polynomial calculus resolution. Annals of Mathematics, 181(2):415-472, 2015. URL: http://dx.doi.org/10.4007/annals.2015.181.2.1.
- Alan Skelley and Neil Thapen. The provably total search problems of bounded arithmetic. Proceedings of the London Mathematical Society, 103(1):106-138, 2011. URL: http://dx.doi.org/10.1112/plms/pdq044.
- Neil Thapen. A tradeoff between length and width in resolution. Theory of Computing, 12(5):1-14, 2016. URL: http://dx.doi.org/10.4086/toc.2016.v012a005.