A Fast Linear-Arithmetic Solver for DPLL(T)

By Bruno Dutertre, Leonardo de Moura. International Conference on Computer Aided Verification, 2006

774 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Software

View Paper: https://www.semanticscholar.org/paper/e64d79a5c57b1f5c6123f230c5c32281c482aaff

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

In Software

Citations in the corpus

Bounded synthesis (2007, methodology): “In spite of the large size of the resulting constraint system, the synthesis problem remains tractable; Yices solves all resulting constraint systems within a few hours, and within a minutes for small constraint systems with up to 1,000 philosophers.”
The YICES SMT Solver (2006, methodology): “The linear arithmetic solver uses a novel Simplex-based algorithm [5,6].”
Efficient E-Matching for SMT Solvers (2007, neutral): “0 timeout+abort 100 10 1 0.1 600 secs 100 10 1 0.1 < 0.01 Yices 1.0”
Z3: An Efficient SMT Solver (2008, methodology): “Z3 uses a linear arithmetic solver based on the algorithm used in Yices [9].”
Higher Order Mutation Testing (2009, methodology): “SHOM uses the Yices constraint solver [87] to solve these constraints.”
Heuristics for Scalable Dynamic Test Generation (2008, methodology): “The search strategy framework provides primitives for writing a concolic search strategy, such as methods for flipping and solving path constraints using the Yices [7] SMT solver.”
Handbook of Satisfiability (2021, methodology): “This is the strategy followed by the solvers Yices and Z3 [61, 55].”
Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints (2007, methodology): “In addition to the implementation for Boolean satisfiability instances that we have focused on in this paper, we have implemented the algorithms on a solver for disjunctive temporal problems [26] and using YICES [14], an efficient satisfiability modulo theories (SMT) solver that covers a wide range ”
Leveraging linear and mixed integer programming for SMT (2014, methodology): “The best-performing arithmetic theory solvers are based on an algorithm that adapts the well-known simplex method to the SMT setting [1].”
A Decision Procedure for Bit-Vectors and Arrays (2007, methodology): “Performance on large examples is discussed, and there is a comparative evaluation with Yices [9], that is well-known for its efficiency.”
Challenging SMT solvers to verify neural networks (2012, neutral): “…involved in our experimentation are the participants to the QF_LRA track of the SMT Competition 2011 [9], namely CVC [6] (version 4 1.0rc.2026), OPENSMT [10], MATH SAT [8,19] (version 5), SMTI NTERPOL [11] (version 2.0pre), YICES [15] (version 1.0.29, with smtlib2 parser) and Z3 [13] (version 3.0).”
Effective Algorithms for the Satisfiability of Quantifier-Free Formulas Over Linear Real and Integer Arithmetic (2014, methodology): “There are two different simplex implementations in CVC4, one that follows the well-known simplex adapted for SMT described in [46, 47], and one based on sum-of-infeasibilities as described in [73].”
cvc5: A Versatile and Industrial-Strength SMT Solver (2022, methodology): “The linear arithmetic solver [78] extends the simplex procedure adapted for SMT by Dutertre and de Moura [56].”