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.

Volltext Dateien herunterladen

Metadaten exportieren

Weitere Dienste

Teilen auf Twitter Suche bei Google Scholar
Verfasserangaben:M. Brickenstein, A. Dreyer
URN (Permalink):urn:nbn:de:hbz:386-kluedo-15442
Schriftenreihe (Bandnummer):Berichte des Fraunhofer-Instituts für Techno- und Wirtschaftsmathematik (ITWM Report) (122)
Sprache der Veröffentlichung:Englisch
Jahr der Fertigstellung:2007
Jahr der Veröffentlichung:2007
Veröffentlichende Institution:Fraunhofer-Institut für Techno- und Wirtschaftsmathematik
Datum der Publikation (Server):28.05.2008
Freies Schlagwort / Tag:Boolean polynomials; Gröber basis; algebraic cryptoanalysis; formal verification; satisfiability
Fachbereiche / Organisatorische Einheiten:Fraunhofer (ITWM)
DDC-Sachgruppen:5 Naturwissenschaften und Mathematik / 510 Mathematik
Lizenz (Deutsch):Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011