Category: Development
-
CryptoMiniSat 5.8.0 Released
After many months of work, CryptoMiniSat 5.8.0 has been released. In this post I’ll go through the most important changes, and how they helped the solver to be faster and win a few awards, among them 1st place at the SAT incremental track, 3rd place SAT Main track, and 2nd&3d place in the SMT BitVector […]
-
ApproxMCv3, a modern approximate model counter
This blogpost and its underlying work has been brewing for many years, and I’m extremely happy to be able to share it with you now. Kuldeep Meel and myself have been working very hard on speeding up approximate model counting for SAT and I think we have made real progress. The research paper, accepted at […]
-
CryptoMiniSat and Parallel SAT Solving
Since CryptoMiniSat has been getting quite a number of awards with parallel SAT solving, it’s about time I talk about how it does that.There is a ton of literature on parallel SAT solving, and I unfortunately I have barely had time to read any of them. The only research within the parallel SAT solving area […]
-
CryptoMiniSat 5.6.3 Released
The latest CryptoMiniSat, version 5.6.3 has been released. This release marks the 12’000th commit to this solver that has weathered more than I originally intended it to weather. It’s been an interesting ride, and I have a lot to thank Kuldeep and NSCC‘s ASPIRE-1 cluster for this release. I have burned over 200k CPU hours […]
-
Testing CryptoMiniSat using GoogleTest
Lately, I have been working quite hard on writing module tests for CryptoMinisat using GoogleTest. I’d like to share what I’ve learnt and what surprised me most about this exercise. An example First of all, let me show how a typical test looks like: TEST_F(intree, fail_1) { s->add_clause_outer(str_to_cl(” 1, 2″)); s->add_clause_outer(str_to_cl(“-2, 3”)); s->add_clause_outer(str_to_cl(“-2, -3”)); inp->intree_probe(); check_zero_assigned_lits_contains(s, “-2”); […]