PolyBoRi: A Gröbner Basis Framework for Boolean Polynomials

Technical Report, Reports of Fraunhofer ITWM, Volume 122, Fraunhofer ITWM, August, 2007

Authors

• Michael Brickenstein
• Alexander Dreyer

Abstract

"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
x² = 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."

Full Text

• Publication: BrickenDreyerITWM07.pdf

BibTeX

 
@TechReport{ BrickenDreyerITWM07, 
   title = { PolyBoRi: A Gröbner Basis Framework for Boolean Polynomials }, 
   author = { Michael Brickenstein and Alexander Dreyer },     
   series = { Reports of Fraunhofer ITWM }, 
   volume = { 122 },     
   publisher = { Fraunhofer ITWM },     
   month = aug, 
   year = 2007, 
} 

---

This publication belongs to the project VerSiS.