search

msoos / cryptominisat

An advanced SAT solver
https://www.msoos.org
Other
803 stars 179 forks source link

Assert Failure? #392

Closed cipherboy closed 7 years ago

cipherboy commented 7 years ago

No idea how, but I managed to trigger this assert:

https://github.com/msoos/cryptominisat/blob/6115500c11877ddb740d1475986b733542c077df/src/propengine.cpp#L321

I am recompiling from latest master and then will rerun the SAT (~2 days). Is this something known/fixed in master?

Command line:

$ ~/GitHub/cryptominisat/cryptominisat5 --threads=4 ./problem.cnf > problem.out
cryptominisat5: /home/cipherboy/GitHub/cryptominisat/src/propengine.cpp:321: CMSat::PropBy CMSat::PropEngine::propagate_any_order_fast(): Assertion `c[1] == false_lit' failed.
Aborted (core dumped)
msoos commented 7 years ago

Wow, that's pretty bad :) Last time that got triggered, it was due to gcc bug. What gcc version are you using? Can you try triggering it again? Can you give me the input that triggered it along with the exact GIT version or "officially versioned" version (e.g. 5.0.1) you have? I will track it down for sure. That's a really serious assert. Thanks in advance!

cipherboy commented 7 years ago

The commit hash (6115500c11877ddb740d1475986b733542c077df) on that link was to the exact version I compiled from. I don't have the old compiled binary still, but I could recompile it again. cmake .; make -j4 was how I built it (no additional flags to gcc beyond what you include). It is currently rerunning with a new binary from the latest commit (f5044d5b24c5a25eec23a8f7f50ad909297f2ed5). The assert took one day and 9 hours days to trigger last time -- I expect it to have crashed by tomorrow if the assert can still be triggered from master. 

$ gcc --version
gcc (GCC) 6.3.1 20161221 (Red Hat 6.3.1-1)
Copyright (C) 2016 Free Software Foundation, Inc.
This is free software; see the source for copying conditions.  There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
$ uname -a
Linux cipherboy-recon7 4.9.10-200.fc25.x86_64 #1 SMP Wed Feb 15 23:28:59 UTC 2017 x86_64 x86_64 x86_64 GNU/Linux
$ cat /proc/cpuinfo | grep 'model name'
model name  : AMD A10-5700 APU with Radeon(tm) HD Graphics

The SAT that triggered it is fitted to these two collisions and is trying to find a third that is similar in structure to those. It was built with the bc2cnf tool from bcsat. Using a SAT fitted to an instance of a MD4 Wang's differential collision runs quickly (seconds) and is satisfiable, producing another collision that has the exact same path as the first. Adding further collisions to the SAT creates a looser fit which also produces collisions. That is the intuition behind exploring this approach with MD5 and Stevens's differential.

Here are the files:

https://github.com/cipherboy/sat/tree/master/cms-issue-392

problem.cnf is the model I was running, problem.out was the output up to the crash, and problem.out.2 is the current progress of the run of a new build from master.

Thanks!

msoos commented 7 years ago

Wow, thanks for the info! So I can just re-build it from that commit and run it with no parameters on problem.out.2 and it should crash? That sounds pretty awesome, should make it really easy to reproduce! Also, much more importantly please submit those problems to the SAT Competition Here is the 2016 one: http://baldur.iti.kit.edu/sat-competition-2016/index.php?cat=benchmarks and here are the organisers' email: organizers@satcompetition.org it's the 2016, but they'll know what to do with them.

They would really help in making the competition more fair by having more diverse CNFs. They would also help you by making sure that SAT solver creators are tuning their solver to your cases. Note that the timeout is ~5000s so you probably need to re-generate them to be easier. A bunch of different instances with different harndesses would be nice, e.g. 20 ultra-hard (expected 10k secs), 20 medium-hard (expected 5k secs) 20 easier (expected 2k secs) and 20 easy (expected 500 sec) would be nice. I know this sounds like a lot of work, and it is. But you can also put them up to some website, people could use them to benchmark their solvers, and it's nice to have a curated set of instances for others and maybe also for you to test different solvers on. Plus if you want to publish, it's good to have some hard evidence and letting others play with it, makes it more likely they'll cite your work :)

msoos commented 7 years ago

This may have been the issue. I suggest you run single-threaded (sometimes it's faster...) and run it with the option -DLARGEMEM=ON as per #389

I'm closing now as I think the fix for #389 has fixed it. Please test that fix if you have a machine that has enough memory :) Thanks again for the report, I think it helped me put the fix to #389 together. Cheers and good luck! If you can reproduce the issue with single-thread after the -DLARGEMEM=ON please create a new issue with the CNF, the exact GIT version, the exact parameters and then I'll reproduce it :)