Regarding SAT Solvers and cnf files

Question

I've been trying to use Cryptominisat (something similar will do) to formulate an attack on Piccolo, a lightweight block cipher, similar to AES.

The equations are something like this:

Z= z1|z2|...|z16, 1<= i<=16

Then, ui= (1+z(4i-3)) ^ (1+ z(4i-2)) ^ (1+z(4i-1)) ^ (1+ z(4i)), 1<=i<=4

Then, (1+u1) V (1+u2) V (1+u3) V (1+u4) =1; ui + uj=1, i<=i<=j<=4

I need some help regarding my next step. I have the CNF equations for the attack and the decryption ready, I really need help on how to use that with the sat solver and put it in a CNF file format. I've been looking all over the internet but there's no clear method given anywhere. Any help would be appreciated. If any more information is needed, please feel free to ask. I need to put the above equations in a cnf file.

Since the equations involved are quite complex(there are more), some references or examples for cnf files and their working would be awesome.

Answer 1

This specification of the CNF format might help you:

http://people.sc.fsu.edu/~jburkardt/pdf/dimacs_cnf.pdf

There are sample files linked on this page:

http://people.sc.fsu.edu/~jburkardt/data/cnf/cnf.html