Presentation of Boolean Polynomials as ZDD-Diagrams

Boolean Gr¨obner basis have shown their practical efficiency for different problems. Among them are algebraic cryptanalysis HFE (Hidden Field Equations), modeling of quantum computing and boolean satisfiability problem (SAT). Algorithms for computing Gr¨obner basis have exponential complexity for execution time as well as for memory usage. The more appropriate data structure was introduced, which is based on zero-suppressed binary decision diagrams (ZDD). Also we show the relation between ZDD and special recursive notation of polynomials. The recursive notation is the collection of equalities which have had one-to-one correspondence with graphical presentation of ZDDs. We prove lemma which gives the number of nodes estimation for ZDD which represent boolean polynomial with all monoms up to d degree of n variables. Furthermore, we present C++11 ZDD package providing possibility for addition and multiplication of boolean polynomials, multiplication by variable, presentation in compressed recursive form and graphical presentation. The package includes its own implementation of red-black trees, lists, and memory manager. ZDD package was developed for using as internal data structure of the boolean polynomials for computation of involutive Gr¨obner basis.

boolean polynomials, binary decision diagram, Gr¨obner basis, SAT