On a generalization of extended resolution
From MaRDI portal
Publication:1961452
DOI10.1016/S0166-218X(99)00037-2zbMath0941.68126OpenAlexW2021870295MaRDI QIDQ1961452
Publication date: 3 August 2000
Published in: Discrete Applied Mathematics (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/s0166-218x(99)00037-2
Related Items
On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers, On preprocessing techniques and their impact on propositional model counting, Exploiting Resolution-Based Representations for MaxSAT Solving, Expressing Symmetry Breaking in DRAT Proofs, Simulating circuit-level simplifications on CNF, Conformant planning as a case study of incremental QBF solving, Unnamed Item, Generating Extended Resolution Proofs with a BDD-Based SAT Solver, Contradiction separation based dynamic multi-clause synergized automated deduction, Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets, Simulating strong practical proof systems with extended resolution, Incremental preprocessing methods for use in BMC, New methods for 3-SAT decision and worst-case analysis, Truth Assignments as Conditional Autarkies, Extended resolution simulates binary decision diagrams, Blocked Clause Elimination for QBF, The resolution of Keller's conjecture, Generating extended resolution proofs with a BDD-based SAT solver, Strong extension-free proof systems, Definability for model counting, Super-Blocked Clauses, Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer, Non-clausal redundancy properties, Investigations on autark assignments, Present and Future of Practical SAT Solving, Covered clauses are not propagation redundant, The resolution of Keller's conjecture, The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1, SAT-Inspired Eliminations for Superposition
Cites Work
- A feasibly constructive lower bound for resolution proofs
- The intractability of resolution
- Solving satisfiability in less than \(2^ n\) steps
- New methods for 3-SAT decision and worst-case analysis
- Solving Satisfiability with Less Searching
- Propositional proof systems, the consistency of first order theories and the complexity of computations
- The relative efficiency of propositional proof systems
- The Complexity of Propositional Proofs
- Unnamed Item
- Unnamed Item
- Unnamed Item
