LP2ATOMIC, LP2LP2, and LP2SAT

These tools translate a normal program into a set of clauses such that any SAT solver can be used to calculate its answer sets. The software is compatible with the intermediate file format of lparse/smodels and can be used with a modern grounder such as gringo. (see the Potassco collection).

Implementation

• There are two mainstream versions based on lp2atomic [Jan06] and lp2lp2 [JN10]. The first tool removes positive conditions from the rules while the second does not.
• Before invoking a SAT solver the tool lp2sat must be called to form the completion of the program in DIMACS format.
• Our normalization tools enable the use of extended rule types (choice rules, cardinality rules, and weight rules) in the input program.
• All tools are available for download here.

Simple Example

The computation of answer sets for program.lp using, e.g., the SAT solver minisat as the back-end:

$ gringo program.lp | lp2atomic | lp2sat > program.cnf
$ gringo program.lp | lp2lp2 | lp2sat > program.cnf
$ minisat program.cnf model.out
$ cat model.out | interpret -p -d program.cnf

The first two lines illustrate the use of either lp2atomic or lp2lp2 for the translation into CNF. After that the SAT solver can be called and any satisfying assignments can be mapped back to answer sets using the tool interpret. To enable this program.cnf contains the required symbolic information as comments. Please refer to the documentation of your SAT solver to see what command line arguments/options are needed for printing the satisfying assignment(s).

Related Publications

LP2ATOMIC

Tomi Janhunen. Some (In)translatability Results for Normal Logic Programs and Propositional Theories. Journal of Applied Non-Classical Logics, 16(1-2), 35-86, 2006. Special issue on implementing logics.

Tomi Janhunen. Representing Normal Programs with Clauses. In R. L. de Mántaras and L. Saitta, editors, the Proceedings of the 16th European Conference on Artificial Intelligence, pages 358-362, Valencia, Spain, August 2004.

Tomi Janhunen. A Counter-Based Approach to Translating Logic Programs into Set of Clauses. In M. de Vos and A. Provetti, editors, the Proceedings of the 2nd International Workshop on Answer Set Programming, pages 166-180, Messina, Sicily, September 2003. Sun SITE Central Europe (CEUR), vol. 78.

Tomi Janhunen. Translatability and Intranslatability Results for Certain Classes of Logic Programs. In the Report Series of the Laboratory for Theoretical Computer Science, Series A, Research Reports, number A82.

LP2LP2

T. Janhunen and I. Niemelä. Compact Translations of Non-Disjunctive Answer Set Programs to Propositional Clauses. In Michael Gelfond's Festschrift, 2010, 111—130. Springer LNCS 6565.