This is a JavaScript version of MiniSat. It was compiled with Emscripten.

To use it, enter a CNF formula in the DIMACS format in the top box. You can find an informal definition of this format here and some large benchmarks here. Once you press "Solve", the result will be printed in the second textbox.

The sample problem below was generated by ToughSAT and represents a formula whose satisfying assignment encodes two non-trivial factors of a number.

Instructions on how to build MiniSat with Emscripten are available on GitHub.

We have also built the Boolector SMT solver with Emscripten. The demo and source are available here.