Siert Wieringa

Postal Address:	P.O.Box 5400, FI-02015 TKK, FINLAND
Street Address:	Konemiehentie 2, Otaniemi, Espoo
Office:	Room T-B252
Telephone:	+358-9-47025244
Email:	siert.wieringaaalto.fi
Research interests:	Boolean satisfiability (SAT), SAT-based model checking,
	Distributed (SAT) algorithms, Unsatisfiable core extraction

Publications

Marijn J.H. Heule, Oliver Kullmann, Siert Wieringa and Armin Biere, Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads, accepted for Haifa Verification Conference 2011 (HVC 2011).

Siert Wieringa, On Incremental Satisfiability and Bounded Model Checking, presented at First International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS11), 2011. (PDF)

Siert Wieringa, Matti Niemenmaa and Keijo Heljanko, Tarmo: A Framework for Parallelized Bounded Model Checking, In Lubos Brim and Jaco van de Pol, editors, Proceedings of the 8th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC09), volume 14 of Electronic Proceedings in Theoretical Computer Science (EPTCS), pages 62-76, 2009.

Hans van Maaren and Siert Wieringa, Finding guaranteed MUSes fast, In H. Kleine Büning and X. Zhao (Eds.): Proceedings of SAT2008, LNCS 4996, pp. 291-304, Springer, Heidelberg (2008).

Resources

DIFTS11 - Resources for the article On Incremental Satisfiability and Bounded Model Checking.

Tarmo - A parallel solver for incrementally encoded SAT instances.

iCNF - Is a file format for sequences of incrementally encoded SAT instances.

MiniUnsat - A tool for extracting minimal unsatisfiable subsets (MUS) from unsatisfiable CNF formulas.

Research reports

Master's thesis:	Finding unsatisfiable cores using a Brouwer's fixed point approximation algorithm
Research assignment:	MiniMarch: Embedding lookahead direction heuristics in a conflict driven solver
Course assignment:	The first steps to a hybrid SAT solver (joined work with Dimosthenis Mpekas and Michiel van Vlaardingen)