MaxSAT for Optimization Problems

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, University College Dublin, Dublin, Ireland

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.