
OptiMathSAT
 Referenced in 7 articles
[sw32308]
 OptiMathSAT: a tool for optimization modulo theories. Welcome to the home page of OptiMathSAT ... efficient Optimization Modulo Theories (OMT) tool. OptiMathSAT is an extension of MathSAT ... OptiMathSAT allows for incremental multiobjective optimization over linear arithmetic objective functions, it supports...

vZ
 Referenced in 10 articles
[sw22666]
 users to pose and solve optimization problems modulo theories. Many SMT applications use models ... build on top of Z3 to get optimal assignments with respect to objective functions...

CVC4
 Referenced in 107 articles
[sw09485]
 source automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used ... large number of builtin logical theories and their combination. CVC4 is the fourth ... features of CVC3 and SMTLIBv2 while optimizing the design of the core system architecture...

LinAIG
 Referenced in 6 articles
[sw10316]
 capabilities of SMT (Satisfiability Modulo Theories) solvers. Constraint minimization optimizes polyhedra by exploiting the fact...

SYMBA
 Referenced in 11 articles
[sw08528]
 Symbolic optimization with SMT solvers. The rise in efficiency of Satisfiability Modulo Theories (SMT) solvers ... arbitrary satisfying assignment, but one that optimizes (minimizes/maximizes) certain criteria. For example, we might...

MTT
 Referenced in 22 articles
[sw09783]
 tool. Despite the remarkable development of the theory of termination of rewriting, its application ... level programming languages is far from being optimal. This is due to the need ... programmable) strategies for controlling the execution, matching modulo axioms, and so on, that are used ... rewriting relation. In particular, Generalized Rewrite Theories (GRT) are a recent generalization of rewrite theories...

TSAT++
 Referenced in 3 articles
[sw21350]
 lazy SATbased approach to satisfiability modulo theories (SMT). SMT is the problem of determining ... literals, where T is a firstorder theory for which a satisfiability procedure ... design in which an enumerator and a theoryspecific satisfiability checker cooperate in order ... satisfiability checkers for different theories (or combinations of theories), to be plugged...

JavaSMT
 Referenced in 1 article
[sw18525]
 Solvers in Java. Satisfiability Modulo Theory (SMT) solvers received a lot of attention ... offered by SMT solvers such as interpolation, optimization, and formula introspection are not supported...

XSat
 Referenced in 1 article
[sw26290]
 floatingpoint satisfiability solver. The Satisfiability Modulo Theory (SMT) problem over floatingpoint arithmetic ... point satisfiability and a class of mathematical optimization (MO) problems known as unconstrained...

AXIOM
 Referenced in 172 articles
[sw00063]
 Axiom is a general purpose Computer Algebra system...

BARON
 Referenced in 316 articles
[sw00066]
 BARON is a computational system for solving nonconvex...

Boolector
 Referenced in 28 articles
[sw00085]
 Boolector: an efficient SMT solver for bitvectors...

CoCoA
 Referenced in 631 articles
[sw00143]
 CoCoA is a system for Computations in Commutative...

CoCoALib
 Referenced in 56 articles
[sw00144]
 CoCoALib: A C++ library for computations in commutative...

Coq
 Referenced in 1807 articles
[sw00161]
 Coq is a formal proof management system. It...

GAP
 Referenced in 2876 articles
[sw00320]
 GAP is a system for computational discrete algebra...

Macaulay2
 Referenced in 1692 articles
[sw00537]
 Macaulay2 is a software system devoted to supporting...

Magma
 Referenced in 2917 articles
[sw00540]
 Computer algebra system (CAS). Magma is a large...

ManySAT
 Referenced in 32 articles
[sw00544]
 ManySAT: a parallel SAT solver. ManySAT, a new...

Maple
 Referenced in 5124 articles
[sw00545]
 The result of over 30 years of cutting...