msoos
commented
3 months ago 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 0And a == -b encodes to:
38 a b 0
38 -a -b 0You 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!
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.