A Tool for Advanced Correspondence Checking in Answer-Set Programming: Preliminary Experimental Results.
Johannes Oetsch, Martina Seidl, Hans Tompits, Stefan Woltran · WLP · 2006
The class of nonmonotonic logic programs under the answer-set semantics [5], with which we are dealing with in this paper, represents the canonical and, due to the availability of efficient answer-set solvers, arguably most widely used approach to answer-set programming (ASP). The latter is based on the idea that problems are encoded in terms of theories such that the solutions of a given problem are determined by the models (“answer sets”) of the corresponding theory. In previous work [4], a general framework for specifying correspondences between logic programs under the answer-set semantics has been introduced. Hereby, the correspondence of two programs is determined in terms of a class C of context programs and a comparison relation ρ such that correspondence between two programs, P and Q, holds iff the answer sets of P ∪R and Q ∪R satisfy ρ, for any program R ∈ C. The framework includes, as special instances, the well-known notions of strong equivalence [8], uniform equivalence [3], and the practicably important case of program comparison under projected answer sets. For the case of propositional disjunctive logic programs, correspondence checking in the above framework under projected answer sets is surprisingly hard, viz. Π 4 -complete in general [4], i.e., lying on the fourth level of the polynomial hierarchy. For computing such program correspondences, efficient reductions to quantified propositional logic have been developed [11]. More specifically, two kinds of reductions, S[·] and T [·], are introduced, where T [·] can be seen as an explicit optimization of S[·]. In this paper, we report about an implementation of these reductions, which we refer to as the system eqcheck, and about initial experimental results. We recall that quantified propositional logic is an extension of classical propositional logic characterised by the condition that its sentences, usually referred to as quantified Boolean formulas (QBFs), are permitted to contain quantifications over atomic formulas. The rationale to consider a reduction approach to QBFs is twofold: (i) complexity results about quantified propositional logic imply that decision problems from the polynomial hierarchy can be efficiently represented in terms of QBFs, and (ii) several practicably efficient solvers for quantified propositional logic are currently available. Indeed, eqcheck uses such solvers as back-end inference engines.