Publica
Hier finden Sie wissenschaftliche Publikationen aus den FraunhoferInstituten. POLYBORI: A framework for Gröbnerbasis computations with Boolean polynomials
 Journal of symbolic computation 44 (2009), No.9, pp.13261345 ISSN: 07477171 ISSN: 1095855X 
 Conference on Effective Methods in Algebraic Geometry (MEGA) <2007, Strobl> 

 English 
 Journal Article, Conference Paper 
 Fraunhofer ITWM () 
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 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 Grobnerbases on specific data structures can be capable of handling problems of industrial size.