Parallel Propositional Satisfiability Solving

The Faculty of Informatics is pleased to announce a seminar given by Antti Hyvarinen

DATE: Wednesday, March 21st 2012
PLACE: USI Università della Svizzera italiana, room A24, Red building (Via G. Buffi 13)
TIME: 14.30

ABSTRACT:
Successful parallel SAT solvers have so far been based on portfolios, where several solvers are competing in solving the same instance simultaneously and co-operating by sharing lemmas.  At the same time the efficiency of the solvers based on search space partitioning has been modest.  In this talk I will give one possible explanation why this might be the case, based on a proof showing that the expected time required to solve an unsatisfiable formula with a search space partitioning solver can always be higher than the expected run time of a corresponding sequential solver. I will then discuss three approaches which are based on search space partitioning but are by design more competitive than plain partitioning.  In particular one of the approaches is guaranteed, under the assumptions used in the proof, to always provide speed-up with increased resources.  I will then provide experimental support that an approach based on search space partitioning performs significantly better than a portfolio based approach on solving instances from a recent SAT solver competition.

BIO:
D.Sc. (Tech) Antti Hyvarinen graduated with distinction in December 2011 from Aalto University, Finland.  He started working in Prof Ilkka Niemela's group in 2004 and in 2006 he graduated as a Master of Science with the best possible grade for the thesis.  With the exception of a research intern position he held in summer 2011 in Dr Youssef Hamadi's group at Microsoft Research Cambridge, he has been continuosly working
for Prof Niemela.  His several publications in respected international journals and conferences form the basis of his dissertation, titled "Grid Based Propositional Satisfiability Solving" and examined by Prof Toby Walsh.  In February 2012 he received the award for best doctoral dissertations from Aalto University school of Science.  His current research interests include constraint based search and optimization, and
in particular their parallelization and connections to machine learning and formal verification.

HOST: Prof. Natasha Sharygina