Tag: binary clauses
-
CryptoMinisat 3.1 released
CryptoMinisat 3.1 has been released. The short changelog is: $ 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 […]
-
Failed literal probing and UIP
I have just realised that CryptoMiniSat, having won a number of medals, does one of the most basic things, failed literal probing, all wrong. Let me tell you why it’s all wrong. In essence, failed literal probing is trivial. We enqueue a fact, such as a, and then propagate it. If this fails, i.e. if […]
-
Caching
“Representation is the essence of programming” Frederic P. Brooks Jr., “The Mythical Man-month” Looking through the literature on SAT solvers, it is rare to find any algorithm that uses a form of time-memory trade-off. In fact, it is rare to find any algorithm that uses too much memory. This also shows up in practice, as […]
-
Transitive OTF self-subsuming resolution
The title may be a bit long, but its essence is very simple: we try to shorten learnt clauses. The basic idea was described in this post: there is a clause we just derived, e.g. d V -e V f V g (1) where d,e,f,g are binary variables, – is binary negation, and V is […]
-
Propagating faster
Propagation (BCP) in SAT is the single most expensive operation. The algorithm essentially does the following: 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 […]