Solving MAXSAT by finding UNSAT Cores
Professor Fahiem Bacchus (University of Toronto)
ARTIFICIAL INTELLIGENCE SEMINARDATE: 2011-11-01
TIME: 12:00:00 - 13:00:00
LOCATION: NICTA - 7 London Circuit
CONTACT: JavaScript must be enabled to display this email address.
ABSTRACT:
(Joint work with Jessica Davies). MAXSAT is an optimization version of SAT in which we are given a set of clauses each having a weight. The task is to find an truth assignment that satisfies a maximum weight of clauses. Hard constraints can be represented with clauses of infinite weight. Many practical problems can be represented as MAXSAT instances, including problems in scheduling, optimal planning, and MAP inference. This talk presents a new method for solving MAXSAT. The method involves solving a series of ordinary SAT problems and from their solution constructing a minimal weight hitting set problem. The hitting set problem can then be solved by a MIPS (Mixed Integer Program) Solver like CPLEX. The solution to the hitting set problems is always a lower bound on the MAXSAT solution, and it converges to the exact solution as we augment the hitting set problem by solving more SAT problems. The approach performs competitively in practice, and better than existing solvers on some benchmark families. The approach also achieves a clean separation between feasibility and optimization. Hence, solvers best suited for each task can be employed.
BIO:
http://www.cs.toronto.edu/~fbacchus/
