anf2cnf hell in Sage

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 ;)


Posted

in

by

Tags:

Comments

0 responses to “anf2cnf hell in Sage”

  1. Aditya Parab Avatar
    Aditya Parab

    Sir,
    Where should we keep the anf2cnf.py file to load it.

    1. msoos Avatar

      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!

  2. Aditya Parab Avatar
    Aditya Parab

    Thank you sir. I will try it

  3. Aditya Parab Avatar
    Aditya Parab

    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.

    1. msoos Avatar

      What kind of matrix form? What do the columns represent?

  4. Suhas Waghmare Avatar
    Suhas Waghmare

    Sir,

    How to give complimented input in sage eg. {x0*(-x1)}

    1. msoos Avatar

      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 :)

      1. Suhas Waghmare Avatar
        Suhas Waghmare

        thank you sir that worked

        1. cgoyet Avatar
          cgoyet

          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 ?

          1. msoos Avatar
            msoos

            Hi,

            Yes, I think this one gets around these problems.

            Cheers,

            Mate