×

Unsatisfiability-based optimization in clasp. (English) Zbl 1281.68204

Dovier, Agostino (ed.) et al., Technical communications of the 28th international conference on logic programming (ICLP 2012), September 4–8, 2012, Budapest, Hungary. Papers based on the presentations at the conference. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-43-9). LIPIcs – Leibniz International Proceedings in Informatics 17, 211-221, electronic only (2012).
Summary: Answer set programming (ASP) features effective optimization capacities based on branch-and-bound algorithms. Unlike this, in the area of satisfiability testing (SAT) the finding of minimum unsatisfiable cores was put forward as an alternative approach to solving maximum satisfiability (MaxSAT) problems. We explore this alternative approach to optimization in the context of ASP. To this end, we extended the ASP solver clasp with optimization components based upon the computation of minimal unsatisfiable cores. The resulting system, unclasp, is based on an extension of the well-known algorithms msu1 and msu3 and tailored to the characteristics of ASP. We evaluate our system on multi-criteria optimization problems stemming from realistic Linux package configuration problems. In fact, the ASP-based Linux configuration system aspuncud relies on unclasp and won four out of seven tracks at the 2011 MISC competition.
For the entire collection see [Zbl 1253.68010].

MSC:

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68T27 Logic in artificial intelligence

Software:

Asparagus
PDFBibTeX XMLCite
Full Text: DOI