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.

A Backjumping Technique for Disjunctive Logic Programming

FABER, WOLFGANG;LEONE, Nicola
2006-01-01

Abstract

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.
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/130601
 Attenzione

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

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