DROPS

Document

DOI: 10.4230/LIPIcs.ICLP.2012.211

Unsatisfiability-based optimization in clasp

Authors: Benjamin Andres, Benjamin Kaufmann, Oliver Matheis, and Torsten Schaub

Published in: LIPIcs, Volume 17, Technical Communications of the 28th International Conference on Logic Programming (ICLP'12) (2012)

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.

Cite as

Benjamin Andres, Benjamin Kaufmann, Oliver Matheis, and Torsten Schaub. Unsatisfiability-based optimization in clasp. In Technical Communications of the 28th International Conference on Logic Programming (ICLP'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 17, pp. 212-221, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

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

Search Results

Documents authored by Matheis, Oliver

Unsatisfiability-based optimization in clasp

Abstract

Cite as

Thanks for your feedback!

Could not send message