CryptoMinisat 3.1 has been released. The short changelog is:
|
1 2 |
$ git diff cryptoms-3.0 cryptoms-3.1 --shortstat 84 files changed, 3079 insertions(+), 2751 deletions(-) |
The changes made were threefold. First, memory usage has been greatly reduced. This is crucial, because memory usage was over 7GB on certain instances. Secondly, the implication cache wasn’t very well-used and an idea that came to my mind greatly improved performance on most problems.
I have lately been trying to get CryptoMiniSat to use implicit binary clauses. The idea is that since binary clauses are very trivial (just two literals), and they don’t really need to keep state (like clause activity), they don’t really need to be stored at a separate location. Instead, they can be stored directly in
Asymmetric branching is an algorithm that shortens CNF clauses in SAT Solvers. A clause, for instance v1 V v2 V v3 V v4 (where letters are binary variables and V represents binary OR) could possibly be shortened to v1 V v2 V v3. To find out if it can be, all we have to do
Propagation (BCP) in SAT is the single most expensive operation. The algorithm essentially does the following:
|
1 2 3 4 5 6 7 8 9 |
while (queue_head < trail.size()) { Literal p = trail[queue_head]; vector<Watch>& thiswatch = watches[p]; for (i = thiswatch.begin(); i!=thiswatch[p].end(); i++) { confl = prop_confl(i->clause); if (confl != NULL) return confl; } queue_head++; } |
where the function prop_confl() executes the propagation or returns a conflict, if necessary. The problem with the above function is that clauses come in all shapes and sizes. In CryptoMiniSat, there are two kinds of clauses, normal clauses
I have talked about optimisations before and I mentioned that there are a few left to describe. In this post I will talk about two of them. The first optimisation I would like to talk about concerns compilation flags. Somehow, everyone seems obsessed with them, like if they could somehow make a slow program fast.
