SAT-based formula simplification

Alexey Ignatiev, Alessandro Previti, Joao Marques-Silva

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

8 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 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
PublisherSpringer
Pages287-298
Number of pages12
ISBN (Electronic)9783319243184
ISBN (Print)9783319243177
DOIs
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
https://www.cs.utexas.edu/~marijn/sat15/

Publication series

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

Conference

ConferenceInternational Conference on Theory and Applications of Satisfiability Testing 2015
Abbreviated titleSAT 2015
Country/TerritoryUnited States of America
CityAustin
Period24/09/1527/09/15
Internet address

Keywords

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

Cite this