PolyBoRi: A framework for Gröbner basis computations with Boolean polynomials
In: Electronic Proceedings of Effective Methods in Algebraic Geometry MEGA 2007. June, 2007
Authors
- Michael Brickenstein
- Alexander Dreyer
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*x=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.
Full Text
BibTeX
@InProceedings{ BrickensteinDreyer07,
title = { PolyBoRi: A framework for Gröbner basis computations with Boolean polynomials },
author = { Michael Brickenstein and Alexander Dreyer },
booktitle = { Electronic Proceedings of Effective Methods in Algebraic Geometry MEGA 2007 },
month = jun,
year = 2007,
}
This publication belongs to the project
VerSiS.
