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

5 Citations (Scopus)


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
Number of pages10
ISBN (Electronic)9783319449531
ISBN (Print)9783319449524
Publication statusPublished - 2016
Externally publishedYes
EventInternational Conference on Principles and Practice of Constraint Programming 2016 - Toulouse, France
Duration: 5 Sept 20169 Sept 2016
Conference number: 22d

Publication series

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


ConferenceInternational Conference on Principles and Practice of Constraint Programming 2016
Abbreviated titleCP 2016
Internet address


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

Cite this