Translating Answer-Set Programs into Bit-Vector Logic

Details Translating Answer-Set Programs into Bit-Vector Logic Translating Answer-Set Programs into Bit-Vector Logic

2011-08-30

arxiv.org/abs/1108.5837v1

Computer Science

Artificial Intelligence

12 pages, 1 figure, 3 tables

Scientific paper

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.

Affiliated with

Also associated with

No associations

Rating

Translating Answer-Set Programs into Bit-Vector Logic does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Translating Answer-Set Programs into Bit-Vector Logic, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Translating Answer-Set Programs into Bit-Vector Logic will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-728795