Category Archives: SAT

CryptoMiniSat: 8000 commits later

Personal, SAT, , ,

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.

The Beginnings

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 →

Machine Learning and SAT

Development, Research, SAT, ,

I have lately been digging myself into a deep hole with machine learning. While doing that it occurred to me that the SAT community has essentially been trying to imitate some of ML in a somewhat poor way. Let me explain.

CryptoMiniSat and clause cleaning strategy selection

When CryptoMiniSat won the SAT Race of 2010, it was in large part because I realized that glucose at the time was essentially unable to solve cryptographic problems. I devised a system where I could detect which problems were cryptographic. It checked the activity stability of variables and if they were more stable than a threshold, it was decided that the problem was cryptographic. Cryptographic problems were then solved using a geometric restart strategy with clause activities for learnt database cleaning. Without this hack, it would have been impossible to win the competition.
Continue reading Machine Learning and SAT →

Towards CryptoMiniSat 5.0

SAT, Tools, ,

I have worked a lot on CryptoMiniSat 5.0 in the past months so I thought I’d write a little bit about what I spent my time on.

Amazon AWS

I have put lots of effort into use Amazon AWS service to run CMS. This is necessary in order to compete at the SAT competition where my competitors have access to massive resources, some to clusters having over 20k CPU cores. Competing against that with a 4-core machine like I did last year will simply not cut it.

The system I built has a client-server infrastructure where the server is a very-very small machine (t1.micro) that hands out jobs to very-very beefy client machine(s) (c4.8xlarge with 18 real cores). I need this architecture because the client I use is a so-called spot instance so Amazon can shut it down any time. The server makes sure to keep in mind what has been solved and what needs to be solved next to complete the job. At the finish of the job, both the server and the client shut down. I simply need to issue, e.g. “./launch_server.py –git 82c4e5adce –s3folder newrun –cnfdir satcomp091113 -t 5000” and it will launch the full SAT competition 09+11+13 instances with a 5000s timeout using a specific GIT revision of CryptoMiniSat. When it finishes (in about 4-5 hours), it (should) send me a mail with the command line to use to download all the data from Amazon S3. It’s neat, fast, and literally just one command line to use.

As for how much I have used it, I have spent over $100 on running costs on AWS in the past 2 months. A run like the one above costs about $2. Not super-cheap, but not the end of the world, either.

Testing and continuous integration

I have TravisCI, Coverity, and Coverall integration. These provide continious integration testing, static analysis, and code coverage analysis, respectively. I find TravisCI to be immensely valuable, I would have trouble not having it for a new project. Coverity is also pretty useful, it has actually found some pretty stupid mistakes I have made. Finally, coveralls has a terrible interface but I like the idea of having test code coverage analysis and it encourages me to put more effort into that. For example, it highlights pretty well the areas that I typically break when coding without realizing it. TravisCI usually warns me if there is something bad except when there is no (or too little) coverage. I am also looking into Docker, which would allow for continuous delivery.

Checking against SWDiA5BY

I have integrated the main idea of SWDiA5BY A26 code into CryptoMiniSat. Further, I am in the process of integrating one of thepatches available on the author’s website. I find these patches to be really interesting and using SWDiA5BY A26 as a check against my own system has allowed me to get rid of a lot of bugs. So, I am greatly indebted to the authors of MiniSat, Glucose and SWDiA5BY.

Conclusions

In the past months I have put a lot of effort into cleaning up, fixing, and taking control of CryptoMiniSat in general. There have been over 240 issues filed at github against CryptoMiniSat over the years, and only 7 are currently open. This is a testament to how open and dynamic the solver development is. In case you are interested in helping to develop or have new ideas, don’t hesitate to contact me. Further, if you have any commercial interest in the solver, don’t hesitate to contact me.

The past half year of SAT and SMT

Development, SAT

It’s been a while I have blogged. Lots of things happened on the way, I met people, changed countries, jobs, etc. In the meanwhile, I have been trying to bite the bullet of what has become of CryptoMiniSat: last year, it didn’t perform too well in the SAT competition. In the past half year I have tried to fix the underlying issues. Let me try to explain what and how exactly.

Validation and cleanup

First, in the past years I ‘innovated’ a lot in directions that were simply not validated. For example, I have systems to cleanly exit the solver after N seconds have passed, but the checks were done by calling a Linux kernel function, which is actually not so cheap. It turned out that calling it took 3-5% of the time, and it was essentially doing nothing. Similar code was all over the place. I was (and still am, in certain builds) collecting massive amounts of solving data. It turns out, collecting them means not having enough registers left to do the real thing so the ASM code was horrific and so was performance. The list could go on. In the end, I had to weed out the majority of the stuff that was added as an experiment without proper validation.

Other solvers

Second, I started looking at other solvers. In particular, the swdia5by solver by Chanseok Oh. It’s a very-very weird solver and it performed exceedingly well. I’m sure it’s on the mind of many solver implementers, and for a good reason. As a personal note, I like the webpage of the author a lot. I think what s/he forgets is that MiniSat is not so well-used because it’s so well-performing. Glucose is better. It’s used because it’s relatively good and extremely well-written. However, the patches on the author’s website are anything but well-written.

The cloud

Finally, I worked a lot on making the system work on AWS, the cloud computing framework by Amazon. Since I don’t have access to clusters like my competitors do, I need to resort to AWS. It’s not _that_ expensive, a full SATComp’14 run sets me back about $5-6. I used spot instances and a somewhat simple, 1000-line python framework for farming out computation to client nodes.<

Conclusions

All in all, I’m happy to say, CryptoMiniSat is no longer as bad as it was last year. There are still some problems around and a lot of fine-tuning needed, but things are looking brighter. I have been thinking lately of trying to release some of the tools I developed for CryptoMiniSat for general use. For example, I have a pretty elaborate fuzz framework that could fuzz any solver using the new SAT library header system. Also, the AWS system could be of use to people. I’ll see.

Faster cleaning of the learnt clause database

Development, SAT,

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 stored in two places: as a list of pointers to the clauses and in a list of lists called the watchlist. Removing clauses from either list can be an O(n^2) operation if we e.g. remove every element from the list, one by one. In fact, an old version of the most popular SAT solver, MiniSat2, used to do exactly this:

sort(learnts, reduceDB_lt());
for (i = j = 0; i < learnts.size() / 2; i++){ if (learnts[i]->size() > 2 && !locked(*learnts[i]))
        removeClause(*learnts[i]);
    else
        learnts[j++] = learnts[i];
}
[...]

Here, removeClause() is called on each clause individually, where removeClause() eventually calls remove() twice, where remove() is a linear operation:

template
static inline void remove(V& ts, const T& t)
{
    int j = 0;
    for (; j < (int)ts.size() && ts[j] != t; j++);
    assert(j < (int)ts.size());
    for (; j < (int)ts.size()-1; j++) ts[j] = ts[j+1];
    ts.pop();
}

It is clear that if the number of learnt clauses removed is a significant percent of all clauses (which it is after some runtime), this is an O(n^2) operation.

My original solution

My original solution to this problem was the following. First, I did a sweep on the watchlist and detached all learnt clauses. This is an O(n) operation. Then, I ran the algorithm above, without the removeClause(). Finally, I attached the remaining learnt clauses: again an O(n) operation. This solution is significantly faster than the MiniSat one as its worst-case runtime is only O(n). The improvement is measurable — worst-case cleaning times dropped from seconds to tenths of seconds. However, it can be further improved.

The improved solution

The improvement that came to my mind just yesterday was the following. I can keep a one bit marker in each learnt clause that indicates whether the clause needs to be detached or not. Then, I can run the algorithm as above but replace removeClause() with markclause() and run through the watchlists once to remove (and free) the marked clauses. This works really well and it only necessitates one sweep of the watchlists, without any useless detach+reattach cycles.

The newer GitHub version of MiniSat also marks the clauses instead of detaching them immediately and then removes them in one sweep, later. Interestingly, it keeps a list of ‘dirty’ occurrence lists and only goes through the ones that need removal. I find that a bit strange for this specific purpose: usually almost all watchlists are affected. In other cases, though, keeping dirty lists in mind can be a good idea, e.g. if only few clauses are removed for some optimization step.