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 boolean function minimization. By using an algebraic encoding, we embed the minimization problem into an algebraic domain, where algorithms for computing Gröbner bases are 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. Our approach is the first to use Gröbner bases for function minimization. Combined with advances of algebraic Gröbner bases in satisfiability checking, this motivates further research on applications of Gröbner bases in the context of boolean logic.

Keywords

• eol>Multi-level Logic Optimization
• Boolean Function Synthesis
• Gröbner Bases

1. Introduction

microarchitectural hash functions [ 6 ]. Some proprietary hash functions, e.g. used for cache slice indexing in modern microprocessors have been reversed (i.e. a compact representation has been found) by using our approach (work under submission). In practice, we observe more compact representations than a minimized DNF even on random formulas, Section 3. Furthermore, for some classes of formulas, nearly optimal results are provable (Theorem 2).

In addition to previous applications of Gröbner bases in logic [ 4, 7 ] that focus on preprocessing for satisfiability checking, our approach is a novel, complementary application of Gröbner bases for boolean logic. This motivates further research in this direction.

1.1. Related Work

Boolean Minimization Usually, a boolean logic minimizer is given a formula in DNF, which can be easily obtained from a truth table. Then, it produces a small, equivalent formula. Existing tools can be classified by the shape of the output formula:

Two-level logic optimization tools produce again a formula in DNF. Classically, Quine and McCluskey [8, 9] focus on optimal two-level minimization. However, their optimal approach quickly becomes infeasible [ 1 ]. Thus, later approaches such as ESPRESSO [ 1 ] make use of a heuristic search for producing a compact DNF. Still, representing a formula in DNF can have exponential overhead. For example, any DNF of (1, . . . , ) = 1 ⊕ · · · ⊕ is exponentially larger in than . This motivates more general minimization approaches.

Multi-level logic optimization allows minimized formulas of arbitrary shape. Still, some tools produce only formulas of a fixed structure. For example, EXORCISM [ 10] always produces formulas of the shape “exclusive-sum-of-products”. Other tools produce formulas of arbitrary depth and structure, for example MIS [11] or LSS [12]. Most multi-level optimization tools rely on two-level optimization and apply syntactic transformations such as subexpression recognition and replacement to the resulting formula [13]. More recently, approaches for multi-level synthesis based on satisfiability [ 14, 15] have been studied. They provide optimal solutions but are only feasible for small instances. Our presented approach provides a heuristic method for multi-level logic optimization which, contrary to previous work, does not rely on syntactic recognitions. Gröbner Bases are special generating sets for ideals and are widely used in computer algebra [16], for example for ideal membership testing of a polynomial. However, we focus on applications of Gröbner bases in logic. For example, Gröbner bases are used in the context of satisfiability checking and model counting, as well as in verification and SMT solving.

In satisfiability checking, Gröbner bases can be used for pre-processing clause sets in conjunctive normal form (CNF) [ 4, 7 ]. Concretely, it is possible to encode a (sub-)set of clauses of a CNF formula as a system of polynomials. Then, a Gröbner basis for this system is computed. The resulting system of polynomials is then, again, interpreted as a set of clauses. The resulting, usually more compact set of clauses is equivalent to the original set. Hence, it is possible to replace sets of clauses with more compact, equivalent sets. Satisfiability checking on the preprocessed clauses is usually faster than on the original CNF [ 4 ]. However, the cost of computing the Gröbner bases outweighs the benefits. A similar encoding can be used for model counting for boolean formulas [17]. Given a set of clauses reduced by the above technique, it becomes (computationally) easy to count satisfiable assignments. In contrast to the above approaches, we apply Gröbner bases to formulas in disjunctive normal form (DNF), and in the context of logic minimization.

Other applications of Gröbner basis are verification of arithmetic gates [ 18, 19, 20] and SMT solving over finite fields [ 21, 22] or real numbers [23]. However, note that both applications do not directly encode boolean formulas as polynomials, but use Gröbner bases for theory solving. Still, combined with our work, this suggests that Gröbner bases have multiple applications in logic and could be worthwhile to investigate further.

2. Gröbner Bases for Logic Minimization

Given a boolean DNF = ⋁︀ ⋀︀ with literals ∈ {1, . . . , , ¬1, . . . , ¬}, we want to find an equivalent smaller formula. Our idea is to switch from boolean formulas to ideals in the polynomial ring F2[1, . . . , ]. Then, Gröbner bases of correspond empirically to smaller equivalent formulas of .

2.1. Encoding Boolean Formulas as Polynomials

In the following, we will identify the truth-values {false, true} with the set F2 = {0, 1}, where false corresponds to 0 and true corresponds to 1. Note that F2 has the structure of a field with multiplication given by ∧ and addition is given by ⊕ . Hence, we can view a polynomial = ∑︀ ∏︀ ∈ F2[1, . . . , ] with ∈ {1, 1, . . . , } as a boolean formula of the form ⨁︀ ⋀︀ . Conversely, we can encode any boolean formula as a polynomial over F2 by additionally using the identities ¬ = ⊕ 1 and ∨ = ¬(¬ ∧ ¬), which will be encoded as + 1 and 1 + (1 + ) · (1 + ) = + + respectively. We call this the algebraic encoding of .

The previous relationship between boolean formulas and polynomials can be further extended to a correspondence between equivalent formulas and ideals in F2[1, . . . , ]. Recall that an ideal in a polynomial ring is a subset ⊆ which can be written as = {∑︀=1 | 1, . . . , ∈ } for some polynomials 1, . . . , ∈ . Such polynomials are called generators of , and we write = (1, . . . , ).

Theorem 1. There is a bijection between equivalence classes of boolean formulas [ ] and ideals ⊆ F2[1, . . . , ] containing 21 + 1, . . ., 2 + , such that () = 0 ⇐⇒ ∀ ∈ , () = 0. Proof. Let [ ] be an equivalence class of boolean formulas in variables. Then it is uniquely determined by its zero set { ∈ F2 | () = 0}. Conversely, any set ⊆ F2 is the zero set of the formula ⋀︀∈ ⋁︀=1( ⊕ ). Hence, there is a bijection between equivalent formulas and subsets of F2. Similarly, any ideal containing 21 + 1, . . . , 2 + is uniquely determined by its zero set { ∈ F2 | ∀ ∈ , () = 0} by Hilbert’s Nullstellensatz for finite fields [ 24]. Additionally, every subset ⊆ F2 is finite and hence a zero set of an ideal by elementary results from algebraic geometry. Further, this ideal can always be assumed to contain 21 + 1, . . . , 2 + , such that we have a bijection between ideals containing 21 + 1, . . . , 2 + and subsets ⊆ F2. By combining this bijection which the first one, we obtain the statement of the theorem.

Importantly, we can explicitly convert a boolean formula to generators of the corresponding ideal and vice versa. Let = ⋁︀ ⋀︀ be a formula in DNF, then its corresponding ideal is generated by 21 + 1, . . ., 2 + and = ∏︀ , where we identify a literal with a polynomial via our algebraic encoding. This can be verified by using Theorem 1 and observing that () = 0 if and only if () = 0 for all , which is equivalent to () = 0 for all ∈ . Similarly, an ideal = (1, . . . , , 21 + 1, . . . , 2 + ) corresponds to the boolean formula ⋁︀ , where the polynomials are again identified with a boolean formula.

Note that the polynomials 2 + represent the idempotency law ∧ = and allow the elimination of all higher powers of during the Gröbner basis computation. Thus, there exist only 2 diferent leading monomials besides 2 , which implies that the size of a reduced Gröbner basis is bounded by 2 + . Further, it is possible to compute this Gröbner basis in time 2() using Buchberger’s algorithm, see Proposition 4.1.1 in [17]. This provides a significant improvement compared to the usual double exponential bound for Gröbner bases.

2.2. Gröbner Basis Minimization

Empirically, Gröbner bases are relatively small if the ideal is not too complex. Hence, we simplify a boolean formula by converting it to an ideal . Then, we compute a Gröbner basis of to obtain a set of generators . is then converted back to a formula of the form ⋁︀∈ ∼= ⋁︀∈ ¬¬. We can apply this approach recursively to the terms ¬ to further reduce the size and obtain a formula of the form ⋁︀ ¬ ⋁︀ ¬ ⋁︀ . . . ∼= ⋁︀ ⋀︀ ⋁︀ . . ., as depicted in the following algorithm: 8:

← ¬ return ⋁︀∈ 1: function Minimize( ) 2: ← GröbnerBasis(Ideal( )) 3: for ∈ do 4: if is linear or recursion limit is reached then 5: ← Formula() 6: else 7:

Minimize(DNF(¬Formula())) Note that it is not guaranteed that our algorithm produces a smaller formula and by the previous bound the Gröbner bases can have a size exponential in the number of variables. However, empirically we observed very compact formulas. Furthermore, for special classes of formulas, better bounds can be proven.

Theorem 2. Let be a formula in DNF which is equivalent to ⋁︀ ⨁︀ for a matrix ∈ F2× . Then |Minimize( )| < 2 · · rank(), where | · | denotes the number of boolean operators and variables in a formula.

Proof. Consider a boolean formula which is equivalent to ⋁︀=1 ⨁︀=1 for a matrix ∈ F2× . Then the corresponding ideal from Theorem 1 is generated by 2 + and the linear terms ∑︀

=1 defined by the rows of . Denote with the rank of and let ′ ∈ F2× the be matrix given by the non-zero rows in the reduced row echelon form of , which can be computed using Gaussian elimination. Then one can check that a reduced Gröbner basis of is given by the terms ∑︀=1 ′ corresponding to the rows of ′ and the terms 2 + for which is not a leading monomial of one of the first terms. Since a reduced Gröbner basis is unique, it will also be computed by our minimization algorithm. Further, the terms of the form 2 + are redundant and will be removed, such that a formula of the form ⋁︀=1 ⨁︀=1 ′ is returned. By counting the number of operators and variables, we obtain that the size of such a formula is always less than 2.

Further Improvements In addition to our main algorithm, we implemented the following two improvements: First, minimizing the DNF with a two-level minimization algorithm during preprocessing reduces the size of the input. This does not change result quality, but can significantly speed up the algebraic computations. Second, some elements of the Gröbner basis can be redundant in the sense that a subset of the Gröbner basis already generates the corresponding ideal. Finding a minimal generating subset of the Gröbner basis can be formulated as a weighted set-cover problem, which we solve in a post-processing step to improve result quality. Eliminating these redundant terms directly during the computation of the Gröbner basis is subject to further work.

3. Evaluation

A first prototype of this algorithm has been implemented in SageMath [ 25], using SINGULAR [26] for computing Gröbner bases, as well as ESPRESSO [ 1 ] for DNF preprocessing and GLPK [27] for set-cover computations. Note that Gröbner bases are computed with respect to the degree reverse lexicographic order. A basic benchmark in Figure 1 shows the average size of a reconstructed formula, and the runtime of the minimization process. This is compared to a minimized formula in DNF from ESPRESSO [ 1 ] and a minimal formula produced with ABC’s ‘exact’ command [28, 14]. The benchmark ran on 200 random formulas for each size. The formulas were sampled uniformly at random on a syntactic level, i.e. one syntax tree is sampled uniformly at random out of all possible syntax trees for a specific size. Note that exact, optimal synthesis with ABC is only possible for up to 7–8 variables, while our approach can deal with up to 20 variables. Our resulting formulas are always more compact than a DNF produced by ESPRESSO. However, our approach has a significantly greater runtime. We are currently working on reverse-engineering microarchitectural hash functions used e.g. for cache indexing in processors with our algorithm (to appear in [29]).

4. Conclusion

We have presented a novel technique for heuristic multi-level formula minimization based on an algebraic encoding of formulas and Gröbner basis computations. Currently, our algorithm can handle functions with up to 20 input bits, whereas exact synthesis can only handle up to 8 input bits. Empirically, our approach produces smaller formulas than two-level minimization algorithms such as ESPRESSO. In particular, our idea works well for formulas with many exclusive-or operations. Our algorithm shows a new application of Gröbner basis computations in logic minimization. In addition to previous work on Gröbner bases in satisfiability [ 4, 7 ], this result suggests that the use of our algebraic encoding, as well as Gröbner bases, brings benefits to boolean logics and could be worthwhile to investigate further.

Acknowledgements:

We thank our anonymous reviewers for their constructive comments. [8] W. V. Quine, The problem of simplifying truth functions, The American mathematical monthly 59 (1952) 521–531. doi:10.1080/00029890.1952.11988183. [9] E. J. McCluskey, Minimization of boolean functions, The Bell System Technical Journal 35 (1956) 1417–1444. doi:10.1002/j.1538-7305.1956.tb03835.x. [10] A. Mishchenko, M. Perkowski, Fast heuristic minimization of exclusive-sums-of-products, 5th International Reed-Muller Workshop (2001). [11] R. K. Brayton, R. Rudell, A. Sangiovanni-Vincentelli, A. R. Wang, MIS: A multiple-level logic optimization system, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 6 (1987) 1062–1081. doi:10.1109/TCAD.1987.1270347. [12] J. A. Darringer, D. Brand, J. V. Gerbi, W. H. Joyner, L. Trevillyan, LSS: A system for production logic synthesis, IBM Journal of Research and Development 28 (1984) 537–545. doi:10.1147/rd.285.0537. [13] M. Perkowski, Multi-level logic minimization, http://web.cecs.pdx.edu/~mperkows/=FSM/ ifnite-sm/node17.html, Accessed: 28.03.2023. [14] M. Soeken, W. Haaswijk, E. Testa, A. Mishchenko, L. G. Amarù, R. K. Brayton, G. D. Micheli, Practical exact synthesis, in: 2018 Design, Automation & Test in Europe Conference & Exhibition (DATE), IEEE, 2018, pp. 309–314. doi:10.23919/DATE.2018.8342027. [15] W. Haaswijk, M. Soeken, A. Mishchenko, G. D. Micheli, SAT-based exact synthesis: Encodings, topology families, and parallelism, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 39 (2020) 871–884. doi:10.1109/TCAD.2019. 2897703. [16] T. Becker, V. Weispfenning, Gröbner bases, Graduate Texts in Mathematics, Springer, 1993.

doi:10.1007/978-1-4612-0913-3. [17] S. Gao, Counting zeros over finite fields with Gröbner bases, Master’s thesis, Carnegie

Mellon University, 2009. URL: https://www.cs.cmu.edu/~sicung/papers/MS_thesis.pdf. [18] D. Ritirc, A. Biere, M. Kauers, Improving and extending the algebraic approach for verifying gate-level multipliers, in: 2018 Design, Automation & Test in Europe Conference & Exhibition (DATE), IEEE, 2018, pp. 1556–1561. doi:10.23919/DATE.2018.8342263. [19] D. Kaufmann, A. Biere, M. Kauers, Verifying large multipliers by combining SAT and computer algebra, in: 2019 Formal Methods in Computer Aided Design (FMCAD), IEEE, 2019, pp. 28–36. doi:10.23919/FMCAD.2019.8894250. [20] D. Kaufmann, A. Biere, M. Kauers, Incremental column-wise verification of arithmetic circuits using computer algebra, Formal Methods in System Design 56 (2020) 22–54. doi:10.1007/s10703-018-00329-2. [21] T. Hader, D. Kaufmann, L. Kovacs, SMT solving over finite field arithmetic, in: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, EasyChair, 2023, pp. 238–256. doi:10.29007/4n6w. [22] A. Ozdemir, G. Kremer, C. Tinelli, C. W. Barrett, Satisfiability modulo finite fields, volume 185 of Frontiers in Artificial Intelligence and Applications , IOS Press, 2009, pp. 825–885. doi:10.3233/978-1-58603-929-5-825. [23] S. Junges, U. Loup, F. Corzilius, E. Ábrahám, On Gröbner bases in the context of satisfiabilitymodulo-theories solving over the real numbers, in: Algebraic Informatics, Springer, 2013, pp. 186–198. doi:10.1007/978-3-642-40663-8\_18. [24] S. R. Ghorpade, A note on Nullstellensatz over finite fields, Contemporary Mathematics (2018). [25] The Sage Developers, Sage Mathematics Software, Version 9.0, http://www.sagemath.org, 2023. [26] W. Decker, G.-M. Greuel, G. Pfister, H. Schönemann, Singular — A computer algebra system for polynomial computations, Version 4.3.0, http://www.singular.uni-kl.de, 2022. [27] GNU Linear Programming Kit, Version 4.32, http://www.gnu.org/software/glpk/glpk.html, 2008. [28] R. Brayton, A. Mishchenko, ABC: An academic industrial-strength verification tool, in: Computer Aided Verification, Springer, 2010, pp. 24–40. doi: 10.1007/ 978-3-642-14295-6_5. [29] L. Gerlach, S. Schwarz, N. Faroß, M. Schwarz, Eficient and generic microarchitectural hash-function recovery, 2024. To appear in the IEEE Symposium on Security & Privacy.

References

[1] R. K. Brayton , G. D. Hachtel , C. McMullen , A. Sangiovanni-Vincentelli , Logic minimization algorithms for VLSI synthesis , The Springer International Series in Engineering and Computer Science, Springer, 1984 . doi: 10 .1007/978-1- 4613 -2821-6.

[2] R. L. Rudell , Multiple-valued logic minimization for PLA synthesis , Technical Report , EECS Department, University of California, Berkeley, 1986 . URL: http://www2.eecs.berkeley. edu/Pubs/TechRpts/1986/734.html.

[3] D. Buchfuhrer , C. Umans , The complexity of boolean formula minimization , in: Automata, Languages and Programming , Springer, 2008 , pp. 24 - 35 . doi: 10 .1007/ 978-3- 540 -70575-8\_3.

[4] C. Condrat , P. Kalla , A Gröbner basis approach to CNF-formulae preprocessing , in: Tools and Algorithms for the Construction and Analysis of Systems , Springer, 2007 , pp. 618 - 631 . doi: 10 .1007/978-3- 540 -71209-1\_ 48 .

[5] B. Buchberger , A theoretical basis for the reduction of polynomials to canonical forms , ACM SIGSAM Bulletin 10 ( 1976 ) 19 - 29 . doi: 10 .1145/1088216.1088219.

[6] J. D. McCalpin , Mapping addresses to L3/CHA slices in Intel processors , Technical Report , TACC, The University of Texas at Austin, 2021 . doi: 10 .26153/tsw/14539.

[7] T. Nguyen , Combinations of boolean Gröbner bases and SAT solvers , Ph.D. thesis , University of Kaiserslautern, 2014 . doi: 10 .13140/RG.2.2.25392.92167.