Sophie

Sophie

distrib > Fedora > 20 > x86_64 > by-pkgid > 53417a31cb7f91df32eca97b9c946a27 > files > 6

cryptominisat-libs-2.9.9-1.fc20.i686.rpm

******************
** XOR clauses ***
******************
If you want to express a xor, e.g.

"var1 + var2 + !var3 = true" 

then you simply need to put into the CNF file the line: 

"x1 2 -3 0"

The "x" in front of the line means that this is a xor-clause clause.


*************************************
** custom branching variable order **
*************************************
The CNF input may contain lines of the form:

    b 3 4 17 0
    b 10 0

This means that the solver will try to branch on the variables 3, 4, 17,
and 10, in that particular order, before branching on any other variables.
Remaining (unspecified) variables will use the regular variable selection
heuristic.

Above by: Vegard Nossum <vegardno@posco.ifi.uio.no>