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 →

STP and CryptoMiniSat in the competitions of 2015

Uncategorized

Both the SAT Race and the SMT competition of 2015 are now over. The results are in and it’s time to draw some conclusions. CryptoMiniSat won the SAT Race’s incremental solving track, and the SMT solver that uses (among other solvers) CryptoMiniSat, CVC4, won the SMT competiton. These two wins are not unrelated — CryptoMiniSat is used in an incremental way by the CVC4 team. What CryptoMiniSat and STP (the other project I work on) hasn’t done is win their respective main competitions. Let me reflect on these quickly.

The SMT competition

The SMT competition’s quantifier free boolean vector track (QF_BV) was won by Boolector.  Boolector is an amazing piece of engineering and so is the SAT solver it uses, lingeling. Second was CVC using CryptoMiniSat and third was STP. The reason for STP being third was because I managed to add a bug into STP and never fuzzed it. So now fuzzing is part of the continuous integration suite. Without this bug, STP would have come pretty close to Boolector, of which I’m proud of.

In general, STP needs to be greatly overhauled. It’s a legacy codebase with global variables, weird dependencies and long list of weirdnesses. It’s also performing amazingly well, so one needs to be careful how to approach it. I have been trying to cut it up and slice it any way I can so it makes more sense to read the code and work on it, but it’s still quite hard.

The SAT competition

The SAT competition had its share of surprises. One such surprise was that lingeling didn’t win any main prizes. I wonder why it wasn’t submitted to the incremental track, for example. Another surprise was the 1st and 2nd places of two solvers by the same author, Jingchao Chen, who unfortunately I have never met or conversed with. I was also a bit disappointed that CryptoMiniSat didn’t make it too high on the list. There have been a number of issues I tried to fix, but apparently  that wasn’t enough. I will be interested in the sources of the winning solvers, see if I can learn something from them.

It’s really hard to create winning SAT solvers that behave well in all circumstances because it takes massive amount of time to code them up and properly test them. Especially the latter is really complicated and writing good test harnesses takes concentrated effort. My test scripts are easily over a thousand lines of code, mostly python. The continuous integration and build systems (both necessary for timely releases) are another thousand, and my AWS scripts for performance testing is almost a thousand as well. That’s more code than some early, well-performing SAT solvers had.
Continue reading STP and CryptoMiniSat in the competitions of 2015 →

Setting up encrypted mail in Chrome and Gmail

Docs/Faqs,

The use of Gmail is now ubiquitous. Unfortunately, it’s easy to read email in transit and some national governments abuse their power to read email in transit. I have always been using PGP to encrypt email, and today I thought I’d put down how to communicate with me, or with your friends, using signed and encrypted mail. I think the biggest reason email encryption is not being used is because it’s hard to set up. So, here is a simple, step-by-step tutorial that is easy to follow.

Installing and creating a key

  1. Install Mailvelope . Click “add to chrome”, pop-up appears, click “add”
  2. little padlock icon appears on the top right of your Chrome
  3. Click little padlock icon, click “Options”
  4. At the bottom, click “Generate key”
  5. Fill in Name (you can put fictitious name, it’s good!), Email (the email you want to use, e.g. Jon.Doe@gmail.com), put in a password that you will remember. This password is never sent anywhere. It’s used so that when you want to read email that is encrypted to you, the encryption keys can be accessed.
  6. Click submit, wait for the generation to finish.
  7. Setup is done!

Continue reading Setting up encrypted mail in Chrome and Gmail →

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.