On incremental core-guided MaxSAT solving

Xujie Si, Xin Zhang, Vasco Manquinho, Mikoláš Janota, Alexey Ignatiev, Mayur Naik

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

3 Citations (Scopus)

Abstract

This paper aims to improve the efficiency of unsat coreguided MaxSAT solving on a sequence of similar problem instances. In particular, we consider the case when the sequence is constructed by adding new hard or soft clauses. Our approach is akin to the well-known idea of incremental SAT solving. However, we show that there are important differences between incremental SAT and incremental MaxSAT, where a straightforward implementation may lead to a sharp decrease in performance. We present alternatives that enable to cope with such issues. The presented algorithm is implemented and evaluated on practical problems. It solves more instances and yields an average speedup of 1.8× on previously solvable instances.

Original languageEnglish
Title of host publicationPrinciples and Practice of Constraint Programming
Subtitle of host publication22nd International Conference, CP 2016 Toulouse, France, September 5–9, 2016 Proceedings
EditorsMichel Rueher
Place of PublicationCham Switzerland
PublisherSpringer
Pages473-482
Number of pages10
ISBN (Electronic)9783319449531
ISBN (Print)9783319449524
DOIs
Publication statusPublished - 2016
Externally publishedYes
EventInternational Conference on Principles and Practice of Constraint Programming 2016 - Toulouse, France
Duration: 5 Sep 20169 Sep 2016
Conference number: 22d
http://cp2016.a4cp.org/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume9892
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceInternational Conference on Principles and Practice of Constraint Programming 2016
Abbreviated titleCP 2016
CountryFrance
CityToulouse
Period5/09/169/09/16
Internet address

Keywords

  • Conjunctive Normal Form
  • Incremental Algorithm
  • Conjunctive Normal Form Formula
  • Soft Clause
  • Abstraction Refinement

Cite this