Assat: Computing answer set of a logic program by sat solvers

We propose a new translation from normal logic pro-grams with constraints under the answer set semantics to propositional logic. Given a logic program, we show that by adding, for each loop in the program, a cor-responding loop formula to the program’s completion, we obtain a one-to-one correspondence between the an-swer sets of the program and the models of the result-ing propositional theory. Compared with the translation by Ben-Eliyahu and Dechter, ours has the advantage that it does not use any extra variables, and is consider-ably simpler, thus easier to understand. However, in the worst case, it requires computing exponential number of loop formulas. To address this problem, we propose an approach that adds loop formulas a few at a time, selectively. Based on these results, we implemented a system called ASSAT(X), depending on the SAT solver X used, and tested it on a variety of benchmarks includ-ing the graph coloring, the blocks world planning, and Hamiltonian Circuit domains. The results are compared with those by smodels and dlv, and it shows a clear edge of ASSAT(X) over them in these domains