Enhancing disjunctive logic programming systems by SAT checkers

Christoph Koch

doi:10.1016/S0004-3702(03)00078-X

2003-12-01

PRE

Christoph Koch

Nicola Leone

Gerald Pfeifer

DOI：10.1016/S0004-3702(03)00078-X

原文链接

原文求助

摘要

En 中文

Disjunctive logic programming (DLP) with stable model semantics is a powerful nonmonotonic formalism for knowledge representation and reasoning. Reasoning with DLP is harder than with normal (boolean OR-free) logic programs, because stable model checking-deciding whether a given model is a stable model of a propositional DLP program-is co-NP-complete, while it is polynomial for normal logic programs. This paper proposes a new transformation Gamma(M) (P), which reduces stable model checking to UNSAT-i.e., to deciding whether a given CNF formula is unsatisfiable. The stability of a model M of a program P thus can be verified by calling a Satisfiability Checker on the CNF formula Gamma(M) (P). The transformation is parsimonious (i.e., no new symbol is added), and efficiently computable, as it runs in logarithmic space (and therefore in polynomial time). Moreover, the size of the generated CNF formula never exceeds the size of the input (and is usually much smaller). We complement this transformation with modular evaluation results, which allow for efficient handling of large real-world reasoning problems. The proposed approach to stable model checking has been implemented in DLV-a state-of-the-art implementation of DLP. A number of experiments and benchmarks have been run using SATZ as Satisfiability checker. The results of the experiments are very positive and confirm the usefulness of our techniques. (C) 2003 Elsevier B.V. All rights reserved.

Keyword:

disjunctive logic programming

nonmonotonic reasoning

head-cycle-free programs

answer set programs

stable model checking