Resolution Is Not Automatizable Unless W[P] Is Tractable

DOI10.1137/06066850XzbMath1169.03044OpenAlexW2152390092MaRDI QIDQ3395034

Michael Alekhnovich, Alexander A. Razborov

Publication date: 20 August 2009

Published in: SIAM Journal on Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1137/06066850x

zbMATH Keywords

resolutionproof complexityparametrized complexityautomatizability

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Mechanization of proofs and logical operations (03B35) Complexity of computation (including implicit computational complexity) (03D15) Complexity of proofs (03F20)

Related Items (37)

On finding short resolution refutations and small unsatisfiable subsets ⋮ On space and depth in resolution ⋮ Describing parameterized complexity classes ⋮ On the automatizability of resolution and related propositional proof systems ⋮ On the complexity of resolution with bounded conjunctions ⋮ The Birth and Early Years of Parameterized Complexity ⋮ A Basic Parameterized Complexity Primer ⋮ On the complexity of finding shortest variable disjunction branch-and-bound proofs ⋮ Parameterized Derandomization ⋮ Parity Games and Propositional Proofs ⋮ Extended clause learning ⋮ Towards NP-P via proof complexity and search ⋮ On reducibility and symmetry of disjoint NP pairs. ⋮ Optimal length cutting plane refutations of integer programs ⋮ Parameterized random complexity ⋮ Satisfiability, branch-width and Tseitin tautologies ⋮ Special issue in memory of Misha Alekhnovich. Foreword ⋮ On the automatizability of polynomial calculus ⋮ An Upper Bound for Resolution Size: Characterization of Tractable SAT Instances ⋮ The NP-hardness of finding a directed acyclic graph for regular resolution ⋮ Confronting intractability via parameters ⋮ The complexity of properly learning simple concept classes ⋮ Automatizability and Simple Stochastic Games ⋮ Parameterized Bounded-Depth Frege Is Not Optimal ⋮ A combinatorial characterization of resolution width ⋮ The parameterized complexity of probability amplification ⋮ Mean-payoff games and propositional proofs ⋮ Parameterized Complexity of DPLL Search Procedures ⋮ Short propositional refutations for dense random 3CNF formulas ⋮ Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers ⋮ Finding a tree structure in a resolution proof is NP-complete ⋮ Boundary Points and Resolution ⋮ Short Proofs Are Hard to Find ⋮ Data compression for proof replay ⋮ Pool resolution is NP-hard to recognize ⋮ Bounded-depth Frege complexity of Tseitin formulas for all graphs ⋮ Parameterized counting problems

This page was built for publication: Resolution Is Not Automatizable Unless W[P] Is Tractable