Home | Quick Search | Advanced Search | Bibliography submission | Bibliography submission using bibtex | Bibliography submission using bibtex file | Links | Help | Internal


TitlePolyBoRi: A framework for Gröbner-basis computations with Boolean polynomials
TypeArticle in Journal
AbstractThis work presents a new framework for Grobner-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 Grobner-basis computations. We introduce a specialised data structure for Boolean polynomials based on zero-suppressed 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 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 Grobner-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 Grobner-bases on specific data structures can be capable of handling problems of industrial size.
KeywordsBoolean Gröbner basis, Formal verification, Algebraic cryptoanalysis, Satisfiability
URL http:/dx.doi.org/10.1016/j.jsc.2008.02.017
JournalJournal of Symbolic Computation
NoteEffective Methods in Algebraic Geometry
Translation No
Refereed No