License: Creative Commons Attribution-NoDerivs 3.0 Unported license (CC BY-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ICLP.2012.211
URN: urn:nbn:de:0030-drops-36235
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2012/3623/
Go to the corresponding LIPIcs Volume Portal

Andres, Benjamin ; Kaufmann, Benjamin ; Matheis, Oliver ; Schaub, Torsten

Unsatisfiability-based optimization in clasp

pdf-format:
21.pdf (0.4 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{andres_et_al:LIPIcs:2012:3623,
  author =	{Benjamin Andres and Benjamin Kaufmann and Oliver Matheis and Torsten Schaub},
  title =	{{Unsatisfiability-based optimization in clasp}},
  booktitle =	{Technical Communications of the 28th International Conference on Logic Programming (ICLP'12)},
  pages =	{211--221},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-43-9},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{17},
  editor =	{Agostino Dovier and V{\'i}tor Santos Costa},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2012/3623},
  URN =		{urn:nbn:de:0030-drops-36235},
  doi =		{10.4230/LIPIcs.ICLP.2012.211},
  annote =	{Keywords: answer-set-programming, solvers}
}

Keywords: answer-set-programming, solvers
Collection: Technical Communications of the 28th International Conference on Logic Programming (ICLP'12)
Issue Date: 2012
Date of publication: 05.09.2012

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI