minisat 1.14 vs. minisat 2.20

[petr.ti...@gmail.com]

Hello, is anyone able to explain me what is the main difference between minisat 1.14 and minisat 2.20 ? I have several examples where the former minisat is much more efficient than the later one.
Thank you in advance for your advise. Petr Tichavsky

[Norbert Manthey]

Hi Petr,

It's complicated. The gap you point at has changed heuristics, restart scheme, way to select the polarity for the next decision literal, and limits wrt simplification size (i did not compare the code, so the latter might actually be wrong). There is likely more.

Could you explain your benchmark (input problem, formula size, used encodings)? With that info, a more educated guess on why one version might be better could be done.

Taking this one step further: there is a competitive SAT event coming up. Do you mind submitting a set of formulas there? That would allow you to see how other solvers perform on your problem, and the community gets another fresh problem set to look at, thanks! Deadline would be 2019-04-22.

This is the page that describes the submission process: http://sat-race-2019.ciirc.cvut.cz/index.php?cat=benchmarks

Best,

Norbert

[Mate Soos]

Hi,

So based on this I had a look and minisat 1.14 solves, out of SAT Competition 2014-18 (1334 unique instances) with 5000s timeout, 464 instances. Newest CryptoMiniSat solves >890. The only ones that minisat-1.14 solves but CryptoMiniSat does not is exactly 15, list at the bottom of the mail. This testifies to how much SAT solving has improved. But getting back to the ones that only minisat-1.14 solved, it's weird: every single one is a "SATISFIABLE" instance. Just like yours. Although satisfiable instances don't interest me much, due to this incredible randomness about them, I decided to do the experiment and CryptoMiniSat, that couldn't solve your instance in over an hour, could solve it in just 347 seconds if I set the polarity of the variables to be forced to FALSE, not caching polarities. Note that the solution has 2746 negatively and 214 positively set variables.

I first heard this from Armin Beire and I thought it to be funny: if one were to create a CNF that represents breaking AES (say, find key given a plaintext-ciphertext combo), then nobody should be able to solve that. However, if I set the polarities such that the solution is exactly the all-false, then most solvers will trivially find a solution. Now if I make the solution polarity random (as it should be in a naturally occurring cryptographic problem), then finding a solution is basically impossible using SAT solvers (or any other techniques for the moment). In other words, finding a satisfying solution to a problem can have absolutely no relation to its complexity, as the starting point can seriously influence whether a solution is found. Hence me being slightly/mostly uninterested in satisfiable problems.

My conclusion is therefore that your problem happens to be encoded such that a solution is relatively close to be found to the all-false polarity and polarity caching moves away from this too far for the solution to be found. Polarity caching is not present in minisat-1.14. It would be interesting to find all solutions, ban them all, and then submit it to the SAT competition as an UNSATISFIABLE problem. In case current systems could prove UNSAT within the 5000s timeframe, I have a feeling that minisat-1.14 wouldn't have a chance -- as it didn't have a chance at solving any UNSAT problems that CryptoMiniSat (or most likely any other modern SAT solver) could solve.

Hence, I don't think this problem should be sent into the SAT Competition. It's encoded in a way that makes it easy to solve in case the solver happens to start with an all-false polarity and sticks to it. Theoretically, the all-false solution is a 1-in-a-2^N chance, where N is almost always over 1'000, often over 20'000 . Maybe we should be building systems that are a bit more generic than that :)

Just my 2 cents,

Mate

PS: Only minisat could solve:

20180321_140833987_p_cnf_320_1120.cnf.gz
aes_32_2_keyfind_1.cnf.gz
bx-d-4-7-6.cnf.gz
bx-d-4-7-8.cnf.gz
by-alt-5-7.cnf.gz
cz-d-4-7-5.cnf.gz
full-ax-xa.rules.7-7.cnf.gz
less-cy-caa.rules.4-9.cnf.gz
modgen-n200-m90860q08c40-6967.cnf.gz
Nb54T6.cnf.gz
Nb8T60.cnf.gz
Nb8T61.cnf.gz
snw_16_9_CCSpre.cnf.gz
snw_16_9_Encpre.cnf.gz
snw_16_9_pre.cnf.gz

--

---
You received this message because you are subscribed to the Google Groups "MiniSat" group.
To unsubscribe from this group and stop receiving emails from it, send an email to minisat+u...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Armin Biere]

Note, Nb54T6.cnf.gz is unsatisfiable, last year's sat competition winner can solve that one and an additional two satisfiable of these .... (in 5000 seconds).

To unsubscribe from this group and stop receiving emails from it, send an email to min...@googlegroups.com.

[Mate Soos]

Hi All,

Ooops, sorry for that, and thanks for double-checking! It turns out that the memory use of CryptoMiniSat was off on this problem, and briefly peaked above 5GiB (~4.7GB), terminating the instance. With a slightly higher limit, it can be solved as well under the same time limit.

Thanks again for pointing out the error, it helped me dig deeper,

Mate

To unsubscribe from this group and stop receiving emails from it, send an email to minisat+u...@googlegroups.com.