Answer Set Enumeration via Assumption Literals

摘要

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 non-trivial. 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.