I have finally managed to fix the script that converts ANF problems to CNF format in the Sage math system. The original script was having some problems that I blogged about. The new script has corrected most of the shortcomings of the original script, as well as added some textual help for the user.

For instance, the equations

sage: print two_polynoms
[x0*x1 + 1, x0*x1 + x1]

that last time required 13 clauses and 4 variables in CNF, now look like this:

sage: print anf2cnf.cnf(two_polynoms)
p cnf 3 6
c ------------------------------
c Next definition: x0*x1 + 1
3 0
c ------------------------------
c Next definition: x0*x1 + x1
3 -2 0
-3 2 0
c ------------------------------
c Next definition: monomial x0*x1
1 -3 0
2 -3 0
3 -1 -2 0

which is 1 variable and 7 clauses shorter than the original, not to mention the visually cleaner look and human-parseable output. The new script is available here. Hopefully, some of my enhancements included in the Grain-of-Salt package will be included in this script. The problem is mainly that Grain-of-Salt uses radically different data structures, and is written in a different programming language, so porting is not trivial.