João Paulo Marques-Silva,

University of Southampton

Abstract:

The problem of Maximum Satisfiability (MaxSAT) and some of its
variants find an increasing number of practical applications in a wide
range of areas. Examples include optimization problems in digital
system design and verification, and in bioinformatics. However, most
practical instances of MaxSAT are too hard for existing branch and
bound algorithms. One recent alternative to branch and bound MaxSAT
algorithms is based on unsatisfiable subformula identification. This
talk provides an overview of recent algorithms for MaxSAT based on
unsatisfiable subformula identification.

 

Date: 2008-Mar-07     Time: 11:00:00     Room: 336


For more information: