MEGA 2007Effective Methods in Algebraic Geometry Strobl, Austria, June 25th - 29th |
 |
Electronic Proceedings
Abstract
| Title | PolyBoRi: A framework for Gröbner basis computations with Boolean polynomials |
| Keywords | Groeber base, formal verification, Boolean polynomials, algebraic cryptoanalysis, satisfiability |
| Abstract | This work presents a new framework for Groebner 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 Groebner 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 Groebner 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 adequate and we believe that our preliminary implementation shows that Groebner bases on specialized data structures can be capable to handle problems of industrial size. |
The Institute is named after the famous Austrian mathematician Johann Radon (1887-1956)
Medieninhaber:
Österreichische Akademie der Wissenschaften
Juristische Person öffentlichen Rechts (BGBl 569/1921 idF BGBl I 130/2003)
Dr. Ignaz Seipel-Platz 2, 1010 Wien
Diese Website dient zur Information über die wissenschaftlichen Aktivitäten der Österreichischen Akademie der Wissenschaften und setzt somit den gesetzlichen Auftrag um, die Wissenschaft in jeder Hinsicht zu fördern.
This RICAM page was made with 100% valid HTML & CSS - Send comments to Webmaster
Today's date and time is 02/09/12 - 10:31 CET and this file ( /mega2007/electronic/26-abs.html ) was last modified on 06/19/07 - 14:54 CEST