satisfiability modulo theories
In plain wordsAn extension of logic-puzzle solving that also understands arithmetic, arrays and other data types, so it can check whether conditions in software, such as 'x + y > 10 and x < 3', can ever be met.
The problem of deciding whether a formula of first-order logicfirst-order logic, n.: A precise formal language for statements about objects and their relations, using 'for all' and 'there exists', such as 'every person has a mother'. It is the standard logic of mathematics and of classic AI. is satisfiable with respect to background theories that fix the meaning of certain symbols — linear integer or real arithmetic, bit-vectors, arrays, uninterpreted functions, strings, floating point — and, by extension, the solvers that do so. Most SMT solvers use the DPLL(T) architecture: a conflict-driven SATBoolean satisfiability problem, n.: The puzzle of deciding whether a set of true-or-false conditions can all be met at once. It is famously hard in theory, yet modern solvers routinely handle millions of conditions. engine searches over the formula's Boolean structure, while specialized theory solvers check the consistency of the chosen literals and explain conflicts back to it. Solvers such as Z3, cvc5, Yices and MathSAT, exchanging problems in the SMT-LIB format, are back ends for program verifiers, symbolic execution, test generation, smart-contract analysis and verification of neural networks; language-modellarge language model, n.: A computer program trained on enormous amounts of text to predict the words that come next. At vast scale, that simple skill lets it chat, answer questions, translate, summarize and write code. agents increasingly call them as toolstool use, n.: An AI model's ability to reach beyond its own knowledge by operating outside tools — searching the web, running code, using a calculator or an app — and folding the results into its work. for exact constraint reasoning.
The SMT solver produced a concrete input that overflows the buffer, so the bug report includes a test case.
Origin
Grew from decision procedures for combining theories by Greg Nelson and Derek Oppen (1979) and Robert Shostak (1984). The name and the DPLL(T) framework took shape in the early 2000s, the SMT-LIB standard and the annual SMT-COMP competition followed in the mid-2000s, and Leonardo de Moura and Nikolaj Bjørner described Microsoft Research's Z3 in 2008.
Related
- Boolean satisfiability problemBoolean satisfiability problem, n.: The puzzle of deciding whether a set of true-or-false conditions can all be met at once. It is famously hard in theory, yet modern solvers routinely handle millions of conditions.
- automated theorem provingautomated theorem proving, n.: Getting computers to prove mathematical or logical statements by themselves, by searching for a chain of valid steps that leads from basic assumptions to the statement.
- first-order logicfirst-order logic, n.: A precise formal language for statements about objects and their relations, using 'for all' and 'there exists', such as 'every person has a mother'. It is the standard logic of mathematics and of classic AI.
- formal verificationformal verification, n.: Using mathematics, not just testing, to prove that a computer system always behaves as specified — for example, that a chip never adds wrongly or that a program can never crash in a particular way.
- constraint satisfaction problemconstraint satisfaction problem, n.: A problem in which each item must be given a value so that every rule is obeyed, like filling in a Sudoku, coloring a map so no neighbors match, or building a timetable without clashes.
- LeanLean, prop. n.: A programming language and proof checker in which mathematicians write proofs that the computer verifies line by line. It has become the main language in which AI systems produce checkable proofs.
Sources
- Nelson, G. & Oppen, D. C. (1979). Simplification by Cooperating Decision Procedures. ACM Transactions on Programming Languages and Systems 1(2), 245–257.
- de Moura, L. & Bjørner, N. (2008). Z3: An Efficient SMT Solver. TACAS 2008, LNCS 4963, 337–340.
Mentioned in
automated theorem provingautomated theorem proving, n.: Getting computers to prove mathematical or logical statements by themselves, by searching for a chain of valid steps that leads from basic assumptions to the statement., Boolean satisfiability problemBoolean satisfiability problem, n.: The puzzle of deciding whether a set of true-or-false conditions can all be met at once. It is famously hard in theory, yet modern solvers routinely handle millions of conditions., formal verificationformal verification, n.: Using mathematics, not just testing, to prove that a computer system always behaves as specified — for example, that a chip never adds wrongly or that a program can never crash in a particular way., program synthesisprogram synthesis, n.: Getting a computer to write a program automatically from a description of what the program should do — a logical specification, a few input–output examples or a request in plain language., IsabelleIsabelle, prop. n.: A widely used proof-checking program in which people write mathematics and verified software; it is known for automation that calls other theorem provers to finish routine steps.