SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers

DOI10.1007/978-3-540-79719-7_8zbMath1138.68537OpenAlexW2119144375MaRDI QIDQ3502696

Robert Nieuwenhuis, Enric Rodríguez-Carbonell, Albert Oliveras, Germain Faure

Publication date: 27 May 2008

Published in: Theory and Applications of Satisfiability Testing – SAT 2008 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-79719-7_8

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items (8)

New techniques for linear arithmetic: cubes and equalities ⋮ Reluplex: a calculus for reasoning about deep neural networks ⋮ A computational status update for exact rational mixed integer programming ⋮ A computational status update for exact rational mixed integer programming ⋮ Fast Cube Tests for LIA Constraint Solving ⋮ A Survey of Satisfiability Modulo Theory ⋮ Superposition Modulo Linear Arithmetic SUP(LA) ⋮ Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)

Uses Software

• BarcelogicTools
• CPLEX
• SMT-LIB
• Yices
• GLPK
• cvc3
• z3
• MathSAT

This page was built for publication: SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers