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

1 2 |
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:

1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
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.