Mixed integer programming methods for computing nonmonotonic deductive databases

TLDR

While the declarative semantics of explicit and nonmonotonic negation in logic programs have been extensively studied, little work has addressed their computation and implementation, and mixed integer programming offers a fully declarative approach that gracefully reuses prior computations. The paper studies three mixed integer linear programming approaches for computing stable models of logic programs, presents algorithms for answer sets under simultaneous classical and nonmonotonic negation, and evaluates their relative efficiency. They implement a prototype compiler that uses mixed integer linear programming to encode four explicit negation semantics and to compute answer sets for programs with simultaneous classical and nonmonotonic negation. Experimental results with the prototype compiler confirm the theoretical analysis.

Abstract

Though the declarative semantics of both explicit and nonmonotonic negation in logic programs has been studied extensively, relatively little work has been done on computation and implementation of these semantics. In this paper, we study three different approaches to computing stable models of logic programs based on mixed integer linear programming methods for automated deduction introduced by R. Jeroslow. We subsequently discuss the relative efficiency of these algorithms. The results of experiments with a prototype compiler implemented by us tend to confirm our theoretical discussion. In contrast to resolution, the mixed integer programming methodology is both fully declarative and handles reuse of old computations gracefully. We also introduce, compare, implement, and experiment with linear constraints corresponding to four semantics for “explicit” negation in logic programs: the four-valued annotated semantics [Blair and Subrahmanian 1989], the Gelfond-Lifschitz semantics [1990], the over-determined models [Grant and Subrahmanian 1989], the Gelfond-Lifschitz semantics [1990], the over-determined models [Grant and Subrahmanian 1990], and the classical logic semantics. Gelfond and Lifschitz[1990] argue for simultaneous use of two modes of negation in logic programs, “classical” and “nonmonotonic,” so we give algorithms for computing “answer sets” for such logic programs too.