Extended Resolution Proofs for Symbolic SAT Solving with Quantification

DOI10.1007/11814948_8MaRDI QIDQ5756562zbMATH OpenOpenAlexFDO

Authors Toni Jussila, Carsten Sinz, Armin Biere

Publication date 4 September 2007

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11814948_8

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Generating extended resolution proofs with a BDD-based SAT solver
• Extended Resolution Proofs for Conjoining BDDs
• Symbolic techniques in satisfiability solving
• Theory and Applications of Satisfiability Testing
• Principles and Practice of Constraint Programming – CP 2004

Cited in

(15)

• Generating extended resolution proofs with a BDD-based SAT solver
• Dual proof generation for quantified Boolean formulas with a BDD-based solver
• Simulating strong practical proof systems with extended resolution
• Solution validation and extraction for QBF preprocessing
• Extracting unsatisfiable cores for LTL via temporal resolution
• Functional encryption for inner product with full function privacy
• NAE-resolution: A new resolution refutation technique to prove not-all-equal unsatisfiability
• Extended Resolution Proofs for Conjoining BDDs
• Enhancing unsatisfiable cores for LTL with information on temporal relevance
• Compressing propositional refutations
• Generating Extended Resolution Proofs with a BDD-Based SAT Solver
• Extended clause learning
• Clausal proofs for pseudo-Boolean reasoning
• Making \(\mathsf{IP}=\mathsf{PSPACE}\) practical: efficient interactive protocols for BDD algorithms
• Symbolic techniques in satisfiability solving

Describes a project that uses

Uses Software

• MiniSat
• SBSAT
• Chaff
• BerkMin
• Velev SAT Benchmarks

This page was built for publication: Extended Resolution Proofs for Symbolic SAT Solving with Quantification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5756562)