Gröbner Bases for Boolean Function Minimization

Abstract Boolean function minimization techniques try to find, for a given formula, a smaller equivalent formula. In this work, we present a novel technique for heuristic multi-level Boolean function minimization. By using an algebraic encoding, we embed the minimization problem into an algebraic domain, where algorithms for computing Gröbner bases become applicable. A Gröbner basis usually forms a compact representation of our encoded function. From the Gröbner basis, we then reconstruct an equivalent, more compact Boolean formula. The minimized formula is in the language of Boolean formulas with negation, conjunction, disjunction and exclusive-or operations. To the best of our knowledge, our approach is the first to use Gröbner bases for function minimization. We evaluate our approach on Boolean formulas created from arithmetic operations as well as on random formulas. Compared to state-of-the-art exact minimization algorithms, our approach can handle formulas with up to three times as many variables. Empirically, we obtain very compact formulas. In particular, our algorithm is especially efficient if there exists a comparatively small equivalent formula or if the minimized formula contains exclusive-or operations. In practice, such functions occur e.g. in embedded systems or cryptography. Overall, our approach forms a new, interesting trade-off between result minimality and runtime.