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:
“Coming on such an ancient human trace
Seems as expressive of the human race
As meeting someone living, face to face.”
—Robert Frost (1874–1963)
“I never saw love as luck, as that gift from the gods which put everything else in place, and allowed you to succeed. No, I saw love as reward. One could find it only after one’s virtue, or one’s courage, or self-sacrifice, or generosity, or loss, has succeeded in stirring the power of creation.”
—Norman Mailer (b. 1923)