Computer Science Colloquium
Im Rahmen des Informatik-Kolloquiums, das von den Instituten des Fachbereichs Informatik, der Österreichischen Gesellschaft für Informatik (ÖGI), der Arbeitsgemeinschaft für Datenverarbeitung (ADV) sowie der Österreichischen Computergesellschaft (OCG) abgehalten wird, spricht
über das Thema:
Solving Max-SAT by Decoupling Optimization and Satisfaction
Zeit: 2014-10-30 16:00:00.0, 60 Minuten
Ort: S3 247 (Science Park 3)
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.
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.
Einladender: Assist.-Prof. Dr. Martina Seidl and Prof. Dr. Armin Biere