» ANF to CNF conversion Homepage of Mate Soos

ANF to CNF conversion

Posted by msoos on July 6, 2010

Posted in: SAT. Tagged: ANF, CNF, Grain of Salt, Sage. 28 comments

Algebraic Normal Form, or simply ANF, is the form used to describe cryptographic functions. It looks like this:
0 = a*b + b*c + b + d 0 = b*c + c + a ...Where a...d are binary variables, the “+” sign is binary XOR, and the “*” sign is binary AND. Every item that is connected with the XOR-s is called a monomial, and its degree is the number of independent variables inside it. So, a*b is a 2-degree monomial in the first equation, and c is a 1-degree monomial in the second equation.

An important problem when dealing with cryptographic functions in SAT is to translate the ANF into the input of SAT solvers: Conjunctive Normal Form, or simply CNF. A CNF formula looks like this:
a V b V c = true a V -d = true ...Where again a...d are binary variables, the “V” sign is the binary OR, and the “-” sign is the binary NOT (i.e. inverse).

The most quoted article about ANF-to-CNF translation is that by Courtois and Bard, which advocates for the following translation process:

Introduce internal variables for every monomial of degree larger than 1
Describe the equations as large XORs using the recently introduced variables

According to this method, the equations presented above are first translated to the following form:
int_var1 = a*b int_var2 = b*c false = int_var1 + int_var2 + b + d false = int_var2 + c + a
Then, each of the above equations are translated to CNF. The internal variables are translated as such:

(translation of int_var1 = a*b :)
int_var1 V -a V -b = true -int_var1 V a = true -int_var1 V b = true

(translation of int_var2 = b*c :)
int_var2 V -b V -c = true -int_var2 V b = true -int_var2 V c = true

And the XOR-s are translated as such:
(translation of false = int_var1 + int_var2 + b + d :)
-int_var1 V int_var2 V b V d = true int_var1 V -int_var2 V b V d = true int_var1 V int_var2 V -b V d = true int_var1 V int_var2 V b V -d = true -int_var1 V -int_var2 V -b V d = true -int_var1 V -int_var2 V b V -d = true -int_var1 V int_var2 V -b V -d = true int_var1 V -int_var2 V -b V -d = true

(translation of false = int_var2 + c + a :)
int_var2 V c V -a = true int_var2 V -c V a = true -int_var2 V c V a = true -int_var2 V -c V -a = true

We are now done. The final CNF file is this. This final CNF has a small header, and some fluffs have been removed: variables are not named, but referred to with a number, and the = true-s have been replaced with a line-ending 0.

As you can imagine, there are many ways to enhance this process. I have written a set of them down in this paper. The set of improvements in a nutshell are the following:

If a variable’s value is given, (e.g. a = true), first substitute this value in the ANF, and transcribe the resulting ANF to CNF.
If there are two monomials, such as: a*b + b in an equation, make a non-standard monomial (-a)*b from the two, and transcribe this to CNF. Since the CNF can use negations, this reduces the size of the resulting CNF
If the ANF can be described using Karnaugh maps shorter than with the method presented above, use that translation method.

I just got a nice script to perform step (1) from Martin Albrecht, one of the developers of Sage:

sage: B = BooleanPolynomialRing(4500,'x')
sage: L = [B.random_element(degree=2,terms=10)
      for _ in range(4000)]
sage: s = [B.gen(i) + GF(2).random_element()
      for i in range(1000)]
sage: %time F =
      mq.MPolynomialSystem(L+s).
      eliminate_linear_variables(maxlength=1)
CPU time: 1.03 s,  Wall time: 1.11 s

In this code, Martin generates a boolean system of equations with 4500 variables, with 4000 random equations each with randomly selected monomials of degree 2 and of XOR size 10. Then, he sets 1000 random variables to a random value (true or false), and finally, he substitutes the assigned values, and simplifies the system. If you think this is a trivial issue, alas, it is not. Both Maple and Sage take hours to perform it if using the standard eval function. The function above uses a variation of the ElimLin algorithm from the Courtois-Bard paper to do this efficiently.

28 comments on “ANF to CNF conversion”

Aditya Parab on December 20, 2010 at 2:56 pm said:

Sir,
i would like to know how to convert a given ANF to CNF manually for small number of variables. Please help.

Reply
- msoos on December 21, 2010 at 12:45 pm said:
  
  Hi Aditya,
  
  If you read the post, you can see that that’s exactly what I did: I manually transformed an ANF to CNF, step by step. Each step was generic, so this works for any ANF of any number of variables. In particular, if your ANF if small, with small number of variables, you should be able to do this step by step by hand, as I have done, and come up with a manual translation of your ANF.
  
  Basically, you have to create a new variable for each new monomial, and then you have to encode your XORs each with 2^(n-1) clauses, where “n” is the size of the XOR. That’s it :)
  
  Reply
Arthy on March 30, 2011 at 10:49 am said:

i want a program that converts from anf to cnf..
i tried to install grain of salt. It is showing some installation error. Is there any specific version for boost c++ library to install?

Reply
- msoos on March 30, 2011 at 3:39 pm said:
  
  Here is one, written in C: http://gitorious.org/anf2cnf/anf2cnf The input format to the “anf2cnf”binary is not trivial, though. An example input is this:
  
  2065,2073,||
  2307,2315,2744,|2061,|2069,2711,|2069,2719,|2076,|2295,2711,|2295,2719,|2317,2711,|2317,2719,|2711,|14580,||
  251,||
  
  Monomials are separated with a “|”, and variables inside them are separated with a “,”. The empty monomial is the TRUE constant. So var 251 is set to TRUE here, for example.
  
  Grain-of-Salt needs some ancient boost library, but I thought it should compile with the newer ones, too. BTW, Grain-of-Salt is not a proper ANF-to-CNF converter. It does that, too, but that particular part is not accessible from the outside, sorry :(
  
  Reply
  - Arthy on April 1, 2011 at 7:01 am said:
    
    I tried the converter said by you in the above link… again it is showing some errors..
    the error was like “MTRand/MersenneTwister.h : No such file or directory” and many errors. I got this particular error when the system was compiling “bestbits.cpp”. I searched for the file in the net and created a directory MTRand and put the file MersenneTwister.h and i tried again and ended up unsuccessful. Will you please guide me for installing the same.
    
    Reply
  - Arthy on April 1, 2011 at 7:49 am said:
    
    Sir,
    I have installed anf2cnf – highdegree…
    after installing, there are four object files. they are “anf2cnf,SATsolve, parseanf,chronoanftocnf” .
    i executed by issuing the command ./anf2cnf
    In the file i gave the input which was given by as an example in the above reply. But it showed me an error as “bad format”.
    
    Reply
    - msoos on April 1, 2011 at 12:32 pm said:
      
      (First of all, forget the “sir” — I am probably younger than you are). Sorry about the missing “MTRand” — I have added it now. It should now compile out of the box if you have a C compiler installed. As for the error with “anf2cnf”, I think your problem may be that you are using Windows, and the end-of-line character is not only a “n” but also a carry-return. You must have only a “n” at the end of each line. Also, don’t leave empty lines, and don’t leave spaces at the end of the lines. For me, the output of that example 3 lines with “anf2cnf” is:
      
      $ ./anf2cnf myfile x1 0 x4 8 9 12 14 15 17 18 20 11 21 0 x22 0 1 -2 -3 0 -1 2 0 -1 3 0 4 -5 -6 -7 0 -4 5 0 -4 6 0 -4 7 0 9 -10 -11 0 -9 10 0 -9 11 0 12 -10 -13 0 -12 10 0 -12 13 0 15 -16 -11 0 -15 16 0 -15 11 0 17 -16 -13 0 -17 16 0 -17 13 0 18 -19 -11 0 -18 19 0 -18 11 0 20 -19 -13 0 -20 19 0 -20 13 0 c c Mapping literals < -> monomials: c 1 := x[2065]*x[2073] c 2 := x[2065] c 3 := x[2073] c 4 := x[2307]*x[2315]*x[2744] c 5 := x[2307] c 6 := x[2315] c 7 := x[2744] c 8 := x[2061] c 9 := x[2069]*x[2711] c 10 := x[2069] c 11 := x[2711] c 12 := x[2069]*x[2719] c 13 := x[2719] c 14 := x[2076] c 15 := x[2295]*x[2711] c 16 := x[2295] c 17 := x[2295]*x[2719] c 18 := x[2317]*x[2711] c 19 := x[2317] c 20 := x[2317]*x[2719] c 21 := x[14580] c 22 := x[251]
      
      If you install “CryptoMiniSat” to the path ($PATH in linux) you can also use “SATSolve” to solve “myfile”, like this:
      
      ./SATsolve myfile propagate: 0.000000 anf2cnf: 0.000000 c Outputting solution to file: /tmp/sol.rcQAtO c This is CryptoMiniSat 2.9.0 c WARNING: for repeatability, setting FPU to use double precision c Reading file '/tmp/cnf.dWSZzx' c -- clauses added: 0 learnts, 25 normals, 2 xors c -- vars added 21 c Parsing time: 0.00 s c N st 0 0 21 7 15 0 63 0 no data no data -- c asymm cl-useful: 0/7/7 lits-rem:0 time: 0.00 c Flit: 0 Blit: 0 bXBeca: 0 bXProp: 0 Bins: 0 BRemL: 0 BRemN: 0 P: 0.0M T: 0.00 c bin-w-bin subsume rem 0 bins time: 0.00 s c subs with bin: 0 lits-rem: 0 v-fix: 0 time: 0.00 s c Subs w/ non-existent bins: 0 l-rem: 0 v-fix: 0 done: 18 time: 0.00 s c Removed useless bin: 0 fixed: 0 props: 0.00M time: 0.00 s c lits-rem: 0 cl-subs: 0 v-elim: 6 v-fix: 0 time: 0.00 s c Finding binary XORs T: 0.00 s found: 0 c Finding non-binary XORs: 0.00 s (found: 0, avg size: -nan) c calculated reachability. Time: 0.00 c Calc default polars - time: 0.00 s pos: 2 undec: 9 neg: 10 c ========================================================================================= c types(t): F = full restart, N = normal restart c types(t): S = simplification begin/end, E = solution found c restart types(rt): st = static, dy = dynamic c t rt Rest Confl Vars NormCls BinCls Learnts ClLits LtLits c B st 0 0 12 6 6 0 41 0 no data no data -- c E st 1 0 0 6 6 0 41 0 no data no data -- c Verified 7 clauses. c Solution needs extension. Extending. c Verified 7 clauses. c num threads : 1 c restarts : 1 c dynamic restarts : 0 c static restarts : 1 c full restarts : 0 c total simplify time : 0.00 c learnts DL2 : 0 c learnts size 2 : 15 c learnts size 1 : 3 (14.29 % of vars) c filedLit time : 0.00 (-nan % time) c v-elim SatELite : 6 (28.57 % vars) c SatELite time : 0.00 (-nan % time) c v-elim xor : 0 (0.00 % vars) c xor elim time : 0.00 (-nan % time) c num binary xor trees : 0 c binxor trees' crown : 0 (-nan leafs/tree) c bin xor find time : 0.00 c OTF clause improved : 0 (-nan clauses/conflict) c OTF impr. size diff : 0 (-nan lits/clause) c OTF cl watch-shrink : 0 (-nan clauses/conflict) c OTF cl watch-sh-lit : 0 (-nan lits/clause) c tried to recurMin cls : 0 (-nan % of conflicts) c updated cache : 0 (-nan lits/tried recurMin) c clauses over max glue : 0 (-nan % of all clauses) c conflicts : 0 (-nan / sec) c decisions : 6 (0.00 % random) c bogo-props : 440 (inf / sec) c conflict literals : 0 (-nan % deleted) c Memory used : 11.04 MB c CPU time : 0.00 s c SAT [ [ #, #, #, #, #, #, #, #, #, #, #, #, #, #, #, #, #, #, #, #, #, #, #, #, #, #, #, #, #, #, ... #, #, #, #, #, #, #, #, #, #, #, #, #, #, #, #, #, #, #, #, #, 0 ] ]
      
      Reply
Cécilia on May 24, 2011 at 2:49 pm said:

Sir,

I would like a ANF-to-CNF converter. Where can I download it? And what language is used? (I need to compile with Windows). Thank you for your help.
Can I speak French with you ?

Regards,

Cécilia

Reply
Nat on May 25, 2011 at 4:08 pm said:

Dear msoos,

I’ve installed anf2cnf – highdegree and i took the same example 3 lines above but I have the error :
“assertion “false” failed: file “libanf2cnf.cpp”, line 84, function: int hash_monomial
Aborted “. What did you think about it?

Reply
- msoos on May 29, 2011 at 8:51 pm said:
  
  Thank you for telling me about this! Sorry, the branch “highdegree” was wrong. It has now been deleted, so it will not confuse others :) The branch to use is “master”. I hope you will find it useful!
  
  Mate
  
  Reply
Arthy on June 2, 2011 at 11:34 am said:

With reference to your paper titled “Extending SAT Solvers to Cryptographic problems”, I tried for Trivium cipher, and i got the following results
guess bits time in sec
10 0.03
20 0.04
30 0.043
40 0.028
50 0.028
60 0.02
I used grain of salt for converting from ANF to CNF. and the command i used was “./grainofsalt –num 100 –outputs 90 –crypto trivium –probBits 20″, For guess bits 20.
Then i used cryptominisat for calculating the time required for solving the CNF files.
As far as i understood, if the guess bits decreases then the time required should increase. But in my case the time increases and decreasing again.(The result is shown above). Will you please help me where I have gone wrong?
Is the time for executing the SAT solver the “CPU time” displayed as the result of executing the SAT solver?

Reply
- msoos on June 3, 2011 at 12:36 am said:
  
  Hi,
  
  90 bits of output is very low for Trivium because if you look at the trivium configuration file, it says:
  
  init_clock = 0
  
  which means that initialisation is not part of the configuration — you have to add that yourself. It would mean that you add the correct number in the config file, and you generate the correct
  
  feedback_init.txt
  
  files in each of the sr0, sr1, sr2 subdirectories. Otherwise, the program will be generating problems without initialisation — and for that, you need to have as many output bits as the size of the cipher state, which is much more than 90.
  
  I hope I have helped,
  
  Mate
  
  Reply
Akshay Gupta on June 2, 2011 at 5:35 pm said:

Sir

Can you give example to convert a cubic polynomial as you did with a quadratic equation in this paper

Thank You

Reply
- msoos on June 3, 2011 at 12:18 am said:
  
  Hi,
  
  For example, the representative ‘int_var1′ of the monomial
  
  a*b*c
  
  i.e. the equation
  
  int_var1 = a*b*c
  
  can be described in CNF like this:
  
  int_var1 V -a V -b V -c -int_var1 V a -int_var1 V b -int_var1 V c
  
  All the rest is the same as per the original blog post. I have simply replaced
  
  int_var1 = a*b
  
  with
  
  int_var1 = a*b*c
  
  changing the equation
  
  0 = a*b + b*c + b + d
  
  to
  
  0 = a*b*c + b*c + b + d
  
  Reply
Akshay Gupta on June 5, 2011 at 9:50 am said:

Sir,

I am trying to implement an anf-cnf converter based on your conversion algorithm, can you tell me the standard format for input file, for anf equations.
Thank You

Reply
- msoos on June 5, 2011 at 11:44 am said:
  
  Hi,
  
  Try out this implementation:
  
  http://gitorious.org/anfconv
  
  It’s input format is:
  
  x1 + x2 * x3
  x2 + x1 * x4
  
  and the output format is DIMACS CNF. Maybe you will find this software useful. If you find any bugs, send them over to soos@srlabs.de
  
  Reply
Akshay Gupta on June 8, 2011 at 10:05 am said:

Sir,

I have few doubts regarding your algorithm for conversion:

1) To convert XOR’s in the given equation:
false = int_var1 + int_var2 + b + d

You used:
-int_var1 V int_var2 V b V d = true
int_var1 V -int_var2 V b V d = true
int_var1 V int_var2 V -b V d = true
int_var1 V int_var2 V b V -d = true
-int_var1 V -int_var2 V -b V d = true
-int_var1 V -int_var2 V b V -d = true
-int_var1 V int_var2 V -b V -d = true
int_var1 V -int_var2 V -b V -d = true

But For: false = int_var2 + c + a

You used:
int_var2 V c V -a = true
int_var2 V -c V a = true
-int_var2 V c V a = true
-int_var2 V -c V -a = true

According to the first equation clauses, shouldn’t the second equation clauses be these:

int_var2 V c V -a = true
int_var2 V -c V a = true
-int_var2 V c V a = true
-int_var2 V -c V a = true
int_var2 V -c V -a = true
-int_var2 V c V -a = true

2) The algo you have given is for:
0 = a*b + b*c + b + d

What if instead of 0 there was a 1 i.e:
1 = a*b + b*c + b + d

Thank you

Reply
- Mate Soos on June 8, 2011 at 1:21 pm said:
  
  Hi,
  
  0) (*please* don’t call me sir)
  
  1) The equations are correct. Think of the clauses as banning solutions. These are not trivial, you have to think through them again and again to understand them. Observe, for instance, that in my solution, the same XOR is only described with the same even/odd number of inversions in the clauses. You have both odd and even number of inversions describing the same XOR — that is impossible.
  
  2) If there is a constant as well, then the number of inversions goes from odd to even and vice-versa.
  
  I hope I have helped!
  
  Reply
Arthy on June 14, 2011 at 8:43 am said:

what value should be set to init_clock in case of trivium? do you i have to change sr0,sr1,sr2, feedback_init.txt manually after setting init_clock?

Reply
- Soos Mate on June 14, 2011 at 4:19 pm said:
  
  Hi Arthy,
  
  Please refer to Trivium’s and Grain of Salt’s documentation, both available online.
  
  Mate
  
  Reply
Akshay on July 6, 2011 at 7:51 pm said:

Hi,

I implemented a anf-cnf converter using C based on the algorithm in this page, however i am now trying to develop a cnf-anf converter and combine them, can you also give the algorithm for cnf-anf conversion.

Thanks

Reply
- Mate Soos on July 7, 2011 at 10:28 am said:
  
  Hi,
  
  Well, if you have implemented it, why don’t you share it with us? I think it’s only fair that I will give a description of how to do CNF->ANF only if you share your code with us :) It’s a give&take game, not a take&take one ;)
  
  Mate
  
  Reply
Akshay Gupta on July 14, 2011 at 12:13 pm said:

Hi,

Can you please now share the cnf-anf algorithm so that I can make a cnf-anf converter

Thank You

Reply
- Mate Soos on July 16, 2011 at 12:05 pm said:
  
  Hi Akshay Gupta,
  
  I will write a blog post soon about CNF->ANF. In your program, I think you forgot to check the input, and it seems to lack documentation :( It’s best to open an account at gitorious.org, upload your source there, and add a README with input requirements, output format, and some usage info :)
  
  Mate
  
  Reply
akshay on July 17, 2011 at 1:06 pm said:

Hi Mate,

Thnks for the feedback :) I am out of town right now. but i will soon post the full anf-cnf convertor with documentation asap.

Akshay

Reply
Akshay on July 22, 2011 at 11:55 am said:

Hi,

I have finished debugging the anf-cnf converter, the read-only link for the files is:

svn checkout http://anf-cnf-converter.googlecode.com/svn/trunk/ anf-cnf-converter-read-only

For any suggestions or doubts please mail me at akshay10010@iiitd.ac.in

For demo input file please refer to the demo.txt file and Read me.

Hoping that you will upload the algorithm for cnf-anf converter soon.

Thanks

Reply
- Akshay on July 24, 2011 at 11:07 am said:
  
  Hi,
  
  I noticed that the access to the code was getting a little messy, so I uploaded it in a new project it’s link is: http://anf-cnf.googlecode.com/svn/trunk/convert/.
  
  To download the code please refer to Read me file, it has a How to download section.
  
  Thanks
  
  Reply
Lynn on May 18, 2012 at 10:04 am said:

Hi,
I have tried this tool and I got an incorrect result as follow:

B. = BooleanPolynomialRing()
solver = ANFSatSolver(B)
print solver.cnf([a*b + b*c + b + d, b*c + c + a])

p cnf 6 14
c ——————————
c Next definition: a*b + b*c + b + d
-3 -5 -2 -6 0
3 5 -2 -6 0
3 -5 2 -6 0
3 -5 -2 6 0
-3 5 2 -6 0
-3 5 -2 6 0
-3 -5 2 6 0
3 5 2 6 0
c ——————————
c Next definition: a + b*c + c
c ——————————
c Next definition: monomial a*b
1 -3 0
2 -3 0
3 -1 -2 0
c ——————————
c Next definition: monomial b*c
2 -5 0
4 -5 0
5 -2 -4 0

could you please help me with this problem?

Thanks!

Reply