Niklas Sörensson

Applications of SAT solving
Ph. Licenciate Thesis, 2003
An extensible SAT solver
Niklas Eén and Niklas Sörensson
Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing, 2003
Temporal Induction by incremental SAT solving
Niklas Eén and Niklas Sörensson
Proceedings of the First International Workshop on Bounded Model Checking, 2003
New techniques that improve MACE-style finite model finding
Koen Claessen and Niklas Sörensson
CADE-19, Workshop W4, Model Computation -- Principles, Algorithms, Applications, 2003
Fair constraint merging tableaux in lazy functional programming style
Reiner Hähnle and Niklas Sörensson
Published in a shorter form in Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, 2003
Symbolic Model Checking based on Induction
Master's Thesis, 2000

MiniSat	A minimalistic SAT solver that I developed together with Niklas Eén, and is currently maintaining. It was the core element of SatELiteGTI, the winning entry to the industrial category of the 2005 edition of the SAT competition. In 2006, MiniSat 2 won the the SAT Race, a smaller scale version of the SAT competition.
Paradox	A finite model finder for first order logic developed together with Koen Claessen. It won the Model class of the SAT division in CASC-19 competition for first order tools.
Tip	An induction based model checker that I developed a prototype for in Haskell and C++. Niklas Eén later developed a full version in C++, keeping the core ideas from my prototypes.
LTab	A toy theorem prover for first order logic. It is an implementation of Constraint Merging Tableaux in the lazy functional programming language Haskell.