Expressive Power of SMT
An SMT instance is a generalization of a Boolean SAT instance in which various sets of variables are replaced by predicates from a variety of underlying theories. Obviously, SMT formulas provide a much richer modeling language than is possible with Boolean SAT formulas. For example, an SMT formula allows us to model the datapath operations of a microprocessor at the word rather than the bit level.
By comparison, answer set programming is also based on predicates (more precisely, on atomic sentences created from atomic formula). Unlike SMT, answer-set programs do not have quantifiers, and cannot easily express constraints such as linear arithmetic or difference logic—ASP is at best suitable for boolean problems that reduce to the free theory of uninterpreted functions. Implementing 32-bit integers as bitvectors in ASP suffers from most of the same problems that early SMT solvers faced: "obvious" identities such as x+y=y+x are difficult to deduce.
Constraint logic programming does provide support for linear arithmetic constraints, but within a completely different theoretical framework.
Read more about this topic: Satisfiability Modulo Theories
Famous quotes containing the words expressive and/or power:
“It’s very expressive of myself. I just lump everything in a great heap which I have labeled “the past,” and, having thus emptied this deep reservoir that was once myself, I am ready to continue.”
—Zelda Fitzgerald (1900–1948)
“All goes to show that the soul in man is not an organ, but animates and exercises all the organs; is not a function, like the power of memory, of calculation, of comparison, but uses these as hands and feet; is not a faculty, but a light, is not the intellect or the will, but the master of the intellect and the will; is the background of our being, in which they lie,—an immensity not possessed and that cannot be possessed.”
—Ralph Waldo Emerson (1803–1882)