Speaker
Prof.
Ilkka Niemelä
(TKK)
Description
Tools for solving the propositional satisfiability (SAT)
problem have advanced dramatically during the last ten years
and are now standardly used in industrial applications such
as hardware design verification and automatic test pattern
generation. SAT solvers are also becoming widely used
search engines in areas with challenging computation
problems such as automated planning, bioinformatics, and
cryptanalysis. We discuss how a SAT solver can be used as
an efficient back-end search engine in such applications.
Then we review algorithmic techniques in state-of-the art
solvers and novelties behind recent substantial improvements
in performance for real world examples. We consider in more
detail the role of branching heuristics for the performance
of a SAT solver and the problem of generating
computationally hard SAT instances for state-of-the-art solvers.
