Bitwuzla

DOI10.1007/978-3-031-37703-7_1MaRDI QIDQ6535525zbMATH OpenFDO

Authors Aina Niemetz, Mathias Preiner

Publication date 12 January 2024

Copyright license Creative Commons Attribution 4.0 International

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

• Towards bit-width-independent proofs in SMT solvers
• Synthesis of domain specific CNF encoders for bit-vector solvers
• A Tutorial on Satisfiability Modulo Theories
• Satisfiability modulo theories
• Solving quantified bit-vector formulas using binary decision diagrams

Cites work

• scientific article; zbMATH DE number 5613976 (Why is no real title available?)
• scientific article; zbMATH DE number 1033831 (Why is no real title available?)
• scientific article; zbMATH DE number 1903356 (Why is no real title available?)
• A Decision Procedure for Bit-Vectors and Arrays
• Bitwuzla
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Counterexample-Guided Model Synthesis
• Propagation based local search for bit-precise reasoning
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• The MathSAT5 SMT solver

Cited in

(1)

• Bitwuzla

This page was built for publication: Bitwuzla

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