On the Configuration of SAT Formulae

Mauro Vallati; Marco Maratea

doi:10.1007/978-3-030-35166-3_19

On the Configuration of SAT Formulae

Mauro Vallati, Marco Maratea

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

1 Citation (Scopus)

Abstract

It is well-known that the order in which clauses and literals are listed in a SAT formulae can have a strong impact on solvers’ performance. In this work we investigate how the performance of SAT solvers can be improved by a specifically-designed SAT formulae configuration. We introduce a fully automated approach for this configuration task, that considers a number of criteria for optimising the order in which clauses and, within clauses, literals, are listed in a formula expressed using the Conjunctive Normal Form. Our experimental analysis, involving three state-of-the-art SAT solvers and six different benchmark sets, shows that the configurations identified by the proposed approach can have a significant positive impact on solvers’ performance.

Original language	English
Title of host publication	AI*IA 2019 – Advances in Artificial Intelligence
Subtitle of host publication	XVIIIth International Conference of the Italian Association for Artificial Intelligence, Rende, Italy, November 19–22, 2019, Proceedings
Editors	Mario Alviano, Gianluigi Greco, Francesco Scarcello
Place of Publication	Cham
Publisher	Springer Verlag
Pages	264-277
Number of pages	14
Volume	LNAI 11946
Edition	1st
ISBN (Electronic)	9783030351663
ISBN (Print)	9783030351656
DOIs	https://doi.org/10.1007/978-3-030-35166-3_19
Publication status	Published - 17 Nov 2019
Event	18th International Conference of the Italian Association for Artificial Intelligence - University of Calabria, Rende, Italy Duration: 19 Nov 2019 → 22 Nov 2019 Conference number: 18 https://aiia2019.mat.unical.it/

Publication series

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

Conference

Conference	18th International Conference of the Italian Association for Artificial Intelligence
Abbreviated title	AIIA 2019
Country/Territory	Italy
City	Rende
Period	19/11/19 → 22/11/19
Internet address	https://aiia2019.mat.unical.it/

Access to Document

10.1007/978-3-030-35166-3_19Licence: Other

SAT_conf___AIxIA19Accepted author manuscript, 269 KBLicence: Unspecified

Cite this

Vallati, M., & Maratea, M. (2019). On the Configuration of SAT Formulae. In M. Alviano, G. Greco, & F. Scarcello (Eds.), AI*IA 2019 – Advances in Artificial Intelligence: XVIIIth International Conference of the Italian Association for Artificial Intelligence, Rende, Italy, November 19–22, 2019, Proceedings (1st ed., Vol. LNAI 11946, pp. 264-277). (Lecture Notes in Computer Science). Springer Verlag. https://doi.org/10.1007/978-3-030-35166-3_19

Vallati, Mauro ; Maratea, Marco. / On the Configuration of SAT Formulae. AI*IA 2019 – Advances in Artificial Intelligence: XVIIIth International Conference of the Italian Association for Artificial Intelligence, Rende, Italy, November 19–22, 2019, Proceedings. editor / Mario Alviano ; Gianluigi Greco ; Francesco Scarcello. Vol. LNAI 11946 1st. ed. Cham : Springer Verlag, 2019. pp. 264-277 (Lecture Notes in Computer Science).

@inproceedings{d452adbda80448068b1dc380d4bee7ab,

title = "On the Configuration of SAT Formulae",

abstract = "It is well-known that the order in which clauses and literals are listed in a SAT formulae can have a strong impact on solvers{\textquoteright} performance. In this work we investigate how the performance of SAT solvers can be improved by a specifically-designed SAT formulae configuration. We introduce a fully automated approach for this configuration task, that considers a number of criteria for optimising the order in which clauses and, within clauses, literals, are listed in a formula expressed using the Conjunctive Normal Form. Our experimental analysis, involving three state-of-the-art SAT solvers and six different benchmark sets, shows that the configurations identified by the proposed approach can have a significant positive impact on solvers{\textquoteright} performance.",

keywords = "Knowledge configuration, Performance improvement, SATisfiability",

author = "Mauro Vallati and Marco Maratea",

year = "2019",

month = nov,

day = "17",

doi = "10.1007/978-3-030-35166-3_19",

language = "English",

isbn = "9783030351656",

volume = "LNAI 11946",

series = "Lecture Notes in Computer Science",

publisher = "Springer Verlag",

pages = "264--277",

editor = "Mario Alviano and Gianluigi Greco and Francesco Scarcello",

booktitle = "AI*IA 2019 – Advances in Artificial Intelligence",

address = "Germany",

edition = "1st",

note = "18th International Conference of the Italian Association for Artificial Intelligence, AIIA 2019 ; Conference date: 19-11-2019 Through 22-11-2019",

url = "https://aiia2019.mat.unical.it/",

}

Vallati, M & Maratea, M 2019, On the Configuration of SAT Formulae. in M Alviano, G Greco & F Scarcello (eds), AI*IA 2019 – Advances in Artificial Intelligence: XVIIIth International Conference of the Italian Association for Artificial Intelligence, Rende, Italy, November 19–22, 2019, Proceedings. 1st edn, vol. LNAI 11946, Lecture Notes in Computer Science, Springer Verlag, Cham, pp. 264-277, 18th International Conference of the Italian Association for Artificial Intelligence, Rende, Italy, 19/11/19. https://doi.org/10.1007/978-3-030-35166-3_19

On the Configuration of SAT Formulae. / Vallati, Mauro; Maratea, Marco.

AI*IA 2019 – Advances in Artificial Intelligence: XVIIIth International Conference of the Italian Association for Artificial Intelligence, Rende, Italy, November 19–22, 2019, Proceedings. ed. / Mario Alviano; Gianluigi Greco; Francesco Scarcello. Vol. LNAI 11946 1st. ed. Cham : Springer Verlag, 2019. p. 264-277 (Lecture Notes in Computer Science).

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

TY - GEN

T1 - On the Configuration of SAT Formulae

AU - Vallati, Mauro

AU - Maratea, Marco

N1 - Conference code: 18

PY - 2019/11/17

Y1 - 2019/11/17

N2 - It is well-known that the order in which clauses and literals are listed in a SAT formulae can have a strong impact on solvers’ performance. In this work we investigate how the performance of SAT solvers can be improved by a specifically-designed SAT formulae configuration. We introduce a fully automated approach for this configuration task, that considers a number of criteria for optimising the order in which clauses and, within clauses, literals, are listed in a formula expressed using the Conjunctive Normal Form. Our experimental analysis, involving three state-of-the-art SAT solvers and six different benchmark sets, shows that the configurations identified by the proposed approach can have a significant positive impact on solvers’ performance.

AB - It is well-known that the order in which clauses and literals are listed in a SAT formulae can have a strong impact on solvers’ performance. In this work we investigate how the performance of SAT solvers can be improved by a specifically-designed SAT formulae configuration. We introduce a fully automated approach for this configuration task, that considers a number of criteria for optimising the order in which clauses and, within clauses, literals, are listed in a formula expressed using the Conjunctive Normal Form. Our experimental analysis, involving three state-of-the-art SAT solvers and six different benchmark sets, shows that the configurations identified by the proposed approach can have a significant positive impact on solvers’ performance.

KW - Knowledge configuration

KW - Performance improvement

KW - SATisfiability

UR - http://www.scopus.com/inward/record.url?scp=85076770280&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-35166-3_19

DO - 10.1007/978-3-030-35166-3_19

M3 - Conference contribution

SN - 9783030351656

VL - LNAI 11946

T3 - Lecture Notes in Computer Science

SP - 264

EP - 277

BT - AI*IA 2019 – Advances in Artificial Intelligence

A2 - Alviano, Mario

A2 - Greco, Gianluigi

A2 - Scarcello, Francesco

PB - Springer Verlag

CY - Cham

T2 - 18th International Conference of the Italian Association for Artificial Intelligence

Y2 - 19 November 2019 through 22 November 2019

ER -

Vallati M, Maratea M. On the Configuration of SAT Formulae. In Alviano M, Greco G, Scarcello F, editors, AI*IA 2019 – Advances in Artificial Intelligence: XVIIIth International Conference of the Italian Association for Artificial Intelligence, Rende, Italy, November 19–22, 2019, Proceedings. 1st ed. Vol. LNAI 11946. Cham: Springer Verlag. 2019. p. 264-277. (Lecture Notes in Computer Science). Epub 2019 Nov 12. doi: 10.1007/978-3-030-35166-3_19

On the Configuration of SAT Formulae

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this