Computer Science Colloquium
Jessica Davies
IST Austria
Solving Max-SAT by Decoupling Optimization and Satisfaction
Thu 30.10.2014, 16:00, 60 minutesS3 247 (Science Park 3)
Abstract
Max-SAT is an optimization version of SAT that can represent a wide variety of important optimization problems. We introduce a new approach for solving Max-SAT, that exploits both a SAT solver and a Mixed Integer Programming (MIP) solver in a hybrid approach. Each solver generates information used by the other solver in a series of iterations that terminates when an optimal solution is found. Empirical results indicate that a bottleneck in this process is the time required by the MIP solver, arising from the large number of times it is invoked. We present two enhancements of the basic algorithm, that address this bottleneck. First, we enrich the constraints given to the MIP solver. Second, we postpone the calls to the MIP solver by substituting non-optimal solutions for the optimal ones computed by the MIP solver, whenever possible. We present empirical results that show that the resulting solver, MaxHS, is the most robust existing solver for Max-SAT.Bio
Jessica Davies is a postdoc in Tom Henzinger´s group at IST Austria. She received a PhD in Computer Science from the University of Toronto in 2013. Her thesis introduced a new approach for solving the Maximum Satisfiability problem, implemented in the MaxHS solver, which is the most robust existing solver for Max-SAT. Her work on an open problem in computational social choice, in collaboration with NICTA Sydney, resulted in an Outstanding Paper award at AAAI 2011. She is the co-author of 10 conference papers and 3 journal papers. Her research interests include model counting, optimization, diagnosis, and software verification and synthesis.Invited by Assist.-Prof. Dr. Martina Seidl and Prof. Dr. Armin Biere
The Computer Science Colloquium is organized by the Department of Coputer Science at JKU, the Österreichische Gesellschaft für Informatik (ÖGI) and the Österreichische Computergesellschaft (OCG).