• 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 multi-objective 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 built-in logical theories and their combination. CVC4 is the fourth ... features of CVC3 and SMT-LIBv2 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 SAT-based approach to satisfiability modulo theories (SMT). SMT is the problem of determining ... literals, where T is a first-order theory for which a satisfiability procedure ... design in which an enumerator and a theory-specific 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]
  • floating-point satisfiability solver. The Satisfiability Modulo Theory (SMT) problem over floating-point 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 bit-vectors...
  • 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...