Modern, efficient Answer Set Programming solvers implement answer set search via non-chronological backtracking algorithms. The extension of these algorithms to answer set enumeration is nontrivial. In fact, adding blocking constraints to discard already computed answer sets is inadequate because the introduced constraints may not fit in memory or deteriorate the efficiency of the solver. On the other hand, the algorithm implemented by CLASP, which can run in polynomial space, requires invasive modifications of the answer set search procedure. The algorithm is revised in this paper so as to make it almost independent from the underlying answer set search procedure, provided that the procedure accepts as input a logic program and a list of assumption literals, and returns either an answer set (and associated branching literals) or an unsatisfiable core. The revised algorithm is implemented in wasp, and compared empirically to the state of the art solver CLASP.
Scheda prodotto non validato
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo
|Titolo:||Answer set enumeration via assumption literals|
|Data di pubblicazione:||2016|
|Appare nelle tipologie:||04.01 - Contributo in atti di convegno|