## ASSAT: computing answer sets of a logic program by SAT solvers.(English)Zbl 1085.68544

Summary: We propose a new translation from normal logic programs with constraints under the answer set semantics to propositional logic. Given a normal logic program, we show that by adding, for each loop in the program, a corresponding loop formula to the program’s completion, we obtain a one-to-one correspondence between the answer sets of the program and the models of the resulting propositional theory. In the worst case, there may be an exponential number of loops in a logic program. To address this problem, we propose an approach that adds loop formulas a few at a time, selectively. Based on these results, we implement a system called ASSAT(X), depending on the SAT solver X used, for computing one answer set of a normal logic program with constraints. We test the system on a variety of benchmarks including the graph coloring, the blocks world planning, and Hamiltonian Circuit domains. Our experimental results show that in these domains, for the task of generating one answer set of a normal logic program, our system has a clear edge over the state-of-art answer set programming systems Smodels and DLV.

### MSC:

 68N17 Logic programming 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

### Software:

Cmodels; ASSAT; Chaff; Smodels
Full Text:

### References:

 [1] Apt, K.R; Blair, H.A; Walker, A, Towards a theory of declarative knowledge, (), 293-322 [2] Babovich, Y; Erdem, E; Lifschitz, V, Fages’ theorem and answer set programming, () [3] Ben-Eliyahu, R; Dechter, R, Propositional semantics for disjunctive logic programs, Ann. math. artificial intelligence, 12, 53-87, (1996) · Zbl 0858.68012 [4] Cheeseman, P; Kanefsky, B; Taylor, W.M, Where the really hard problems are, (), 331-337 · Zbl 0747.68064 [5] Clark, K.L, Negation as failure, (), 293-322 [6] Fages, F, Consistency of Clark’s completion and existence of stable of stable models, J. methods logic comput. sci., 1, 51-60, (1994) [7] Gelfond, M; Lifschitz, V, The stable model semantics for logic programming, (), 1070-1080 [8] Huang, G.-S; Jia, X; Liau, C.-J; You, J.-H, Two-literal logic programs and satisfiability representation of stable models: a comparison, (), 119-131 · Zbl 1048.68599 [9] Lee, J, Nondefinite vs. definite causal theories, (), 141-153 · Zbl 1122.68626 [10] Lee, J; Lifschitz, V, Loop formulas for disjunctive logic programs, (), 451-465 · Zbl 1204.68056 [11] Lee, J; Lin, F, Loop formulas for circumscription, (), in press · Zbl 1131.68105 [12] Leone, N, DLV: a disjunctive Datalog system, (2001), release 2001-6-11. At [13] Li, C.M; Anbulagan, Heuristics based on unit propagation for satisfiability problems, (), 366-371 [14] Lierler, Y; Maratea, M, Cmodels-2: SAT-based answer set solver enhanced to non-tight programs, (), 346-350 · Zbl 1122.68377 [15] Lin, F; Zhao, Y, ASSAT: computing answer sets of a logic program by sat solvers, (), 112-118 [16] McCain, N; Turner, H, Causal theories of action and change, (), 460-465 [17] Moskewicz, M; Madigan, C; Zhao, Y; Zhang, L; Malik, S, Chaff: engineering an efficient SAT solver, (), 530-535 [18] Niemelä, I, Logic programs with stable model semantics as a constraint programming paradigm, Ann. math. artificial intelligence, 25, 3-4, 241-273, (1999) · Zbl 0940.68018 [19] Selman, B; Kautz, H.A; Cohen, B, Noise strategies for improving local search, (), 337-343 [20] Silva, J.P.M; Sakallah, K.A, GRASP—A new search algorithm for satisfiability, (), 220-227 [21] Simons, P, Smodels: A system for computing the stable models of logic programs, (2000), version 2.25. At [22] Tarjan, R, Depth-first search and linear graph algorithms, SIAM J. comput., 1, 146-160, (1972) · Zbl 0251.05107 [23] B. Vandegriend, Finding Hamiltonian Cycles: algorithms, graphs and performance, MSc Thesis, Department of Computer Science, University of Alberta, 1998 · Zbl 0910.68085 [24] You, J; Cartwright, R; Li, M, Iterative belief revision in extended logic programs, Theoret. comput. sci., 170, (1996) · Zbl 0874.68044 [25] Zhang, H; Stickel, M.E, Implementing the Davis-Putnam method, J. automat. reasoning, 24, 1/2, 277-296, (2000) · Zbl 0967.68148
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.