2005 | OriginalPaper | Buchkapitel
cmodels – SAT-Based Disjunctive Answer Set Solver
verfasst von : Yuliya Lierler
Erschienen in: Logic Programming and Nonmonotonic Reasoning
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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 SMODELS as an inference engine for both tasks. Systems CMODELS and ASSAT use SAT solvers as search engines. They are based on the relationship between the completion semantics [Cla78], loop formulas [LZ02] and answer set semantics for logic programs. Here we present the implementation of a SAT-based algorithm for finding answer sets for disjunctive logic programs within
cmodels
. The work is based on the definition of completion for disjunctive programs [LL03] and the generalisation of loop formulas [LZ02] to the case of disjunctive programs [LL03]. We propose the necessary modifications to the SAT based ASSAT algorithm [LZ02] as well as to the generate and test algorithm from [GLM04] in order to adapt them to the case of disjunctive programs. We implement the algorithms in
cmodels
and demonstrate the experimental results.