Physical Sciences and Mathematics Commons^™

Termination Of Grounding Is Not Preserved By Strongly Equivalent Transformations, Yuliya Lierler, Vladimir Lifschitz

Computer Science Faculty Proceedings & Presentations

The operation of a typical answer set solver begins with grounding—replacing the given program with a program without variables that has the same answer sets. When the given program contains function symbols, the process of grounding may not terminate. In this note we give an example of a pair of consistent, strongly equivalent programs such that one of them can be grounded by LPARSE, DLV, and gringo, and the other cannot.

One More Decidable Class Of Finitely Ground Programs, Yuliya Lierler, Vladimir Lifschitz

Computer Science Faculty Proceedings & Presentations

When a logic program is processed by an answer set solver, the first task is to generate its instantiation. In a recent paper, Calimeri et el. made the idea of efficient instantiation precise for the case of disjunctive programs with function symbols, and introduced the class of “finitely ground” programs that can be efficiently instantiated. Since that class is undecidable, it is important to find its large decidable subsets. In this paper, we introduce such a subset—the class of argumentrestricted programs. It includes, in particular, all finite domain programs, ω-restricted programs, and λ-restricted programs.

Cmodels: Sat-Based Answer Set Programming System, Yuliya Lierler, Marco Maratea

Computer Science Faculty Publications

CMODELS [1, 2] is an answer set programming [3] system that uses the same frontend LPARSE as answer set solver SMODELS (http://www.tcs.hut.fi/Software/smodels/). CMODELS main computational characteristics is that it computes answer sets using a SAT solver for search.

The use of SAT solvers for generating answer sets is based on the fact that for logic programs satisfying syntactic condition, tightness, the answer set semantics is equivalent to the Clark’s completion semantics. In addition, [4] introduced concept of a loop formula, and demonstrated that the answer sets of a logic program are exactly the models of its completion that satisfy the …

Cmodels – Sat-Based Disjunctive Answer Set Solver, Yuliya Lierler

Computer Science Faculty Proceedings & Presentations

Disjunctive logic programming under the stable model semantics [GL91] is a new methodology called answer set programming (ASP) for solving combinatorial search problems. This programming method uses answer set solvers, such as DLV [Lea05], GNT [Jea05], SMODELS [SS05], ASSAT [LZ02], CMODELS [Lie05a]. Systems DLV and GNT are more general as they work with the class of disjunctive logic programs, while other systems cover only normal programs. DLV is uniquely designed to find the answer sets for disjunctive logic programs. On the other hand, GNT first generates possible stable model candidates and then tests the candidate on the minimality using system …

Cmodels For Tight Disjunctive Logic Programs, Yuliya Lierler

Computer Science Faculty Proceedings & Presentations

Disjunctive logic programming under the stable model semantics [GL91] is a new answer set programming (ASP) methodology for solving combinatorial search problems. It is a form of declarative programming related to logic programming languages, such as Prolog, where the solutions to a problem are represented by answer sets, and not by answer substitutions produced in response to a query as in convential logic programming. Instead of Prolog systems, this programming method uses answer set solvers, such as smodels1, smodelscc2, cmodels3, dlv4, and gnt1. These systems made it possible for ASP to be successfully applied in such areas as planning, bounded …

Cmodels-2: Sat-Based Answer Set Solver Enhanced To Non-Tight Programs, Yuliya Lierler, Marco Maratea

Computer Science Faculty Proceedings & Presentations

Answer set programming is a new programming paradigm proposed in [1] and [2], and based on the answer set semantics of Prolog [3]. It is well known that an answer set for a logic program is also a model of the program’s completion [4]. The converse is true when the logic program is “tight” [6, 5]. Lin and Zhao [7] showed that for non-tight programs the models of completion which do not correspond to answer sets can be eliminated by adding to the completion what they called “loop formulas”. Nevertheless, their solver ASSAT¹ has some disadvantages: it can work …