Answer set programming (ASP) is a paradigm for declarative problem solving
where problems are first formalized as rule sets, i.e., answer-set programs, in
a uniform way and then solved by computing answer sets for programs. The
satisfiability modulo theories (SMT) framework follows a similar modelling
philosophy but the syntax is based on extensions of propositional logic rather
than rules. Quite recently, a translation from answer-set programs into
difference logic was provided---enabling the use of particular SMT solvers for
the computation of answer sets.