On the complexity of regular resolution and the Davis-Putnam procedure

DOI10.1016/0304-3975(77)90054-8zbMath0385.68048OpenAlexW2070017679MaRDI QIDQ1249435

Zvi Galil

Publication date: 1977

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(77)90054-8

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Classical propositional logic (03B05)

Related Items

A lower bound for tree resolution, Problem solving by searching for models with a theorem prover, Width versus size in resolution proofs, The relative complexity of resolution and cut-free Gentzen systems, Davis-Putnam resolution versus unrestricted resolution, An average case analysis of a resolution principle algorithm in mechanical theorem proving., A satisfiability tester for non-clausal propositional calculus, Probabilistic performance of a heurisic for the satisfiability problem, A bound on the length of a random derivation-search tree in general multi-premise calculi, Optimizing propositional calculus formulas with regard to questions of deducibility, Generating hard satisfiability problems, A note on regular resolution, A simplified proof that regular resolution is exponential, The \(Multi\)-SAT algorithm, The symmetry rule in propositional logic, The NP-hardness of finding a directed acyclic graph for regular resolution, Unrestricted resolution versus N-resolution, Meta-resolution: An algorithmic formalisation, Near-optimal lower bounds on regular resolution refutations of Tseitin formulas for all constant-degree graphs, Tseitin's formulas revisited, Counting truth assignments of formulas of bounded tree-width or clique-width, The complexity of the Hajós calculus for planar graphs, The complexity of Gentzen systems for propositional logic, Resolution deduction to detect satisfiability for another class including non-Horn sentences in propositional logic, Exact thresholds for DPLL on random XOR-SAT and NP-complete extensions of XOR-SAT, A comparative study of several proof procedures, Hard satisfiable instances for DPLL-type algorithms, On Exponential Lower Bounds for Partially Ordered Resolution, The intractability of resolution, A Logical Autobiography, Reflections on Proof Complexity and Counting Principles

Cites Work

• Unnamed Item
• Unnamed Item
• Forest embeddings in regular graphs of large girth
• A Way to Simplify Truth Functions
• A Machine-Oriented Logic Based on the Resolution Principle
• A Computing Procedure for Quantification Theory
• The complexity of theorem-proving procedures