A Survey of Satisfiability Modulo Theory
From MaRDI portal
Publication:2830018
DOI10.1007/978-3-319-45641-6_26zbMath1453.68116arXiv1606.04786OpenAlexW2433853642MaRDI QIDQ2830018
Publication date: 9 November 2016
Published in: Computer Algebra in Scientific Computing (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1606.04786
Logic in computer science (03B70) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Computational aspects of satisfiability (68R07)
Related Items (4)
An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis ⋮ Computing optimal hypertree decompositions with SAT ⋮ An interleaved depth-first search method for the linear optimization problem with disjunctive constraints ⋮ A posthumous contribution by Larry Wos: excerpts from an unpublished column
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Cuts from proofs: a complete and practical technique for solving linear inequalities over integers
- Deciding floating-point logic with abstract conflict driven clause learning
- The intractability of resolution
- Representing polynomials by positive linear functions on compact convex polyhedra
- Solving systems of polynomial inequalities in subexponential time
- Anneaux preordonnes
- Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
- An interpolating theorem prover
- Polyhedral Approximation of Multivariate Polynomials Using Handelman’s Theorem
- Generating Non-linear Interpolants by Semidefinite Programming
- Solving Non-linear Arithmetic
- Optimization in SMT with ${\mathcal LA}$ (ℚ) Cost Functions
- A Model-Constructing Satisfiability Calculus
- Playing in the grey area of proofs
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- Applying Linear Quantifier Elimination
- Invariant Generation through Strategy Iteration in Succinctly Represented Control Flow Graphs
- SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
- Natural Domain SMT: A Preliminary Assessment
- Generalizing DPLL to Richer Logics
- On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure
- A Decision Procedure for the First Order Theory of Real Addition with Order
- Symbolic execution and program testing
- Linear Programming
- A BLAS based C library for exact linear algebra on integer matrices
- Proof Tree Preserving Interpolation
- A Quantifier Elimination Algorithm for Linear Real Arithmetic
- Fast LCF-Style Proof Reconstruction for Z3
- Linear Quantifier Elimination as an Abstract Decision Procedure
- Lazy Abstraction with Interpolants
- Algorithms in real algebraic geometry
This page was built for publication: A Survey of Satisfiability Modulo Theory
