Abstract
Optimization problems whose corresponding decision problems can be encoded into SAT can be solved by solving a sequence of SAT problems. For example, a maximum clique can be found by using SAT to solve a sequence of decisions "does a clique of size k exist" for different values of k. In practice, however, often this is not an effective approach to optimization. In this talk I will discuss some alternative approaches for using SAT for optimization, approaches that have arisen from research into building better MaxSat solvers. One approach is to extract cores from the SAT solver when the decision problem is UNSAT, these cores can then be used to generate an alternate, and usually more effective, sequence of SAT queries to obtain optimal solutions. Another approach is to exploit a hybrid of SAT and an alternate optimization solver, where the SAT solver is used to dynamically generate a problem for the alternate solver to solve, and the alternate solver is used to generate candidate solutions for the SAT solver to verify. Both approaches yield interesting new applications and challenges for SAT.