Extended Resolution Proofs for Symbolic SAT Solving with Quantification

DOI10.1007/11814948_8zbMath1187.68550OpenAlexW1720224351MaRDI QIDQ5756562

Armin Biere, Carsten Sinz, Toni Jussila

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)

Related Items

Extracting unsatisfiable cores for LTL via temporal resolution ⋮ Solution validation and extraction for QBF preprocessing ⋮ Generating Extended Resolution Proofs with a BDD-Based SAT Solver ⋮ Extended clause learning ⋮ Simulating strong practical proof systems with extended resolution ⋮ Enhancing unsatisfiable cores for LTL with information on temporal relevance ⋮ Compressing Propositional Refutations ⋮ Functional Encryption for Inner Product with Full Function Privacy ⋮ Generating extended resolution proofs with a BDD-based SAT solver ⋮ Dual proof generation for quantified Boolean formulas with a BDD-based solver

Uses Software

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