Hier finden Sie wissenschaftliche Publikationen aus den Fraunhofer-Instituten.

POLYBORI: A framework for Gröbner-basis computations with Boolean polynomials

: Brickenstein, M.; Dreyer, A.


Journal of symbolic computation 44 (2009), No.9, pp.1326-1345
ISSN: 0747-7171
ISSN: 1095-855X
Conference on Effective Methods in Algebraic Geometry (MEGA) <2007, Strobl>
Journal Article, Conference Paper
Fraunhofer ITWM ()

This work presents a new framework for Grobner-basis computations with Boolean polynomials. Boolean polynomials can be modelled in a rather simple way, with both coefficients and degree per variable lying in {0, 1}. The ring of Boolean polynomials is, however, not a polynomial ring, but rather the quotient ring of the polynomial ring over the field with two elements modulo the field equations x(2) = x for each variable x. Therefore, the usual polynomial data structures seem not to be appropriate for fast Grobner-basis computations. We introduce a specialised data structure for Boolean polynomials based on zero-suppressed binary decision diagrams (ZDDs), which are capable of handling these polynomials more efficiently with respect to memory consumption and also computational speed. Furthermore, we concentrate on high-level algorithmic aspects, taking into account the new data structures as well as structural properties of Boolean polynomials. For example, a new useless-pair criterion for Grobner-basis computations in Boolean rings is introduced. One of the motivations for our work is the growing importance of formal hardware and software verification based on Boolean expressions, which suffer - besides from the complexity of the problems - from the lack of an adequate treatment of arithmetic components. We are convinced that algebraic methods are more suited and we believe that our preliminary implementation shows that Grobner-bases on specific data structures can be capable of handling problems of industrial size.