On incremental core-guided MaxSAT solving

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

doi:10.1007/978-3-319-44953-1_30

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 proceeding › Conference Paper › Research › peer-review

6 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 language	English
Title of host publication	Principles and Practice of Constraint Programming
Subtitle of host publication	22nd International Conference, CP 2016 Toulouse, France, September 5–9, 2016 Proceedings
Editors	Michel Rueher
Place of Publication	Cham Switzerland
Publisher	Springer
Pages	473-482
Number of pages	10
ISBN (Electronic)	9783319449531
ISBN (Print)	9783319449524
DOIs	https://doi.org/10.1007/978-3-319-44953-1_30
Publication status	Published - 2016
Externally published	Yes
Event	International Conference on Principles and Practice of Constraint Programming 2016 - Toulouse, France Duration: 5 Sept 2016 → 9 Sept 2016 Conference number: 22d http://cp2016.a4cp.org/

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	9892
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	International Conference on Principles and Practice of Constraint Programming 2016
Abbreviated title	CP 2016
Country/Territory	France
City	Toulouse
Period	5/09/16 → 9/09/16
Internet address	http://cp2016.a4cp.org/

Keywords

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

Access to Document

10.1007/978-3-319-44953-1_30

Cite this

Si, X., Zhang, X., Manquinho, V., Janota, M., Ignatiev, A., & Naik, M. (2016). On incremental core-guided MaxSAT solving. In M. Rueher (Ed.), Principles and Practice of Constraint Programming: 22nd International Conference, CP 2016 Toulouse, France, September 5–9, 2016 Proceedings (pp. 473-482). (Lecture Notes in Computer Science; Vol. 9892 ). Springer. https://doi.org/10.1007/978-3-319-44953-1_30

@inproceedings{ecd3bba75bed4185b57569bba746159e,

title = "On incremental core-guided MaxSAT solving",

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.",

keywords = "Conjunctive Normal Form, Incremental Algorithm, Conjunctive Normal Form Formula, Soft Clause, Abstraction Refinement",

author = "Xujie Si and Xin Zhang and Vasco Manquinho and Mikol{\'a}{\v s} Janota and Alexey Ignatiev and Mayur Naik",

year = "2016",

doi = "10.1007/978-3-319-44953-1\_30",

language = "English",

isbn = "9783319449524",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "473--482",

editor = "Michel Rueher",

booktitle = "Principles and Practice of Constraint Programming",

address = "Switzerland",

note = "International Conference on Principles and Practice of Constraint Programming 2016, CP 2016 ; Conference date: 05-09-2016 Through 09-09-2016",

url = "http://cp2016.a4cp.org/",

}

Si, X, Zhang, X, Manquinho, V, Janota, M, Ignatiev, A & Naik, M 2016, On incremental core-guided MaxSAT solving. in M Rueher (ed.), Principles and Practice of Constraint Programming: 22nd International Conference, CP 2016 Toulouse, France, September 5–9, 2016 Proceedings. Lecture Notes in Computer Science, vol. 9892 , Springer, Cham Switzerland, pp. 473-482, International Conference on Principles and Practice of Constraint Programming 2016, Toulouse, France, 5/09/16. https://doi.org/10.1007/978-3-319-44953-1_30

On incremental core-guided MaxSAT solving. / Si, Xujie; Zhang, Xin; Manquinho, Vasco et al.
Principles and Practice of Constraint Programming: 22nd International Conference, CP 2016 Toulouse, France, September 5–9, 2016 Proceedings. ed. / Michel Rueher. Cham Switzerland: Springer, 2016. p. 473-482 (Lecture Notes in Computer Science; Vol. 9892 ).

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research › peer-review

TY - GEN

T1 - On incremental core-guided MaxSAT solving

AU - Si, Xujie

AU - Zhang, Xin

AU - Manquinho, Vasco

AU - Janota, Mikoláš

AU - Ignatiev, Alexey

AU - Naik, Mayur

N1 - Conference code: 22d

PY - 2016

Y1 - 2016

N2 - 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.

AB - 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.

KW - Conjunctive Normal Form

KW - Incremental Algorithm

KW - Conjunctive Normal Form Formula

KW - Soft Clause

KW - Abstraction Refinement

UR - https://www.scopus.com/pages/publications/84986213310

U2 - 10.1007/978-3-319-44953-1_30

DO - 10.1007/978-3-319-44953-1_30

M3 - Conference Paper

SN - 9783319449524

T3 - Lecture Notes in Computer Science

SP - 473

EP - 482

BT - Principles and Practice of Constraint Programming

A2 - Rueher, Michel

PB - Springer

CY - Cham Switzerland

T2 - International Conference on Principles and Practice of Constraint Programming 2016

Y2 - 5 September 2016 through 9 September 2016

ER -

Si X, Zhang X, Manquinho V, Janota M, Ignatiev A, Naik M. On incremental core-guided MaxSAT solving. In Rueher M, editor, Principles and Practice of Constraint Programming: 22nd International Conference, CP 2016 Toulouse, France, September 5–9, 2016 Proceedings. Cham Switzerland: Springer. 2016. p. 473-482. (Lecture Notes in Computer Science). doi: 10.1007/978-3-319-44953-1_30

On incremental core-guided MaxSAT solving

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Cite this