STP and CryptoMiniSat in the competitions of 2015

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.

In general, 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.

Most competing SAT solvers (with the exception of lingeling) don’t have such elaborate test and release systems in place. Although maintaining such systems seems like a burden, in the long run, they pay off well. For example, the incremental track is particularly hard to compete in without proper tests and hence CryptoMiniSat had a good chance there — and I don’t see why lingeling didn’t compete, given that is must have extremely elaborate test and release systems, too.


It has been a good year for CryptoMiniSat and STP. Some of their strengths have been highlighted more than others, and progress has been made on all fronts. They might both be released as part of standard packages in Debian, Fedora and other distros. All this sounds great. I have put lots of effort into both, and some of that effort is paying off, which is good to hear.

On the CryptoMiniSat side, in the future, I need to concentrate more on experimentation so it can be as agile as some of the newly winning solvers. On the STP side, I need to put more effort into fuzzing, testing, and refactoring.

Setting up encrypted mail in Chrome and Gmail

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., 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!

Obtaining keys of others

You need to get the keys of others so you can send encrypted email to them. Here is how.

  1. Look for your friend’s email here and copy the gibberish text that appears, e.g. mine
  2. Click the little padlock icon on the top right of your Chrome
  3. Click “setup” on list of things
  4. Paste the gibberish text in the textbox
  5. Click Import
  6. It should say “success … Mate Soos [or your friend’s fictitious name]… imported”
  7. Done!

Sending encrypted email

  1. Go to
  2. Click compose. Fill in subject and recipient (these will not be encrypted)
  3. You will see a little notepad icon in the email text body. Click it.
  4. 1st Pop-up appears. Write your mail here! Note that these drafts are not saved, so you need to be careful
  5. Click “Encrypt”
  6. 2nd Pop-up comes up. Your own email address will be automatically added to “Encrypt for”
  7. You need to select at the top drop-down menu the destination email address (which you must have imported as per setup). Once you selected the destination,  click “Add” (don’t forget to click “Add’, it’s easy to forget)
  8. You now have 2 email addresses in the bottom list. One is yourself, one is the recipient
  9. Click OK. 2nd pop-up disappears. Your email is now encrypted in this popup.
  10. Click “Transfer”, 1st Pop-up disappears
  11. You are now in the compose window again. Don’t change anything, just click “Send”
  12. Done!

Reading encrypted email

  1. go to
  2. click on email to read
  3. email window opens, email is yellow with a lock on top. Click!
  4. enter the password you used above
  5. decrypted email appears

Backing up your private keys

  1. In chrome, click the top right padlock
  2. Click Options
  3. Click Export
  4. Popup appears. Click Download
  5. The file “all_keys.asc” is now saved to disk
  6. Keep this file backed up. Done!

Sending your public key to others

You need to send your public key to your recipient so they can send you encrypted mail (and verify your signature). Also, it’s a good idea to put them on a public site, like your blog or on

  1. In chrome, click the top right padlock
  2. Click Options
  3. Pop-up appears. On the bottom, click the email address that says “primary”
  4. 2nd pop-up appears. On the top menu, click “Export”
  5. Here, make sure you have “Public” selected (it’s the default)
  6. Click download.
  7. Attach that file to an email to me or anyone you want to send you encypted mail
  8. Upload the contents of the file here

Try no to confuse the private and the public keys. Send the public key to everyone. Never send the private key to anyone, ever.

Closing thoughts

The security professionals would point out that trusting the public key is not discussed above. It’s true, it’s not discussed, and it’s not easy to know what to trust. However, the vast majority of the time, the resurrecting duckling principle will work well — it’s when you trust the first thing you see, just like the duckling trusting that the first thing it sees is its mother. It’s imperfect, but the web of trust is very unintuitive and therefore may bring less benefits than most think. A technology that is good but is unintuitive often harms more than most people would admit.

Trusting the first key will be good for most people. In case you are in danger of being seriously harmed for the information you are about to send, though, please try to make sure the key you got was legitimate, by, e.g. phoning up your recipient and confirming the key fingerprint (displayed on the setup page).

Note that in case your computer is compromised, the above will not help. They will be able to read your data and read your password as you type it. So, try not to visit dodgy sites, allow Windows and Mac to encrypt your drive, choose a strong login password,  use a password manager for all sites, and keep your Mac and Windows updated.

Machine Learning and 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.

It is clear that there could have been a number of ways to detect that a problem is cryptographic without using such an elaborate scheme. However, that would have demanded a mixture of more features to decide. The scheme only used the average and the standard deviation.

Lingeling and clause cleaning strategy selection

The decision made by lingeling about whether to use glues or activities to clean learnt clauses is somewhat similar to my approach above. It calculates the average and the standard deviation of the learnt clauses’ glues and then makes a decision. Looking at the code, the option actavgmax/stdmin/stdmax gives the cutoffs and the function lglneedacts calculates the values and decides. This has been in lingeling since 2011 (lingeling-587f).

Probably a much better decision could be made if more data was taken into account (e.g. activities) but as a human, it’s simply hard to make a decision based on more than 2-3 pieces of data.

Enter machine learning

It is clear that the above schemes were basically trying to extract some feature from the SAT solver and then decide what features (glues/activities) to use to clear the learnt clause database. It is also clear that both have been extremely effective, it’s by no luck that they have been inside successful SAT solvers.

The question is, can we do better? I think yes. First of all, we don’t need to cut the problem into two steps. Instead, we can integrate the features extracted from the solver (variable activities, clause glue distribution, etc) and the features from the clause (glue, activities, etc.) and make a decision whether to keep the clause or not. This means we would make keep/throwaway decisions on individual clauses based on potentially hundreds of extracted features — and that requires machine learning. But it would allow much more than what we have now. By giving a large number of features to the machine learning algorithm, it could extract interesting high-level features from them. In particular, deep learning could possibly have come up with glues(!) if the decision levels of the variables (along with the current decision level) were given to it. I think there must be more and better higher-level features than just glues.

It’s highly inefficient to ask humans to come up with high-level features and decision trees for clause keep/throwaway when there are readily-available systems that can extract high-level features and make immensely complex (and effective!) decision trees in very reasonable amount of time on modern machines.


I think we have been wasting research and development time on coming up with high-level features and decision trees for keeping or throwing away learnt clauses. It’s time we looked at a discipline that has been exploding in computer science and stopped mocking SATZilla — effectively, all modern SAT solvers employ a hand-crafted poor man’s version of some of SATZilla.

Post Scriptum

This file in the SAT Race 2015 version of CryptoMiniSat will be super-controversial. It on-the-fly reconfigures CryptoMiniSat after ~160K of conflicts and three runs of pre- and in-processing based on over 50 extracted features. It’s crappy. And effective. I did it in one week, over the CAV conference. It simulates the decision by CryptoMiniSat and lingeling about activities/glues, and more. Thanks Ofer Strichman!

Towards CryptoMiniSat 5.0

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. “./ –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.


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

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.<


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.