Search code examples
booleanboolean-logicboolean-expressioncircuit

Boolean expression simplification


I am trying to simplify a Boolean expression with exactly 39 inputs, and about 500 million - 800million terms (as in that many and/not/or statements).

A perfect simplification is not needed, but a good one would be nice.

I am aware of the K-maps , Quine–McCluskey, Espresso algorithms. However I am also aware that these mechanisms would take way too long to simplify a circuit of this size based on what I have read

I would need to simplify this expression as much as possible within a 24 hour period.

After google searching, I find it difficult to find any resources for attempting to simplify a machine of quite this magnitude! Any resources out there or a library out there that can attempt to at least simplify this to some extent within a 24 time period?


Solution

  • A greedy heuristic Simplify is described in the somewhat dated book

    Robert K. Brayton , Gary D. Hachtel , C. McMullen , Alberto Sangiovanni-Vincentelli Logic Minimization Algorithms for VLSI Synthesis

    You can find the chapter online.

    Simplify is based on the unate paradigm. In divide-and-conquer style, it recursively applies Shannon's expansion theorem to split the function into smaller sub-functions. The heuristic rule is to split by the most binate variable first, i.e. the variable which separates the largest number of terms.


    A second approach could be to use graph partitioning tools like METIS to split the terms into independent (or at least loosely related) subsets. But I am not aware that this has been tried sucessfully for logic synthesis tasks. My favorite search engine is sceptical and does not return any hits.


    A more recent algorithm based on Binary Decision Diagrams was published in

    Olivier Coudert: Doing Two-Level Logic Minimization 100 Times Faster

    The paper lists examples with very high number of terms similar to your task at hand.

    A somewhat related simplification technique BDD Sweeping as described in A Study of Sweeping Algorithms in the Context of Model Checking.