There is an ANF (Algebraic Normal Form) to CNF (Conjunctive Normal Form) converter by Martin Albrecht in Sage. Essentially, it performs the ANF to CNF conversion that I have described previously in this blog entry. Me, as unsuspecting as anyone else, have been using this for a couple of days now. It seemed to do its job. However, today, I wanted to backport some of my ideas to this converter. And then it hit me.
Let me illustrate with a short example why I think something is wrong with this converter. We will try to encode that variable 0 and variable 1 cannot both be TRUE. This is as simple as saying x0*x1 = 0 in plain old math. In Sage this is done like this:
sage: B = BooleanPolynomialRing(10,'x') sage: load anf2cnf.py sage: anf2cnf = ANFSatSolver(B) sage: polynom = B.gen(0)*B.gen(1) sage: print polynom x0*x1
So far, so good. Let’s try to make a CNF out of this:
sage: print anf2cnf.cnf([polynom]) p cnf 4 6 2 -4 0 3 -4 0 4 -2 -3 0 1 0 4 1 0 -4 -1 0
Oooops. Why do we need 6 clauses to describe this? It can be described with exactly one:
p cnf 2 1 -1 -2
This lonely clause simply bans the solution 1 = TRUE, 2 = TRUE, which was our original aim.
Let me just mention one more thing about this converter: it repeats definitions. For example:
sage: print two_polynoms [x1*x2 + 1, x1*x2 + x1] sage: print anf2cnf.cnf(two_polynoms) p cnf 4 13 2 -4 0 3 -4 0 4 -2 -3 0 1 0 4 0 2 -4 0 3 -4 0 4 -2 -3 0 1 0 4 2 1 0 -4 -2 1 0 -4 2 -1 0 4 -2 -1 0
Notice that clause 2 -4 0 and the two following it have been repeated twice, as well as the clause setting 1 to TRUE.
I have been trying to get around these problems lately. When ready, the new script will be made available, along with some HOWTO. It will have some minor shortcomings, but already, the number of clauses in problem descriptions have dramatically dropped. For example, originally, the description of an example problem in CNF contained 221’612 clauses. After minor corrections, the same can now be described with only 122’042 clauses. This of course means faster solving, cleaner and even human-readable CNF output, etc. Fingers are crossed for an early release ;)
Comments
0 responses to “anf2cnf hell in Sage”
Sir,
Where should we keep the anf2cnf.py file to load it.
Just put it anywhere, and then type: “load PATH_TO_FILE” to load anf2cnf.py. I am on linux and I keep in in “/home/soos/devel/”, so I type: “load /home/soos/devel/anf2cnf.py”. If you want to solve using the MiniSat2 executable interface, you have to have minisat2 compiled as a binary, called “minisat2” (maybe with “.exe” at the end for windows) in the executable path — installing it into “/usr/bin” in linux does the trick, for windows you may have to put it into the point where “sage” is running from.
I hope I have helped!
Thank you sir. I will try it
Sir,
I want to enter a 1000 variable ANF equation in matrix form to be converted to cnf. Can you help me with the script.
What kind of matrix form? What do the columns represent?
Sir,
How to give complimented input in sage eg. {x0*(-x1)}
Hi Suhas,
Just write “polyRing.gen(0) * ( polyRing.gen(1) + polyRing.one() )”. Essentially, the “polyRing.one()” is the constant one, so adding that to a boolean variable complements it. I.e. in boolean terms: “a XOR 1 = -a”. BTW, I used something like “polyRing = BooleanPolynomialRing(10,’x’)”. I hope I have helped :)
thank you sir that worked
Hi mate,
in fact your second example ([x1*x2 + 1, x1*x2 + x1]) needs only 3 clauses and 2 variables:
p cnf 3 3
c x1*x2 + 1
1
2
c x1*x2 + x1 = x1*(x2+1)
-1 2
Is there a way to detect and to simplify these kind of unnecessary clauses ?
Hi,
Yes, I think this one gets around these problems.
Cheers,
Mate