A Backjumping Technique for Disjunctive Logic Programming

In this work we present a backjumping technique for Disjunctive Logic Programming under the Stable Model Semantics (SDLP). It builds upon related techniques that had originally been introduced for constraint solving, which have been adapted to propositional satisfiability testing, and recently also to non-disjunctive logic programming under the stable model semantics (SLP) [1, 2]. We focus on backjumping without clause learning, providing a new theoretical framework for backjumping in SDLP, elaborating on and exploiting peculiarities of the disjunctive setting. We present a reason calculus and associated computations, which - compared to the traditional approaches - reduces the information to be stored, while fully preserving the correctness and the efficiency of the backjumping technique, handling specific aspects of disjunction in a benign way. We implemented the proposed technique in DLV, the state-of-the-art SDLP system. We have conducted several experiments on hard random and structured instances in order to assess the impact of backjumping. To this end, we have compared DLV in various versions: With and without the backjumping method described in this paper, in combination with two different heuristic functions. Our conclusion is that under any of the heuristic functions, DLV with backjumping is favourable to DLV without backjumping. DLV with backjumping performs particularly well on structured satisfiability and quantified boolean formula instances, where the search space and execution time are effectively cut.