Encoding Redundancy for Satisfaction-Driven Clause Learning

DOI10.1007/978-3-030-17462-0_3MaRDI QIDQ6091331zbMATH OpenOpenAlexFDO

Authors Marijn J. H. Heule, Benjamin Kiesl, Armin Biere

Publication date 24 November 2023

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-17462-0_3

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• scientific article; zbMATH DE number 2243370
• On the power of clause-learning SAT solvers as resolution engines
• Extended clause learning
• Short proofs without new variables
• Clause vivification by unit propagation in CDCL SAT solvers

Cited in

(10)

• Covered clauses are not propagation redundant
• Clause size reduction with all-UIP learning
• Truth assignments as conditional autarkies
• Simple and Efficient Clause Subsumption with Feature Vector Indexing
• Theory and Applications of Satisfiability Testing
• scientific article; zbMATH DE number 2243370 (Why is no real title available?)
• Never trust your solver: certification for SAT and QBF
• Lower bounds for set-blocked clauses proofs
• Improving and understanding the power of satisfaction-driven clause learning
• Extended resolution clause learning via dual implication points

This page was built for publication: Encoding Redundancy for Satisfaction-Driven Clause Learning

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