Exact Synthesis of ESOP Forms

TL;DR

This paper introduces an exact, SAT-based method for synthesizing minimal ESOP forms for Boolean functions, capable of handling incomplete specifications and optimizing for the least number of product terms.

Contribution

It formalizes the ESOP synthesis problem as a decision problem and develops search procedures to find minimal or small-sized ESOP forms efficiently.

Findings

Effective for functions with few product terms

Handles incompletely specified Boolean functions

Shows promising performance in experiments

Abstract

We present an exact synthesis approach for computing Exclusive-or Sum-of-Products (ESOP) forms with a minimum number of product terms using Boolean satisfiability. Our approach finds one or more ESOP forms for a given Boolean function. The approach can deal with incompletely-specified Boolean functions defined over many Boolean variables and is particularly fast if the Boolean function can be expressed with only a few product terms. We describe the formalization of the ESOP synthesis problem with a fixed number of terms as a decision problem and present search procedures for determining ESOP forms of minimum size. We further discuss how the search procedures can be relaxed to find ESOP forms of small sizes in reasonable time. We experimentally evaluate the performance of the SAT-based synthesis procedures on completely- and incompletely-specified Boolean functions.