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\} \cup \{{x_1^2+x_1,\ldots,x_n^2+x_n}\}$ (we assume that $ x=x_i$ 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

d=ll_encode([x+c])
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
ll_red_nf_noredsb(f,d)
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 implicitely (at least using the boost::python-based interface ipbori).

    So you may call

    ll_red_nf_noredsb(f,x+c)
    
    In this case, there is no need for calling ll_encode. The second argument is converted implicitely to BooleSet.
  2. A second optimization is to call just
    ll_red_nf_redsb(f,x+c)
    
    As $ \{x+c\}$ is a reduced Boolean Gröbner basis (equivalently $ \{x+c,{x_1^2+x_1,\ldots,x_n^2+x_n}\}\backslash \{x^2+x\}$ is a reduced Gröbner basis).

2009-04-03