Bitwuzla

DOI10.1007/978-3-031-37703-7_1zbMATH Open1545.68123MaRDI QIDQ6535525FDOQ6535525

Authors: Aina Niemetz, Mathias Preiner 

Publication date: 12 January 2024

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

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)

Cites Work

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

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)