A feasible interpolation for random resolution

DOI10.23638/LMCS-13(1:5)2017zbMATH Open1448.03047arXiv1604.06560MaRDI QIDQ2980967FDOQ2980967

Authors: Jan Krajíček 

Publication date: 8 May 2017

Abstract: Random resolution, defined by Buss, Kolodziejczyk and Thapen (JSL, 2014), is a sound propositional proof system that extends the resolution proof system by the possibility to augment any set of initial clauses by a set of randomly chosen clauses (modulo a technical condition). We show how to apply the general feasible interpolation theorem for semantic derivations of Krajicek (JSL, 1997) to random resolution. As a consequence we get a lower bound for random resolution refutations of the clique-coloring formulas.

Full work available at URL: https://arxiv.org/abs/1604.06560

Recommendations

• Randomized feasible interpolation and monotone circuits with a local oracle
• Random resolution refutations
• Random resolution refutations
• A conditional superpolynomial lower bound for extended resolution
• Sparser random 3-SAT refutation algorithms and the interpolation problem (extended abstract)

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Complexity of proofs (03F20) First-order arithmetic and fragments (03F30) Complexity of computation (including implicit computational complexity) (03D15)

Cites Work

• Monotone Circuits for Connectivity Require Super-Logarithmic Depth
• Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
• The monotone circuit complexity of Boolean functions
• Title not available (Why is that?)
• Title not available (Why is that?)
• Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic
• Fragments of approximate counting
• Interpolation by a Game

Cited In (5)

• A conditional superpolynomial lower bound for extended resolution
• Resolution with counting: dag-like lower bounds and different moduli
• Randomized feasible interpolation and monotone circuits with a local oracle
• Resolution over linear equations and multilinear proofs
• Random resolution refutations

This page was built for publication: A feasible interpolation for random resolution

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2980967)