Tinisat

Tinisat is a simple clause learning SAT solver. The version that participated in the 2007 SAT Competition, Tinisat 0.22, was written in 550 lines of C++ not counting comments and blank lines. Coupled with the SatELite preprocessor, Tinisat 0.22 won a Bronze Medal in the UNSAT industrial division of the competition.

Click here to download the source code of Tinisat 0.22.

Click here for detailed results of the experiments described in A Case for Simple SAT Solvers, Jinbo Huang, Proceedings of the 13th International Conference on Principles and Practice of Constraint Programming (CP-07).

Click here for detailed results of a superset of the experiments described in The Effect of Restarts on the Efficiency of Clause Learning, Jinbo Huang, Proceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI-07), along with executables of Tinisat 0.1 used for the experiments.

Back to my home page