Random Resolution Refutations

Authors Pavel Pudlák, Neil Thapen

Thumbnail PDF


  • Filesize: 0.51 MB
  • 10 pages

Document Identifiers

Author Details

Pavel Pudlák
Neil Thapen

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)


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.
  • proof complexity
  • random
  • resolution


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Sanjeev Arora and Boaz Barak. Computational Complexity: A Modern Approach. Cambridge University Press, 2009. URL: http://dx.doi.org/10.1017/CBO9780511804090.
  2. 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.
  3. 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.
  4. 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.
  5. 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.
  6. 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.
  7. 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.
  8. 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.
  9. 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.
  10. Jan Krajíček. On the weak pigeonhole principle. Fundamenta Mathematicae, 170:123-140, 2001. URL: http://dx.doi.org/10.4064/fm170-1-8.
  11. Jan Krajíček. A feasible interpolation for random resolution, 2016. Preprint arXiv:1604.06560. URL: http://arxiv.org/abs/1604.06560.
  12. 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.
  13. 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/.
  14. 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.
  15. 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.
  16. 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.
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail