Page History

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

.

h1. [Joao Marques-Silva|http://www.csi.ucd.ie/staff/jpms/], 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.

{attachments

:patterns

=.*}