...
The success of SAT technology has motivated work on using SAT as the
underlying engine for solving other related computational problems.
One example is linear optimization over Boolean domains, including
Maximum Satisfiability (MaxSAT). Concrete practical applications
include fault localization in C code, debugging of hardware designs,
and haplotype inference. This talk overviews different ways of
representing optimization problems and their equivalence. It also
summarizes representative practical applications. In addition, the
talk overviews different approaches for solving optimization problems,
emphasizing SAT-based solutions.
...
Joao Marques-Silva holds a PhD degree in Electrical Engineering and
Computer Science from the University of Michigan, Ann Arbor, in 1995,
and the Habiliation degree in Computer Science from the Technical
University of Lisbon, Portugal, in 2004. Currently, he is Stokes
Professor of Computer Science and Informatics at University College
Dublin (UCD), Ireland. He is also Professor of Computer Science at
Instituto Superior Tecnico (IST), Portugal. His research interests
include algorithms for constraint solving and optimization, and
applications in formal methods, artificial intelligence, and
bioinformatics. He received the 2009 CAV award for fundamental
contributions to the development of high-performance Boolean
satisfiability solvers.
Attachments | ||
---|---|---|
|