Tag: BCP
-
On variable renumbering
Variable renumbering in SAT solvers keeps a mapping between the external variable numbers that is visible to the users and the internal variable numbers that is visible the to the system. The trivial mapping that most SAT solvers use is the one-to-one mapping where there is no difference between outer and internal variables. A smart […]
-
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 […]
-
On benchmark randomization
As many of you have heard, the SAT Competition for this year has been announced. You can send in your benchmarks between the 12th and the 22nd of April, so get started. I have a bunch of benchmarks I have already submitted about 2 years ago, still waiting for any reply from those organizers — […]
-
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 […]
-
Understanding Implication Graphs
Implication graphs are a core functionality of modern conflict-driven SAT solvers. In this blog post I give some examples of how these graphs look and how they can be used in the 1-UIP conflict generation scheme.