SAT-based formula simplification

Alexey Ignatiev; Alessandro Previti; Joao Marques-Silva

doi:10.1007/978-3-319-24318-4_21

SAT-based formula simplification

Alexey Ignatiev, Alessandro Previti, Joao Marques-Silva

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

12 Citations (Scopus)

Abstract

The problem of propositional formula minimization can be traced to the mid of the last century, to the seminal work of Quine and McCluskey, with a large body of work ensuing from this seminal work. Given a set of implicants (or implicates) of a formula, the goal for minimization is to find a smallest set of prime implicants (or implicates) equivalent to the original formula. This paper considers the more general problem of computing a smallest prime representation of a non-clausal propositional formula, which we refer to as formula simplification. Moreover, the paper proposes a novel, entirely SAT-based, approach for the formula simplification problem. The original problem addressed by the Quine-McCluskey procedure can thus be viewed as a special case of the problem addressed in this paper. Experimental results, obtained on wellknown representative problem instances, demonstrate that a SAT-based approach for formula simplification is a viable alternative to existing implementations of the Quine-McCluskey procedure.

Original language	English
Title of host publication	Theory and Applications of Satisfiability Testing – SAT 2015
Subtitle of host publication	18th International Conference Austin, TX, USA, September 24–27, 2015 Proceedings
Editors	Marijn Heule, Sean Weaver
Place of Publication	Cham Switzerland
Publisher	Springer
Pages	287-298
Number of pages	12
ISBN (Electronic)	9783319243184
ISBN (Print)	9783319243177
DOIs	https://doi.org/10.1007/978-3-319-24318-4_21
Publication status	Published - 2015
Externally published	Yes
Event	International Conference on Theory and Applications of Satisfiability Testing 2015 - Austin, United States of America Duration: 24 Sept 2015 → 27 Sept 2015 Conference number: 18th https://www.cs.utexas.edu/~marijn/sat15/

Publication series

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

Conference

Conference	International Conference on Theory and Applications of Satisfiability Testing 2015
Abbreviated title	SAT 2015
Country/Territory	United States of America
City	Austin
Period	24/09/15 → 27/09/15
Internet address	https://www.cs.utexas.edu/~marijn/sat15/

Keywords

Boolean Function
Conjunctive Normal Form
Disjunctive Normal Form
Propositional Formula
Conjunctive Normal Form Formula

Access to Document

10.1007/978-3-319-24318-4_21

Cite this

Ignatiev, A., Previti, A., & Marques-Silva, J. (2015). SAT-based formula simplification. In M. Heule, & S. Weaver (Eds.), Theory and Applications of Satisfiability Testing – SAT 2015: 18th International Conference Austin, TX, USA, September 24–27, 2015 Proceedings (pp. 287-298). (Lecture Notes in Computer Science; Vol. 9340). Springer. https://doi.org/10.1007/978-3-319-24318-4_21

@inproceedings{f8a0cc92200a49378ef2769cdbde2560,

title = "SAT-based formula simplification",

abstract = "The problem of propositional formula minimization can be traced to the mid of the last century, to the seminal work of Quine and McCluskey, with a large body of work ensuing from this seminal work. Given a set of implicants (or implicates) of a formula, the goal for minimization is to find a smallest set of prime implicants (or implicates) equivalent to the original formula. This paper considers the more general problem of computing a smallest prime representation of a non-clausal propositional formula, which we refer to as formula simplification. Moreover, the paper proposes a novel, entirely SAT-based, approach for the formula simplification problem. The original problem addressed by the Quine-McCluskey procedure can thus be viewed as a special case of the problem addressed in this paper. Experimental results, obtained on wellknown representative problem instances, demonstrate that a SAT-based approach for formula simplification is a viable alternative to existing implementations of the Quine-McCluskey procedure.",

keywords = "Boolean Function, Conjunctive Normal Form, Disjunctive Normal Form, Propositional Formula, Conjunctive Normal Form Formula",

author = "Alexey Ignatiev and Alessandro Previti and Joao Marques-Silva",

year = "2015",

doi = "10.1007/978-3-319-24318-4\_21",

language = "English",

isbn = "9783319243177",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "287--298",

editor = "Marijn Heule and Sean Weaver",

booktitle = "Theory and Applications of Satisfiability Testing – SAT 2015",

address = "Switzerland",

note = "International Conference on Theory and Applications of Satisfiability Testing 2015, SAT 2015 ; Conference date: 24-09-2015 Through 27-09-2015",

url = "https://www.cs.utexas.edu/\textasciitilde{}marijn/sat15/",

}

Ignatiev, A, Previti, A & Marques-Silva, J 2015, SAT-based formula simplification. in M Heule & S Weaver (eds), Theory and Applications of Satisfiability Testing – SAT 2015: 18th International Conference Austin, TX, USA, September 24–27, 2015 Proceedings. Lecture Notes in Computer Science, vol. 9340, Springer, Cham Switzerland, pp. 287-298, International Conference on Theory and Applications of Satisfiability Testing 2015, Austin, Texas, United States of America, 24/09/15. https://doi.org/10.1007/978-3-319-24318-4_21

SAT-based formula simplification. / Ignatiev, Alexey; Previti, Alessandro; Marques-Silva, Joao.
Theory and Applications of Satisfiability Testing – SAT 2015: 18th International Conference Austin, TX, USA, September 24–27, 2015 Proceedings. ed. / Marijn Heule; Sean Weaver. Cham Switzerland: Springer, 2015. p. 287-298 (Lecture Notes in Computer Science; Vol. 9340).

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

TY - GEN

T1 - SAT-based formula simplification

AU - Ignatiev, Alexey

AU - Previti, Alessandro

AU - Marques-Silva, Joao

N1 - Conference code: 18th

PY - 2015

Y1 - 2015

N2 - The problem of propositional formula minimization can be traced to the mid of the last century, to the seminal work of Quine and McCluskey, with a large body of work ensuing from this seminal work. Given a set of implicants (or implicates) of a formula, the goal for minimization is to find a smallest set of prime implicants (or implicates) equivalent to the original formula. This paper considers the more general problem of computing a smallest prime representation of a non-clausal propositional formula, which we refer to as formula simplification. Moreover, the paper proposes a novel, entirely SAT-based, approach for the formula simplification problem. The original problem addressed by the Quine-McCluskey procedure can thus be viewed as a special case of the problem addressed in this paper. Experimental results, obtained on wellknown representative problem instances, demonstrate that a SAT-based approach for formula simplification is a viable alternative to existing implementations of the Quine-McCluskey procedure.

AB - The problem of propositional formula minimization can be traced to the mid of the last century, to the seminal work of Quine and McCluskey, with a large body of work ensuing from this seminal work. Given a set of implicants (or implicates) of a formula, the goal for minimization is to find a smallest set of prime implicants (or implicates) equivalent to the original formula. This paper considers the more general problem of computing a smallest prime representation of a non-clausal propositional formula, which we refer to as formula simplification. Moreover, the paper proposes a novel, entirely SAT-based, approach for the formula simplification problem. The original problem addressed by the Quine-McCluskey procedure can thus be viewed as a special case of the problem addressed in this paper. Experimental results, obtained on wellknown representative problem instances, demonstrate that a SAT-based approach for formula simplification is a viable alternative to existing implementations of the Quine-McCluskey procedure.

KW - Boolean Function

KW - Conjunctive Normal Form

KW - Disjunctive Normal Form

KW - Propositional Formula

KW - Conjunctive Normal Form Formula

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

U2 - 10.1007/978-3-319-24318-4_21

DO - 10.1007/978-3-319-24318-4_21

M3 - Conference Paper

SN - 9783319243177

T3 - Lecture Notes in Computer Science

SP - 287

EP - 298

BT - Theory and Applications of Satisfiability Testing – SAT 2015

A2 - Heule, Marijn

A2 - Weaver, Sean

PB - Springer

CY - Cham Switzerland

T2 - International Conference on Theory and Applications of Satisfiability Testing 2015

Y2 - 24 September 2015 through 27 September 2015

ER -

SAT-based formula simplification

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Cite this