CNF with XOR extension

[aljungberg]

Some ANF systems with long XOR equations really blow up when converted to CNF and use massive amounts of RAM plus introduce additional temporary variables and clauses which slow down the SAT solver.

Since Bosphorus uses Crytpominisat for the SAT stage, shouldn't it use XOR clauses, at least internally?

I don't know exactly what CMS does with the XOR clauses. Maybe it cuts them internally to fit into its CNF based solving strategies. But even if it does cut internally, at least it doesn't need to spend time in the XOR recovery stage mentioned in the blog post.

[msoos]

Hi,

Thanks for filing the issue! See below for the actual solution. Now for some background :) The newer CryptoMiniSat doesn't have special data structure for XOR clauses and hence they do indeed take up memory and are slower to run than with the old CryptoMiniSat. However, for the vast majority of problems, this trade-off is okay, as the improved inprocessing systems more than make up for it. It is however possible that for your particular problem domain this may slow down solving.

So, I have worked a few hours today to fix this. We now support XOR clauses as an output format, yay! Please git pull and re-compile, then pass the parameter --xorclause and it will then emit XOR clauses whenever possible. For example:

$ cat a2.anf 
x0 + x1 + x1*x2 + x2 + x3 + x4 + x5 + x6 + x7 + x8

$ ./bosphorus --xorclause --anfread a2.anf --cnfwrite b2.cnf

$ cat b2.cnf
-10 2 0
-10 3 0
10 -2 -3 0
x1 10 2 3 4 5 6 7 8 9 0

You can then use the last version of CryptoMiniSat that naively used XOR clauses, here:

https://www.msoos.org/largefiles/cryptominisat-cryptominisat-strange-night2-st.tar.gz

It's the version from the SAT Competition of 2011. Again, a lot of improvements have gone into CryptoMiniSat since, but if this turns out to be faster in your case, that's possible.

I believe this solves the issue, so I'm closing it. In case you have another query, please open another issue if it's different than this one. If it's the same, you can just comment here and I'll re-open the issue.

[aljungberg]

That's brilliant, thank you very much!

It makes sense that the new CryptoMiniSat doesn't use a special structure for XORs. It must add a lot of complexity and overhead to have more than one fundamental data structure. Every strategy will become different if you have propagation and constraints in two data structures.

Either way this change will be really helpful. I'm very curious about what difference using CryptoMiniSat 2011 will make. Thanks again!

[saadislamm]

I am getting different solutions with and without --xorclause

$ cat book_eg.anf 
1 + x1 + x2 + x3 + x0*x3 + x2*x3
x1+ x3 + x0*x1+ x0*x2 + x0*x3 + x1*x2 + x1*x3 + x2*x3 + 1
x0 + x2 + x0*x1+ x1*x3 + x2*x3
x1+ x0*x1+ x0*x2 + x0*x3 + x2*x3 + 1

$ ./bosphorus --anfread book_eg.anf --cnfwrite book_eg.cnf
$ cat book_eg.cnf 
1 2 0
-1 -2 0
-1 3 0
1 -3 0
-4 0
c Learnt 4 fact(s)

$ ./bosphorus --xorclause --anfread book_eg.anf --cnfwrite book_eg_xor.cnf
$ cat book_eg_xor.cnf 
x-1 2 0
x1 3 0
x4 0
c Learnt 4 fact(s)

$ ./cryptominisat5 --maxsol 16 book_eg.cnf
s SATISFIABLE
v -1 2 -3 -4 0
c Number of solutions found until now:      1
s SATISFIABLE
v 1 -2 3 -4 0
c Number of solutions found until now:      2

$ ./cryptominisat5 --maxsol 16 book_eg_xor.cnf
s SATISFIABLE
v -1 -2 3 4 0
c Number of solutions found until now:      1
s SATISFIABLE
v 1 2 -3 4 0
c Number of solutions found until now:      2

The solutions I found without --xorclause are correct and with --xorclause are incorrect. Am I doing something wrong?

[msoos]

Oh, thank you so much for letting us know about this bug I introduced! I have now disabled this option so it will not be able to produce incorrect results in the future. Unfortunately, currently I don't have the time to fix this issue :( I will, however make sure to use the above bug report to test the system when I get a chance to fix it :)

In the meanwhile, please feel free to try to fix the issue. Bosphorus is open source software, and you are very welcome to create a pull request as per:

https://help.github.com/en/github/collaborating-with-issues-and-pull-requests/about-pull-requests

to fix the issue. Thanks a lot in advance for looking into it,

Mate

[msoos]

Hey! I have improved the tool a lot in the past weeks, thanks to your and other's suggestions. I still don't have XOR clauses, but it now can tell you the number of solutions from the tool itself and it has been fuzzed extensively so I don't bump into the issue you have mentioned above :) So, things should be a lot more reliable and it will be easier to find bugs than before.

To find all solutions:

docker run --rm -v `pwd`/:/dat/ msoos/bosphorus \
    --anfread /dat/myfile.anf \
    --cnfwrite /dat/myfile.cnf \
    --solve --allsol
[...]
s ANF-SATISFIABLE
v x(0) x(1) x(2) x(3)
s ANF-SATISFIABLE
v x(0) x(1) 1+x(2) 1+x(3)
s ANF-UNSATISFIABLE
c Number of solutions found: 2

All solutions are verified against the ANF. The README additionally contains a section about fuzzing that explains how to use the fuzzer. Things should be a lot better now :) I hope you appreciate the work we put into the tool and continue using it! Thanks again for your issue, I hope you can see it helped us make the tool better by making it more robust using a fuzzer.