One of the most challenging problems when trying to describe cryptographic primitives in SAT solvers is the XOR function that is used very often in cryptography. MiniSat (and most DPLL-based SAT solvers) only understands the Conjunctive Normal Form, or CNF for short. However, to describe a XOR function in CNF you need to have 2^{n-1} clauses, where n is the size of your XOR function. To overcome this exponential explosion, XOR functions are cut up into manageable sizes (6-7) and then implemented in 2^5–2^6 clauses each. This is not only tedious, uses a lot of memory and slow, but also makes it impossible to do interesting operations on XORs directly, such as XOR-ing two XORs to knock out variables. Note that CryptoMiniSat 2.0 and above can recover the XOR clauses from the CNF, but it is still of considerable interest in using the XOR notation described below.

In CryptoMiniSat, the DIMACS standard format is augmented with the following extension: having an “x” in front of a line makes that line an XOR clause. For instance, the line

x10 2 7 0

means that

v10 + v2 + v7 = true (where + is the binary XOR)

If we wish to invert the xor-clause, it is sufficient to invert one of the variables:

x10 2 -7 0

has now the XOR is inverted (i.e. it is equated to false):

v10 + v2 + v7 = false (where “+” is the binary XOR)

Naturally, if two variables are inverted, their inversions cancel each other out, and the XOR is equated to true. There is no need to cut up XOR clauses to smaller sizes, they can be of any length. Using this representation instead of the cut-and-convert-CNF will give you approximately 2x the speed, lots of memory savings and a potentially more understandable CNF file.