A feasible interpolation for random resolution

DOI10.23638/LMCS-13(1:5)2017MaRDI QIDQ2980967zbMATHFDO

Authors Jan Krajíček

Publication date 8 May 2017

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

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)

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.

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)

Cites work

• scientific article; zbMATH DE number 1215500 (Why is no real title available?)
• scientific article; zbMATH DE number 1142303 (Why is no real title available?)
• Fragments of approximate counting
• Interpolation by a Game
• Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
• Monotone Circuits for Connectivity Require Super-Logarithmic Depth
• The monotone circuit complexity of Boolean functions
• Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic

Cited in

(5)

• Randomized feasible interpolation and monotone circuits with a local oracle
• Resolution over linear equations and multilinear proofs
• Resolution with counting: dag-like lower bounds and different moduli
• A conditional superpolynomial lower bound for extended resolution
• 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)