SMT For Undecidable Theories
Most of the common SMT approaches support decidable theories. However, many real-world systems can only be modelled by means of non-linear arithmetic over the real numbers involving transcendental functions, e.g. an aircraft and its behavior. This fact motivates an extension of the SMT problem to non-linear theories, e.g. determine whether
where
is satisfiable. Then, such problems become undecidable in general. (It is important to note, however, that the theory of real closed fields, and thus the full first order theory of the real numbers, are decidable using quantifier elimination. This is due to Alfred Tarski.) The first order theory of the natural numbers with addition (but not multiplication), called Presburger arithmetic, is also decidable. Since multiplication by constants can be implemented as nested additions, the arithmetic in many computer programs can be expressed using Presburger arithmetic, resulting in decidable formulas.
Examples of SMT solvers addressing Boolean combinations of theory atoms from undecidable arithmetic theories over the reals are ABsolver, which employs a classical DPLL(T) architecture with a non-linear optimization packet as (necessarily incomplete) subordinate theory solver, and iSAT, building on a unification of DPLL SAT-solving and interval constraint propagation called the iSAT algorithm.
Read more about this topic: Satisfiability Modulo Theories
Famous quotes containing the word theories:
“The two most far-reaching critical theories at the beginning of the latest phase of industrial society were those of Marx and Freud. Marx showed the moving powers and the conflicts in the social-historical process. Freud aimed at the critical uncovering of the inner conflicts. Both worked for the liberation of man, even though Marx’s concept was more comprehensive and less time-bound than Freud’s.”
—Erich Fromm (1900–1980)