Details:
Title  PolyBoRi: A framework for Gröbnerbasis computations with Boolean polynomials  Author(s)   Type  Article in Journal  Abstract  This work presents a new framework for Grobnerbasis 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 Grobnerbasis computations. We introduce a specialised data structure for Boolean polynomials based on zerosuppressed 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 highlevel algorithmic aspects, taking into account the new data structures as well as structural properties of Boolean polynomials. For example, a new uselesspair criterion for Grobnerbasis 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 sufferbesides 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 Grobnerbases on specific data structures can be capable of handling problems of industrial size.  Keywords  Boolean Gröbner basis, Formal verification, Algebraic cryptoanalysis, Satisfiability  ISSN  07477171 
URL 
http:/dx.doi.org/10.1016/j.jsc.2008.02.017 
Language  English  Journal  Journal of Symbolic Computation  Volume  44  Number  9  Pages  13261345  Year  2009  Note  Effective Methods in Algebraic Geometry  Edition  0  Translation 
No  Refereed 
No 
