cid 2f5fb434fdf8dd3e16f9a239ec97f2be90921905229ca1f97e60c1d5c8d85ebe · original · open access · via wikipedia
Title: Satisfiability modulo theories
Authors:
Venue: Wikipedia
Year: unknown
Canonical: wiki:satisfiability-modulo-theories
URL: https://en.wikipedia.org/wiki/Satisfiability_modulo_theories
Collector: wikipedia
OA: true
ABSTRACT
In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involving real numbers, integers, and/or various data structures such as lists, arrays, bit vectors, and strings. The name is derived from the fact that these expressions are interpreted within ("modulo") a certain formal theory in first-order logic with equality. SMT solvers are tools that aim to solve the SMT problem for a practical subset of inputs. SMT solvers such as Z3 and cvc5 have been used as a building block for a wide range of applications across computer science, including in automated theorem proving, program analysis, program verification, and software testing.