Features Overview
Goals
Gröbner bases have become a standard tool for treating problems which can be described by polynomial systems. While the concept of Gröbner bases was known much longer, their current practical importance is a result of dramatical improvements in performance and algorithms in recent years.
The motivation for this project was to provide a framework for computations with Boolean polynomials, which have the following special properties: coefficients lie in the field with two elements and exponents are bounded to degree one in each variable. The latter originates from the application of field equations of the form: x² = x. This occurs in many significant applications like formal verification but also in cryptography, logic, and many more. This is due to the fact, that Boolean polynomials correspond to Boolean functions.
Although Gröbner bases have already become a standard tool for treating polynonomial systems, current implementations have not been capable of satisfyingly handling Boolean polynomials from real-world applications yet. One of the first questions was: Can we use the simplified model to get better data structures? Of course, we did also ask, whether we can find algorithmic improvements of the situation.
PolyBoRi can be understood as a framework of high performance data structures and sample Gröbner bases algorithms. On the other hand it is very clear, that many problems arising from practice can only be attacked, if optimisations occurs on many levels, e.g. data structures, higher level algorithms, formulation of equations/problems, good monomial orderings.
An important aspect in symbolic computation, is that independent of the strategy polynomials can become very big, but usually keep structured (in a very general sense). Using this structure to keep the memory consumption moderate was a primary design goal of PolyBoRi. Another observation is, that in Gröbner bases computations often arithmetical operations on similar polynomials (differing only in a few terms) occur. PolyBoRi also gives an answer to that problem using a cache on the level of substructures.
What is PolyBoRi?
PolyBoRi is implemented as a C++ library for Polynomials over Boolean Rings, which provides high-level data types for Boolean polynomials and monomials, exponent vectors, as well as for the underlying polynomial rings. The ring variables may be identified by their indices or by a custom string. Polynomial structures and monomials use zero-suppressed binary decision diagrams (ZDDs) as internal storage type, but this is hidden from the user. The current implementation uses the decision-diagram management from Cudd .
In addition, basic polynomial operations - like addition and multiplication - have been implemented and associated to the corresponding operators. In order to enable efficient implementation, these operations were reformulated in terms of set operations, which are compatible with the ZDD approach. This also applies to other classical functionality like degree computation and leading term computations. The ordering-dependent functions are currently available for lexicographical, degree-lexicographical ordering (with first variable being the largest one), and degree-reverse-lexicographical ordering, whereas in the latter case the variables are treated in reversed order, for efficiency reasons. Product orderings consisting of blocks of these are scheduled.
A complete Python interface allows for parsing of complex polynomial systems, and also sophisticated and easy extendable strategies for Gröbner base computation have been made possible by this. An extensive testsuite, which mainly carries satisfiability examples and some from cryptography, is used to ensure validity during development. Also, with the tool ipython the PolyBoRi data structures and procedures can be used interactively as a command line tool.
In addition to optimized data structures, PolyBoRi features a performant reference implementation for Gröbner basis computation, using an enhanced variant of the slimgb algorithm, which was implemented first in the computer algebra system Singular . The framework was developed and designed together with slimgb's original author.
The initial performance of PolyBoRi seems to be very promising. It can be seen, that the advantage of PolyBoRi grows with the number of variables. For many practical applications this size will even bigger. We are very confident, that it will be possible to attack some of this problems in future by using more specialized approaches. This is a key point in the development of PolyBoRi to facilitate problem specific, high performance solutions.
