On the Configuration of SAT Formulae

Mauro Vallati, Marco Maratea

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 languageEnglish
Title of host publicationAI*IA 2019 – Advances in Artificial Intelligence
Subtitle of host publicationXVIIIth International Conference of the Italian Association for Artificial Intelligence, Rende, Italy, November 19–22, 2019, Proceedings
EditorsMario Alviano, Gianluigi Greco, Francesco Scarcello
Place of PublicationCham
PublisherSpringer Verlag
Pages264-277
Number of pages14
VolumeLNAI 11946
Edition1st
ISBN (Electronic)9783030351663
ISBN (Print)9783030351656
DOIs
Publication statusPublished - 17 Nov 2019
Event18th International Conference of the Italian Association for Artificial Intelligence - University of Calabria, Rende, Italy
Duration: 19 Nov 201922 Nov 2019
Conference number: 18
https://aiia2019.mat.unical.it/

Publication series

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

Conference

Conference18th International Conference of the Italian Association for Artificial Intelligence
Abbreviated titleAIIA 2019
CountryItaly
CityRende
Period19/11/1922/11/19
Internet address

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). Cham: 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’ 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.",
keywords = "SATisfiability, Knowledge configuration, Performance improvement",
author = "Mauro Vallati and Marco Maratea",
year = "2019",
month = "11",
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",
edition = "1st",

}

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 proceedingConference contribution

TY - GEN

T1 - On the Configuration of SAT Formulae

AU - Vallati, Mauro

AU - Maratea, Marco

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 - SATisfiability

KW - Knowledge configuration

KW - Performance improvement

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

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). https://doi.org/10.1007/978-3-030-35166-3_19