SAT-based formula simplification

Alexey Ignatiev, Alessandro Previti, Joao Marques-Silva

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

8 Citations (Scopus)


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 languageEnglish
Title of host publicationTheory and Applications of Satisfiability Testing – SAT 2015
Subtitle of host publication18th International Conference Austin, TX, USA, September 24–27, 2015 Proceedings
EditorsMarijn Heule, Sean Weaver
Place of PublicationCham Switzerland
Number of pages12
ISBN (Electronic)9783319243184
ISBN (Print)9783319243177
Publication statusPublished - 2015
Externally publishedYes
EventInternational Conference on Theory and Applications of Satisfiability Testing 2015 - Austin, United States of America
Duration: 24 Sep 201527 Sep 2015
Conference number: 18th

Publication series

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


ConferenceInternational Conference on Theory and Applications of Satisfiability Testing 2015
Abbreviated titleSAT 2015
Country/TerritoryUnited States of America
Internet address


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

Cite this