Resolution Is Not Automatizable Unless W[P] Is Tractable

DOI10.1137/06066850XMaRDI QIDQ3395034zbMATH OpenOpenAlexFDO

Authors Michael Alekhnovich, Alexander 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

automatizabilityparametrized complexityproof complexityresolution

Mathematics Subject Classification ID

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

Cited in

(44)

• Finding a tree structure in a resolution proof is NP-complete
• Data compression for proof replay
• Pool resolution is NP-hard to recognize
• On reducibility and symmetry of disjoint NP pairs.
• 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
• Parameterized random complexity
• On the automatizability of polynomial calculus
• Bounded-depth Frege complexity of Tseitin formulas for all graphs
• On the complexity of finding shortest variable disjunction branch-and-bound proofs
• The complexity of properly learning simple concept classes
• A combinatorial characterization of resolution width
• Parameterized counting problems
• Trade-offs between time and memory in a tighter model of CDCL SAT solvers
• The birth and early years of parameterized complexity
• A basic parameterized complexity primer
• An upper bound for resolution size: characterization of tractable SAT instances
• Automatizability and simple stochastic games
• Parameterized bounded-depth Frege is not optimal
• Parameterized Derandomization
• Boundary Points and Resolution
• Towards NP-P via proof complexity and search
• Satisfiability, branch-width and Tseitin tautologies
• Special issue in memory of Misha Alekhnovich. Foreword
• Confronting intractability via parameters
• Short Proofs Are Hard to Find
• Parity Games and Propositional Proofs
• Parameterized complexity of DPLL search procedures
• Optimal length cutting plane refutations of integer programs
• Extended clause learning
• On computing small variable disjunction branch-and-bound trees
• Proof complexity and beyond. Abstracts from the workshop held March 24--29, 2024
• Failure of feasible disjunction property for k-DNF resolution and NP-hardness of automating it
• Depth-d Frege systems are not automatable unless P\,=\,NP
• Quantum automating TC^0-Frege is LWE-hard
• Quantum automating \(\mathrm{TC}^0\)-Frege is LWE-hard
• Optimal length cutting plane refutations of integer programs
• Mean-payoff games and propositional proofs
• Short propositional refutations for dense random 3CNF formulas
• On finding short resolution refutations and small unsatisfiable subsets
• The NP-hardness of finding a directed acyclic graph for regular resolution
• The parameterized complexity of probability amplification

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

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