Electronic Systems Design Seminar
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.