2 How to program efficiently

The goal of this section is to explain how to get most performance out of PolyBoRi using the underlying ZDD structure. This awareness can be seen on several levels

2.1 Low level friendly programming

PolyBoRi is implemented as layer over a decision diagram library (CUDD at the moment).

In CUDD every diagram node is unique: If two diagrams have the same structure, they are in fact identical (same position in memory). Another observation is, that CUDD tries to build a functional style API in the C programming language. This means, that no data is manipulated, only new nodes are created. Functional programming is a priori very suited for caching and multithreading (at the moment however threading is not possible in PolyBoRi). The ite-operator is the most central function in CUDD. It takes two nodes/diagrams t, e and an index i and creates a diagram with root variable i and then-branch t, else-branch e. It is necessary that the branches have root variables with bigger index (or are constant). It creates either exactly one node, or retrieves the correct node from the cache. Function calls which come essentially down to a single ite call are very cheap.

For example taking the product x1 (x2 (x3 (x4 ⋆ x5))) is much cheaper than ((((x1 ⋆ x2) ⋆ x3) ⋆ x4) ⋆ x5).

In the first case, in each step a single node is prepended to the diagram, while in the second case, a completely new diagram is created. The same argument would apply for the addition of these variables. This example shows, that having a little bit background about the data structure, it is often possible to write code, that looks as well algebraic as provides good performance.

2.2 Replace algebra by set operations

Often there is an alternative description in terms of set operations for algebraic operations, which is much faster.

2.2.1 Construct power sets

An example for this behaviour is the calculation of power sets (sets of monomials/polynomials containing each term in the specified variables). The following code constructs such a power set very inefficiently for the first three variables:

    for i1 in (0,1) 
    for i2 in (0,1) 
    for i3 in (0,1)])

The algorithm has of course exponential complexity in the number of variables. The resulting ZDD however has only as many nodes as variables. In fact it can be constructed directly using the following function (from specialsets.py).

def power_set(variables): 
    if not variables: 
        return BooleConstant(1) 
    res=Polynomial(1, variables[0].ring()).set() 
    for v in variables: 
    return res

Note, that we switched from polynomials to Boolean sets. We inverse the order of variable indices for iteration to make the computation compatible with the principles in 2.1 (simple ite operators instead of complex operations in each step).

2.2.2 All monomials of degree d

The following function constructs the complete homogeneous polynomial/BooleSet containing all possible monomials of degree d.

def all_monomials_of_degree_d(d,variables): 
    if d==0: 
        return BooleConstant(1) 
    if not variables: 
        return [] 
    for v in variables[:-1]: 
    return res

We use the set of all monomials of one degree lower using the cartesian product with the set of variables and remove every term, where the degree did not increase (boolean multiplication: x2 = x).

2.3 Direct constructions of diagrams

Sometimes, it is possible to construct the decision diagram directly, as it is theoretically known, how it looks like. In the following, we construct the same polynomial as in 2.2.2 directly by elementary if_then_else operations. This will save much recursion overhead.

def all_monomials_of_degree_d(d, variables): 
    if not variables: 
        assert d==0 
        return BooleConstant(1) 
    ring = variables[0].ring() 
    if d>len(variables): 
        return Polynomial(0, ring) 
    if d<0: 
        return Polynomial(1, ring) 
    #this ensures sorting by indices 
    for i in xrange(1, len(variables)-d+1): 
        while not nav.constant(): 
        acc=Polynomial(1, ring) 
        for (nav, v) in reversed(zip(navs, deg_variables)): 
            acc=if_then_else(v, acc, nav) 
    return res.set()

2.4 Case study: Graded part of a polynomial

In the following we will show five variants to implement a function, that computes the sum of all terms of degree d in a polynomial f.

2.4.1 Simple, algebraic solution
def simple_graded(f, d): 
    return sum((t for t in f.terms() if t.deg()==d))

This solution is obvious, but quite slow.

2.4.2 Low level friendly, algebraic solution
def friendly_graded(f, d): 
    for t in f.terms: 
        if t.deg()!=d: 
    return add_up_polynomials(vec)

We leave it to the heuristic of the add_up_polynomials function how to add up the monomials. For example a divide and conquer strategy is quite good here.

2.4.3 Highlevel with set operations
def highlevel_graded(f,d): 
    return Polynomial( 

This solution build on the fast intersection algorithm and decomposes the task in just two set operations, which is very good.

However it can be quite inefficient, when f has many variables. This can increase the number of steps in the intersection algorithm (which takes with high probability the else branch of the second argument in each step).

2.4.4 Recursive

The repeated unnecessary iteration over all variables in f (during the intersection call in the last section) can be avoided by taking just integers as second argument for the recursive algorithm (in the last section this was intersection).

def recursive_graded(f,d): 
    def do_recursive_graded(f,d): 
        if f.empty(): 
            return f 
        if d==0: 
            if Monomial(f.ring()) in f: 
                return Polynomial(1, f.ring()).set() 
                return BooleSet(f.ring()) 
            if nav.constant(): 
                return BooleSet() 
            return if_then_else( 
    return Polynomial( 

Recursive implementations are very compatible with our data structures, so are quite fast. However this implementation does not use any caching techniques. CUDD recursive caching requires functions to have one, two or three parameters, which are of ZDD structure (so no integers). Of course we can encode the degree d by the d-th Variable in the Polynomial ring.

2.4.5 Decision-diagram style recursive implementation in PolyBoRi

The C++ implementation of the functionality in PolyBoRi is given in this section, which is recursive and uses caching techniques.

// determine the part of a polynomials of a given degree 
template <class CacheType, class NaviType, 
class DegType, class SetType> 
dd_graded_part(const CacheType& cache, NaviType navi, DegType deg, 
               SetType init) { 
  if (deg == 0) { 
    return SetType(navi); 
    return SetType(); 
  // Look whether result was cached before 
  NaviType cached = cache.find(navi, deg); 
  if (cached.isValid()) 
    return SetType(cached); 
  SetType result = 
                navi.then_branch(), deg - 1, init), 
                navi.else_branch(), deg, init) 
  // store result for later reuse 
  cache.insert(navi, deg, result.navigation()); 
  return result; 

The encoding of integers for the degree as variable is done implicitly by our cache lookup functions.

2.5 Case study: Evaluation of a polynomial

2.5.1 Substitute a single variable x in a polynomial by a constant c

Given a Boolean polynomial f, a variable x and a constant c, we want to plug in the constant c for the variable x.

Naive approach The following code shows how to tackle the problem, by manipulating individual terms. While this is a very direct approach, it is quite slow. The method reducible_by gives a test for divisibility.

def subst(f,x,c): 
    if c==1: 
        return sum([t/x for t in f.terms() 
            if t.reducible_by(x)])+\ 
            sum([t for t in f.terms() 
                if not t.reducible_by(x)]) 
        return sum([t for t in f.terms() 
            if not t.reducible_by(x)])

Solution 1: Set operations In fact, the problem can be tackled quite efficiently using set operations.

def subst(f,x,c): 
   c=BooleConstant(c) # if c was int is now converted mod 2, 
   #so comparison to int(0) makes sense 
   if c==0: 
       #terms with x evaluate to zero 
       return Polynomial(s.subset0(i)) 
       return Polynomial(s.subset1(i))+Polynomial(s.subset0(i))

Solution 2: Linear Lexicographical Lead rewriting systems On the other hand, this linear rewriting forms a rewriting problem and can be solved by calculating a normal form against a Gröbner basis. In this case the system is {x + c}∪{x21 + x1,,x2n + xn} (we assume that x = xi for some i). For this special case, that all Boolean polynomials have pairwise different linear leading terms w. r. t. lexicographical ordering, there exist special functions. First, we encode the system {x + c} into one diagram


This is a special format representing a set of such polynomials in one diagram, which is used by several procedures in PolyBoRi. Then we may reduce f by this rewriting system


This can be simplified in our special case in two ways.

  1. If our system consists of exactly one Boolean polynomial, ll_encode does essentially a type conversion only (and much overhead). This type conversion can be done implicitly (at least using the boost::python-based interface ipbori).

    So you may call


    In this case, there is no need for calling ll_encode. The second argument is converted implicitly to BooleSet.

  2. A second optimization is to call just

    Note, that {x + c} is a reduced Boolean Gröbner basis: Equivalently

           2          2        2
{x + c,x1 +x1,...,xn + xn}∖{x + x}

    is a reduced Gröbner basis).

2.5.2 Evaluate a polynomial by plugging in a constant for each variable

We want to a polynomial f(x1,,xn) by xi↦→ci, where c1,,cn are constants.

Naive approach First, we show it in a naive way, similar to the first solution above.

def evaluate(f,m): 
    for term in f.terms(): 
        for variable in term.variables(): 
    return Polynomial(res)

Solution 1: n set operations The following approach is faster, as it does not involve individual terms, but set operations

def evaluate(f,m): 
   while not f.constant(): 
       if c==0: 
           #terms with x evaluate to zero 
           f=Polynomial(nav.then_branch(), f.ring()) 
           f=Polynomial(nav.then_branch(), f.ring())+ 
              Polynomial(nav.else_branch(), f.ring()) 
       return f

For example, the call


results in 1.

We deal here with navigators, which is dangerous, because they do not increase the internal reference count on the represented polynomial substructure. So, one has to ensure, that f is still valid, as long as we use a navigator on f. But it will show its value on optimized code (e. g. PyRex), where it causes less overhead. A second point, why it is desirable to use navigators is, that their then_branch- and else_branch-methods immediately return (without further calculations) the results of the subset0 and subset1-functions, when the latter are called together with the top variable of the diagram f. In this example, this is the crucial point in terms of performance. But, since we already call the polynomial construction on the branches, reference counting of the corresponding subpolynomials is done anyway.

This is quite fast, but suboptimal, because only the inner functions (additions) use caching. Furthermore, it contradicts the usual ZDD recursion and generates complex intermediate results.

Solution 2: Linear Lexicographical Lead rewriting systems The same problem can also be tackled by the linear-lead routines. In the case, when all variables are substituted by constants, all intermediate results (generated during ll_red_nf_redsb/ll_red_nf_noredsb) are constant. In general, we consider the overhead of generating the encoding d as small, since it consists of very few, tiny ZDD operations only (and some Python overhead in the quite general ll_encode).


Since the tails of the polynomials in the rewriting system consist of constants only, this forms also a reduced Gröbner basis. Therefore, you may just call


This is assumed to be the fastest way.

2.5.3 General Linear Lexicographical Lead Rewriting Systems

We used ll_red_nf_redsb/ll_red_nf_noredsb functions on rewriting systems, where the tails of the polynomials was constant and the leading term linear. They can be used in a more general setting (which allows to eliminate auxiliary variable).

Definition 2 Let L be a list of Boolean polynomials. If all elements p of L have pairwise different leading terms with respect to lexicographical ordering, then we call L a linear lexicographical lead rewriting system.

We know that such a system forms together with the complete set of field equations a Gröbner basis w. r. t. lexicographical ordering.

In particular we can use ll_red_nf_redsb to speedup substitution of a variable x by a value v also in the more general case, that the lexicographical leading term of x + v is equal to x. This can be tested most efficiently by the expression


In many cases, we have a bigger equation system, where many variables have a linear leading term w. r. t. lexicographical ordering (at least one can optimize the formulation of the equations to fulfill these condition). These systems can be handled by the function eliminate in the module polybori.ll. I returns three results:

  1. A maximal subset L of the equation system, which forms a linear lexicographical lexicographical rewriting system.
  2. A normal form algorithm f, s. th. f(p) forms a reduced normal form of p against the Gröbner basis consisting of L and the field equations.
  3. A list of polynomials R, which are in reduced normal form against L, s. th. L R spans modulo field equations the same ideal as the original equation system.
In [1]: from polybori.ll import eliminate 
In [2]: E=[x(1)+1,x(1)+x(2),x(2)+x(3)*x(4)] 
In [3]: (L,f,R)=eliminate(E) 
In [4]: L 
Out[4]: [x(1) + 1, x(2) + x(3)*x(4)] 
In [5]: R 
Out[5]: [x(3)*x(4) + 1] 
In [6]: f(x(1)+x(2)) 
Out[6]: x(3)*x(4) + 1