Tag: Optimisation
-
Faster cleaning of the learnt clause database
In SAT solvers, removing unneeded learnt clauses from the clause database sounds like a trivial task: we somehow determine which clauses are not needed and we call remove() on them. However, in case performance is an issue, it can get a bit more more complicated. The problem The issue at hand is that clauses are […]
-
On using less memory for binary clauses in lingeling’s watchlists
Armin Biere gave a lecture at the Pragmatics of SAT workshop (proceeedings here) in Vienna about all the things inside lingeling which won a lot of awards[PDF] this year. If you weren’t there, you missed an amazing presentation. In this blog post I’ll reflect on a particular part of the presentation dealing with a memory […]
-
Why it’s hard to eliminate variables
Let’s examine why it’s hard to eliminate variables. I remember the code I looked at in SatElite that did it: it was crazy clean code and looked like it was pretty easy to perform. In this post I’ll examine how that simple code became more than a 1’000 lines of code today. What needs to […]
-
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 […]
-
Implicit binary clauses
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 […]