  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. In this paper, the translation is revised for
another SMT fragment, namely that based on fixed-width bit-vector theories.
Thus, even further SMT solvers can be harnessed for the task of computing
answer sets. The results of a preliminary experimental comparison are also
reported. They suggest a level of performance which is similar to that achieved
via difference logic.

Artificial Intelligence;Logic in Computer Science