Random resolution refutations
Tóm tắt
We study the random resolution refutation system defined in Buss et al. (J Symb Logic 79(2):496–525, 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
$${{\bf P} \neq {\bf 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.
Tài liệu tham khảo
Ajtai, Miklós: The complexity of the pigeonhole principle. Combinatorica 14(4), 417–433 (1994)
Sanjeev Arora & Boaz Barak (2009). Computational complexity: a modern approach Cambridge University Press.
Albert Atserias & Neil Thapen: The ordering principle in a fragment of approximate counting. ACM Transactions on Computational Logic 15(4), 29 (2014)
Eli Ben-Sasson & Avi Wigderson: Short proofs are narrow—resolution made simple. Journal of the ACM 48(2), 149–169 (2001)
Buss, Samuel, Impagliazzo, Russell, Krajíček, Jan, Pudlák, Pavel, Razborov, Alexander, Sgall, Jiri: Proof complexity in algebraic systems and bounded depth Frege systems with modular counting. Computational Complexity 6(3), 256–298 (1996)
Buss, Samuel, Kołodziejczyk, Leszek A., Thapen, Neil: Fragments of approximate counting. Journal of Symbolic Logic 79(2), 496–525 (2014)
Buss, Samuel, Kołodziejczyk, Leszek A., Zdanowski, Konrad: Collapsing modular counting in bounded arithmetic and constant depth propositional proofs. Transactions of the American Mathematical Society 367(11), 7517–7563 (2015)
Mario Chiari & Jan Krajíček: Witnessing functions in bounded arithmetic and search problems. Journal of Symbolic Logic 63(3), 1095–1115 (1998)
Vašek Chvátal & Endre Szemerédi: Many hard examples for resolution. Journal of the ACM 35(4), 759–768 (1988)
Stephen Cook & Robert Reckhow: The relative efficiency of propositional proof systems. Journal of Symbolic Logic 44(1), 36–50 (1979)
Russell Impagliazzo & Jan Krajíček: A note on conservativity relations among bounded arithmetic theories. Mathematical Logic Quarterly 48(3), 375–377 (2002)
Russell Impagliazzo, Toniann Pitassi & Alasdair Urquhart (1994). Upper and lower bounds for tree-like cutting planes proofs. In Proceedings of LICS'94, 220–228
Jeřábek, Emil: On independence of variants of the weak pigeonhole principle. Journal of Logic and Computation 17(3), 587–604 (2007)
Bala Kalyanasundaram & Georg Schintger: The probabilistic communication complexity of set intersection. SIAM Journal on Discrete Mathematics 5(4), 545–557 (1992)
Krajíček, Jan: Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. Journal of Symbolic Logic 62(2), 457–486 (1997)
Krajíček, Jan: On the weak pigeonhole principle. Fundamenta Mathematicae 170(1–2), 123–140 (2001)
Jan Krajíček (2017). A feasible interpolation for random resolution. Logical Methods in Computer Science 13(1).
Jan Krajíček (2018). Randomized feasible interpolation and monotone circuits with a local oracle. Journal of Mathematical Logic 18(2).
Krajíček, Jan, Pudlák, Pavel, Woods, Alan: An exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle. Random Structures & Algorithms 7(1), 15–39 (1995)
Krajíček, Jan, Skelley, Alan, Thapen, Neil: NP search problems in low fragments of bounded arithmetic. Journal of Symbolic Logic 72(2), 649–672 (2007)
Ran Raz & Avi Wigderson: Monotone circuits for matching require linear depth. Journal of the ACM 39(3), 736–744 (1992)
Alexander Razborov (2015). Pseudorandom generators hard for k-DNF resolution and polynomial calculus resolution. Annals of Mathematics 415–472
Alan Skelley & Neil Thapen: The provably total search problems of bounded arithmetic. Proceedings of the London Mathematical Society 103(1), 106–138 (2011)
Thapen, Neil: A tradeoff between length and width in resolution. Theory of Computing 12, 5 (2016)
Alasdair Urquhart & Xudong Fu: Simplified lower bounds for propositional proofs. Notre Dame Journal of Formal Logic 37(4), 534–544 (1996)