Boolean Satisfiability & Optimization Algorithms & Applications

Monday morning, 16th August, 2010, Room 6.1.36 

The development of efficient Boolean Satisfiability (SAT) solvers is a success story in computer science. Although SAT is NP-complete, current SAT solvers can handle problem instances with hundreds of thousands of variables and millions of clauses. This success has been further underlined by the many practical applications of SAT, which include software and hardware verification, termination analysis of programs and haplotype inference, among many others. The success of SAT has also led to its use in optimization problems, including Boolean optimization and Maximum Satisfiability (MaxSAT), and to its extension to more expressive logics, including Pseudo-Boolean (PB) constraints, Quantified Boolean Formulas (QBF), and Satisfiability Modulo Theories (SMT). This tutorial provides an overview of SAT, and covers the most widely used SAT algorithms, well-known extensions of SAT, standard modelling solutions, and representative applications.

Short bio

Joao Marques-Silva is SFI Stokes Professor at University College Dublin, Ireland, and has held academic positions at the University of Southampton, UK, and at IST, Portugal. He holds a PhD degree from the University of Michigan, USA, and the Habilitation, MSc and BSc degrees from IST, Portugal. Joao Marques-Silva is co-recipient of the CAV 2009 Award, for fundamental contributions to the development of high-performance Boolean satisfiability solvers. His research interests include decision and optimization procedures, with applications in Artificial Intelligence, Bioinformatics, Formal Methods and Design Automation.