Lately, I have become an LLVM nut. LLVM is amazing, it can do a lot, and, weirdly enough, a system developed from it is probably one of the biggest users of SAT solvers. I’m talking about KLEE, the symbolic virtual execution machine. It takes a source, compiles it with LLVM, then translates the LLVM IR into SMT, runs STP on it, which in turn runs CryptoMiniSat, and voila… the user gets back a free bug report. Or 1’200 bug reports.

### Emscripten

Another great use of LLVM is emscripten, which takes the LLVM IR (again) and turns it into javascript. This of course means we can now run SAT solvers in the browser. This is *so* much fun. Here you can play with it, this is MiniSat “core”, from the golden old days of 2009. Just type in any CNF in DIMACS format and enjoy :) You can now solve the most basic NP-complete problem, right from your browser!

### MiniSat in javascript

### Epiloge

Yes, it’s actually running in your browser. The default CNF describes the HiTag2 cipher, with 10 output bits and 2 help bits given. The instance was generated using the Grain of Salt system. Note that the web page hangs until MiniSat finishes. Try typing in your own CNFs, play as much as you like. If you are patient, it can solve many problems, including reversing modern ciphers, finding SHA-1 collisions (PDF), verifying hardware and software… you just have to be patient enough.

Probably unbeknownst to you, you are using products of SAT solvers for your daily life: CPUs are verified using SAT solver-based techniques, airplane software is formally verified using SAT solvers, FPGA and CPU layouts are optimized using them, and if you are lucky, your car’s safety-critical systems are also verified using formal techniques, which basically means SAT solvers. Actually, even train schedules and public transport schedules are created using SAT solvers — I know for a fact that many trains in Europe are scheduled using these techniques. All these can be done using the very simple problem description, the CNF, you see above — and many of these systems use MiniSat.

### How I did it and what could be improved

It’s relatively easy to compile any C or C++-based SAT solver to javascript using emscripten. Here is my github repo, with included HOWTO, for MiniSat. I would love to compile current lingeling, but its license doesn’t seem to allow emscripten to even think about compiling it. I’ll compile CryptoMiniSat later, it’s a bit hairy right now, I’m trying to refactor the code since it’s a mess. Until then, I hope you’ll enjoy playing with MiniSat!

### Acknowledgements

A big thanks to my colleagues who pushed me to became an LLVM nut. Also, big thanks to Niklas Eén and Niklas Sörensson for MinSat!

[paypal-donation]

Just for my understanding of the above CNF and problem behind:

You have given a link to Wikipedia. There is a link to a description of HiTag2 on this page (on top right side). It seems there is a key with 48 bits, an initialization vector of 32 bits and perhaps some output bits? How do they map to CNF variables? Which parts are fixed, which parts are calculated in above CNF? It seems that above CNF has more than one solution.

I have used the Grain of Salt tool that I developed to create the CNF. If you create the CNF with that tool, it will output the mapping of the input, output, and the key to the CNF file itself, as comments. Just download the tool, run it, and take a look at the CNF generated. In the above CNF, I stripped the comments, because it made it larger, eating bandwidth.

I hope the above helped,

Mate

This is cool! I’ve actually done the same thing myself: https://github.com/jgalenson/research.js. I’d like to translate even more projects to JavaScript; do you have any more ideas about what we can target?

Well… CryptoMiniSat? :D But in all seriousness, I would go for STP or another SMT solver. That would bring variability — currently, these are all SAT solvers.

Just my 2 cents,

Mate