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

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 Sep 2015 → 27 Sep 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 |

## Keywords

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