MaxHS a hybrid approach to solving Maxsat
COM1 Level 2
SR1, COM1-02-06
This is a distinguished talk as part of the NUS Computer Science Research Week 2019 (http://researchweek.comp.nus.edu.sg).
Abstract:
The talk starts with a brief introduction to CDCL Sat solvers. In this tutorial we discuss the core algorithm used in modern Conflict Driven Clause Learning satisfiability solvers. The main topics will be: watch literals for detecting unit clauses, 1-UIP clause learning, bounded variable elimination preprocessing, and assumption based Sat solving.
Maxsat is the optimization version of satisfiability, in which one wants to find a truth assignment of minimum cost. Weighted Maxsat is in the complexity class FP to the NP, and as such it can be solved by a polynomial number of calls to a Satisfiability oracle. Most algorithms for solving Maxsat use this idea. MaxHS on the other hand uses the idea of incrementally constructing a hitting set problem and using an Integer Programming solver to find a minimal cost hitting set. This provides a lower bound on the cost of a optimal solution. A Sat solver on the other hand generates upper bounds or augments the hitting set problem thus increasing the lower bound. This hybrid approach has proved to be quite effective, and MaxHS is currently the best performing Maxsat solver on weighted problems and one of the best on unweighted problems. In this talk we will explain the algorithmic ideas underpinning MaxHS and review its performance.
Biodata:
Fahiem Bacchus is a Professor of Computer Science at the University of Toronto. His research fits broadly in the area of Knowledge Representation and Reasoning, a sub-field of Artificial Intelligence. He has made a number of key contributions during his career, including the development of first-order logics for representing different forms of probabilistic knowledge, and automated planning algorithms that can exploit domain specific control knowledge expressed in Linear Temporal Logic (LTL). For the past 15 years his work has concentrated on automated reasoning algorithms for solving various forms of the satisfiability problem: finding a model (SAT), counting the number of models (#SAT), solving quantified Boolean formulas (QBF), and finding optimal models (MaxSat). His group has been successful in building award winning solvers for all of these problems. He has served as Program Chair of several major AI conferences, including UAI, ICAPS and SAT; is a member of the IJCAI board of trustees, having served as Conference Chair of IJCAI-17; is currently Chair of the SAT Association which organizes the annual SAT conference; and has won a number of distinguished and influential paper awards. Fahiem is also a Fellow of the Association for the Advancement of AI (AAAI) since 2006.