POLYBORI: A Gröbner basis framework for Boolean polynomials

  • This work presents a new framework for Gröbner basis computations with Boolean polynomials. Boolean polynomials can be modeled 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 x2 = x for each variable x. Therefore, the usual polynomial data structures seem not to be appropriate for fast Gröbner basis computations. We introduce a specialized data structure for Boolean polynomials based on zero-suppressed binary decision diagrams (ZDDs), which is 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 Gröbner 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 Gröbner bases on specific data structures can be capable to handle problems of industrial size.

Export metadata

  • Export Bibtex
  • Export RIS

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Author:M. Brickenstein, A. Dreyer
URN (permanent link):urn:nbn:de:hbz:386-kluedo-15442
Serie (Series number):Berichte des Fraunhofer-Instituts für Techno- und Wirtschaftsmathematik (ITWM Report) (122)
Document Type:Report
Language of publication:English
Year of Completion:2007
Year of Publication:2007
Publishing Institute:Fraunhofer-Institut für Techno- und Wirtschaftsmathematik
Tag:Boolean polynomials ; Gröber basis ; algebraic cryptoanalysis ; formal verification ; satisfiability
Faculties / Organisational entities:Fraunhofer (ITWM)
DDC-Cassification:510 Mathematik

$Rev: 12793 $