Enhancing disjunctive logic programming systems by SAT checkers

摘要

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.