On the complexity of regular resolution and the Davis-Putnam procedure
From MaRDI portal
Publication:1249435
DOI10.1016/0304-3975(77)90054-8zbMath0385.68048MaRDI QIDQ1249435
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
Related Items
Meta-resolution: An algorithmic formalisation, Exact thresholds for DPLL on random XOR-SAT and NP-complete extensions of XOR-SAT, The NP-hardness of finding a directed acyclic graph for regular resolution, The intractability of resolution, A satisfiability tester for non-clausal propositional calculus, Probabilistic performance of a heurisic for the satisfiability problem, Optimizing propositional calculus formulas with regard to questions of deducibility, A note on regular resolution, A simplified proof that regular resolution is exponential, Unrestricted resolution versus N-resolution, Tseitin's formulas revisited, The complexity of Gentzen systems for propositional logic, A lower bound for tree resolution, Problem solving by searching for models with a theorem prover, 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., Resolution deduction to detect satisfiability for another class including non-Horn sentences in propositional logic, A comparative study of several proof procedures, The \(Multi\)-SAT algorithm, The symmetry rule in propositional logic, The complexity of the Hajós calculus for planar graphs, Width versus size in resolution proofs, Counting truth assignments of formulas of bounded tree-width or clique-width, Hard satisfiable instances for DPLL-type algorithms, A bound on the length of a random derivation-search tree in general multi-premise calculi
Cites Work
