XOR clauses

[lazarescusimona]

Hi!

I tried to use this solver for inputs that look like this:

p wcnf 6 15 21
x 21 1 0
x 21 2 0
x 21 3 0
x 21 4 0
x 21 5 0
x 21 6 0
x 21 2 5 0
x 21 2 3 4 5 6 0
x 21 1 2 4 5 6 0
x 21 1 3 4 5 0
x 21 2 3 5 0
x 21 4 5 6 0
x 21 4 5 6 0
x 21 2 5 6 0
x 21 2 3 4 5 6 0

Because XOR constraints must be at least 3-long, I transformed the above input in:

wcnf 22 16 38
x 38 1 2000 2001 0
x 38 2 2002 2003 0
x 38 3 2004 2005 0
x 38 4 2006 2007 0
x 38 5 2008 2009 0
x 38 6 2010 2011 0
x 38 2 5 2012 0
x 38 2 3 4 5 6 0
x 38 1 2 4 5 6 0
x 38 1 3 4 5 0
x 38 2 3 5 0
x 38 2013 2014 2015 0
x 38 4 5 6 0
x 38 4 5 6 0
x 38 2 5 6 0
x 38 2 3 4 5 6 0

where I added some new variables (which I no longer use elsewhere) in order to make an XOR constraint of length 3.

This idea works for small inputs, but when I try to apply the same method on bigger inputs (for example, 500 variables and 700 constraints), I get a segmentation fault error message. I leave an input file for this case here: https://filetransfer.io/data-package/iTkNZKGW#link

Do you have any suggestions on what I could do in this case? Thank you.

[msoos]

Hi,

For 2-long XORs you don't need XORs at all. Just encode them as regular clauses:

a == b encodes to:

38 a -b 0
38 -a b 0

And a == -b encodes to:

38 a b 0
38 -a -b 0

You don't need, and shouldn't use XORs for that. I'll look into the segmentation fault, though, that shouldn't happen.

BTW, I would discourage you from adding these constraints. If a == b then just replace "a" with "b" everywhere. Similarly, if a == -b, then just replace "a" with "-b" everywhere. I suggest thinking about what kind of improvements like this you can do to your encoding. Encoding matters.. a lot :) There are of people who work on tricks like this a good chunk of their research career... me included :D I suggest to read some encoding papers, you may be able to get some ideas for tricks like this for your encoding!

[msoos]

Ooopppss... sorry, I won't be able to debug this in the next 6 days because I forgot to copy over my academic CPLEX license to my new computer and I'm away from home. So I can't run the tool. Sorry. I'll fix this when I get home.

HOWEVER.... your WCNF is actually just a CNF? It doesn't have any clauses that are soft clauses. So you shouldn't be using a MaxSAT solver anyway. Just change "p wcnf 586 701 1287" to "p cnf 586 701" and remove the "x 1287 " in front of everything and replace it with "x ", and then use cryptominisat: https://github.com/msoos/cryptominisat It will then work flawlessly.

Also... you have ONLY XOR constraints. This whole problem is just a big matrix. There is no need to even use CryptoMiniSat. Just use a solver Gauss-Jordan elimination from some math library. This whole thing sounds so strange. I'm sorry, I'm not sure I can help you much beyond this point. You seem to be using an unnecessary complication of a tool, GaussMaxHS, to solve a problem that can be solved with tools from a standard math library from the 1960s. I'm confused. Please use a standard math library.

Thanks,

Mate