| |
|
|
Electronic Systems Design Seminar
|
 |
|
SLIDES [SAT]
In recent years SAT has also been the subject of intensive research.
With direct significance to EDA, new backtrack search algorithms have
been proposed, that include new strategies, new techniques and new
implementations. Broadly, improvements in SAT solvers have been
characterized by a few significant paradigm shifts. First, GRASP and
rel-sat very successfully proposed using clause recording and
non-chronological backtracking in SAT solvers. More recently, search
restart strategies have been shown to be extremely effective for
solving real-world problem instances. Finally, the most recent
paradigm shift was observed first in SATO and more recently and more
drastically in Chaff, that proposed several significant new ideas on
how to efficiently implement backtrack search SAT algorithms.
This talk proposes to investigate the paradigm shift personified by
SATO and Chaff. How effective are the data structures proposed by
these SAT solvers? Are these data structures the best option for
existing SAT solvers? Are these data structures the most adequate for
the expected next generation SAT solvers? Is it possible to do better?
This talk describes a first study to answer these questions.
Joao Marques-Silva obtained the BSc and MSc degrees at the Technical University of Lisbon, Portugal, in 1988 and 1991, respectively, and the PhD degree at the University of Michigan, Ann Arbor, in 1995. Since 1995, he has been an Assistant Professor at the Computer Science Department of the Technical University of Lisbon, Portugal, and a member of the Cadence European Laboratories. His research research interests include Algorithms for Discrete Optimization Problems, namely Satisfiability, Unate/Binate Covering and Integer Programming, and Applications of Discrete Optimization in EDA.