Ampithéatre CTL
25 June 2009 - 14h00
On Some Problems in Satisfiability Solving (Phd Defense)
by Scott Cotton from Verimag
Abstract: An increasing array of applications from verification to non-linear optimization make use of satisfiability and SMT solvers. At the same time, satisfiability and SMT solvers have made enormous progress recently. But satisfiability and SMT solvers are tasked with hard and intractable problems and their performance can be hard to predict. Thus satisfiability and SMT solving is an active area of research. This seminar presents mechanisms related to satisfiability and SMT solvers in four parts.
First, we give an introduction to some basic ideas in propositional satisfiability solving and DPLL(T).
Second, we introduce the concept of label-composed solvers, which may be seen as a variant of DPLL(T). In this part, we further examine the composition of a difference logic (DL) solver with a propositional solver. We instantiate an efficient DL solver based on an incremental shortests paths algorithm. We present experimental results showing that label-composed solvers can be efficient and that, together with the efficient DL solver, the results improve on previous work.
Third, we revisit propositional satisfiability in more depth, and present a restart strategy which heuristically guides the solver to termination. The strategy randomly deviates from a best prefix of the search tree on every choice point immediately following a conflict.
Fourth and finally, we present a generic direct method of solving conjunctive problems based on depth first search over variable valuations. The method makes use of a local consistency condition we call unate consistency. We examine the similarities and differences between the method and DPLL based solving, with an emphasis on the case of infinite domain variables. We conclude with preliminary experiments based on a Java prototype.
Jury composé de
Yassine Lakhnech Président (Proposé)
Nikolaj Bjørner Rapporteur
Sharad Malik Rapporteur
Kenneth McMillan Rapporteur
Armin Biere Examinateur
Eugene Asarin Examinateur
Andreas Podelski Examinateur
Oded Maler Directeur de Thèse
