On a generalization of extended resolution
From MaRDI portal
Recommendations
- Extended resolution simulates \({\mathsf{DRAT}}\)
- Short proofs are narrow -- resolution made simple
- Short proofs are narrow—resolution made simple
- Upper and lower bounds on the complexity of generalised resolution and generalised constraint satisfaction problems
- Theory and Applications of Satisfiability Testing
Cites work
- scientific article; zbMATH DE number 3583767 (Why is no real title available?)
- scientific article; zbMATH DE number 1113996 (Why is no real title available?)
- scientific article; zbMATH DE number 3313427 (Why is no real title available?)
- A feasibly constructive lower bound for resolution proofs
- New methods for 3-SAT decision and worst-case analysis
- Propositional proof systems, the consistency of first order theories and the complexity of computations
- Solving Satisfiability with Less Searching
- Solving satisfiability in less than \(2^ n\) steps
- The Complexity of Propositional Proofs
- The intractability of resolution
- The relative efficiency of propositional proof systems
Cited in
(35)- On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers
- Extended resolution simulates binary decision diagrams
- New methods for 3-SAT decision and worst-case analysis
- Certified SAT solving with GPU accelerated inprocessing
- Conformant planning as a case study of incremental QBF solving
- On preprocessing techniques and their impact on propositional model counting
- The (D)QBF preprocessor HQSpre -- underlying theory and its implementation
- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
- Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets
- Upper and lower bounds on the complexity of generalised resolution and generalised constraint satisfaction problems
- Expressing symmetry breaking in DRAT proofs
- scientific article; zbMATH DE number 1341621 (Why is no real title available?)
- Simulating strong practical proof systems with extended resolution
- scientific article; zbMATH DE number 7350778 (Why is no real title available?)
- Without loss of satisfaction
- Incremental preprocessing methods for use in BMC
- Contradiction separation based dynamic multi-clause synergized automated deduction
- Generating extended resolution proofs with a BDD-based SAT solver
- Super-blocked clauses
- The resolution of Keller's conjecture
- The resolution of Keller's conjecture
- Generating Extended Resolution Proofs with a BDD-Based SAT Solver
- Non-clausal redundancy properties
- Definability for model counting
- Covered clauses are not propagation redundant
- Truth assignments as conditional autarkies
- Simulating circuit-level simplifications on CNF
- Strong extension-free proof systems
- On Incremental Pre-processing for SMT
- Exploiting resolution-based representations for MaxSAT solving
- SAT-Inspired Eliminations for Superposition
- The packing chromatic number of the infinite square grid is 15
- Blocked clause elimination for QBF
- Present and Future of Practical SAT Solving
- Investigations on autark assignments
This page was built for publication: On a generalization of extended resolution
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1961452)
