Tag: branching
-
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 […]
-
The variable speed of SAT solving
Vegard Nossum asked me about the varying time it took for CryptoMiniSat to solve a certain instance that was satisfiable. This inspired me to write an overly long reply, which I think might interest others. So, why does the solving time vary for a specific instance if we permutate the clauses? Intuitively, just by permutating […]
-
Dependent Literals
I have lately been trying to work on branching heuristics. The idea is relatively simple. If we have a cache of what propagates what, we can try to branch on literals that propagate a lot of other literals. The algorithm boils down to the following: For each literal L, we select a literal DL that […]