Abstract 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 (∨-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 Γ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 Γ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.

Enhancing Disjunctive Logic Programming Systems by SAT Checkers

LEONE, Nicola;
2003-01-01

Abstract

Abstract 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 (∨-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 Γ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 Γ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.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/20.500.11770/139357
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 38
  • ???jsp.display-item.citation.isi??? ND
social impact