I’ve been reading through the source code of the 2016 SAT Competition Main Track winner, MapleCOMSPS_DRUP, and I found that it has an important piece of code, regulating its behaviour that depends on timing:
static bool switch_mode = false;
static void SIGALRM_switch(int signum) { switch_mode = true; }
lbool Solver::solve_()
{
signal(SIGALRM, SIGALRM_switch);
alarm(2500);
CryptoMiniSat 5.0.0, after winning the incremental track at SAT Competition 2016 and getting 3rd place at the parallel track, has been released. The new solver contains a number of important additions. The most important are that the solver can now be used as a preprocessor and Gauss-Jordan Elimination is back.
Continue reading CryptoMiniSat 5.0.0 released
I have been trying to debug why some MiniSat-based solvers perform better at unit propagation than CryptoMiniSat. It took me exactly 3 full days to find out and I’d like to share this tidbit of information with everyone, as I think it might be of interest and I hardly believe many understand it.
The mystery of the faster unit propagation was that I tried my best to make my solver behave exactly as MiniSat to debug the issue, but even though it was behaving almost identically, it was still slower. It made no sense and I had to dig deeper. You have to understand that both solvers use their own memory managers. In fact, CryptoMiniSat had a memory manager before MiniSat. Memory managers are used so that the clauses are put close to one another so there is a chance that they are in the same memory page, or even better, close enough for them not to waste memory in the cache. This means that a contiguous memory space is reserved where the clauses are placed.
Lately, I have been working quite hard on writing module tests for CryptoMinisat using GoogleTest. I’d like to share what I’ve learnt and what surprised me most about this exercise.
First of all, let me show how a typical test looks like:
TEST_F(intree, fail_1)
{
s->add_clause_outer(str_to_cl(" 1, 2"));
s->add_clause_outer(str_to_cl("-2, 3"));
s->add_clause_outer(str_to_cl("-2, -3"));
inp->intree_probe();
check_zero_assigned_lits_contains(s, "-2");
}
Here we are checking that intree probing finds that the set of three binary clauses cause a failure and it enqueues “-2” at top level. If one looks at it, it’s a fairly trivial test. It turns out that most are in fact, fairly trivial if the system is set up well. This test’s setup is the following test fixture:
struct intree : public ::testing::Test {
intree()
{
must_inter = false;
s = new Solver(NULL, &must_inter);
s->new_vars(30);
inp = s->intree;
}
~intree()
{
delete s;
}
Solver* s;
InTree* inp;
bool must_inter;
};
The GitHub repository for CryptoMiniSat just hit 8000 commits. To celebrate this rather weird and crazy fact, let me put together a bit of a history.
CryptoMiniSat began as a way of trying to prove that a probabilistic cryptographic scheme was not possible to break using SAT solvers. This was the year 2009, and I was working in Grenoble at INRIA. It was a fun time and I was working really hard to prove what I wanted to prove, to the point that I created a probabilistic SAT solver where one could add probability weights to clauses. The propagations and conflict engine would only work if the conflict or propagation was supported by multiple clauses. Thus began a long range of my unpublished work in SAT. This SAT solver, curiously, still works and solves problems quite well. It’s a lot of fun, actually — just add some random clause into the database that bans the only correct solution and the solver will find the correct solution. A bit of a hackery, but hey, it works. Also, it’s so much faster than doing that solving with the “right” systems, it’s not even worth comparing.
Continue reading CryptoMiniSat: 8000 commits later