The Efficiency of Resolution and Davis--Putnam Procedures

DOI10.1137/S0097539700369156zbMath1004.03048WikidataQ56812992 ScholiaQ56812992MaRDI QIDQ2784492

Toniann Pitassi, P. W. Beame, Richard M. Karp, Michael E. Saks

Publication date: 23 April 2002

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

zbMATH Keywords

lower boundsresolutionsearch algorithmssatisfiabilityproof complexityDavis-Putnam procedurerandom formulas

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Analysis of algorithms (68W40) Mechanization of proofs and logical operations (03B35) Complexity of computation (including implicit computational complexity) (03D15) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Complexity of proofs (03F20)

Related Items

Many hard examples in exact phase transitions ⋮ On the complexity of resolution with bounded conjunctions ⋮ Data reductions, fixed parameter tractability, and random weighted \(d\)-CNF satisfiability ⋮ Counting for satisfiability by inverting resolution ⋮ Conjunctive query evaluation by search-tree revisited ⋮ An efficient approach to solving random \(k\)-SAT problems ⋮ Space Complexity in Polynomial Calculus ⋮ On CDCL-Based Proof Systems with the Ordered Decision Strategy ⋮ Random Instances of W[2-Complete Problems: Thresholds, Complexity, and Algorithms] ⋮ On Random Betweenness Constraints ⋮ Lower bounds for \(k\)-DNF resolution on random 3-CNFs ⋮ Constructing Hard Examples for Graph Isomorphism ⋮ Parameterized Bounded-Depth Frege Is Not Optimal ⋮ Limitations of restricted branching in clause learning ⋮ The Complexity of Propositional Proofs ⋮ Parameterized Complexity of DPLL Search Procedures ⋮ Short propositional refutations for dense random 3CNF formulas ⋮ Supercritical Space-Width Trade-offs for Resolution ⋮ On Random Ordering Constraints ⋮ Resolution for Max-SAT ⋮ When does the giant component bring unsatisfiability? ⋮ Lower bounds for the weak pigeonhole principle and random formulas beyond resolution ⋮ The resolution complexity of random graph \(k\)-colorability ⋮ Spines of random constraint satisfaction problems: definition and connection with computational complexity ⋮ Unrestricted vs restricted cut in a tableau method for Boolean circuits