Algorithms for Maximum Satisfiability with Applications to AI

AAAI-16 Tutorial
Saturday, February 13, 2:00 PM - 6:00 PM

Introduction

Many important AI problems involve an optimization component. Maximum satisfiability (MaxSAT) is an optimization version of Boolean satisfiability (SAT) that can be applied to a variety of optimization problems that arise in AI. From a simple propositional encoding one can automatically achieve a working optimizer for your application by using a MaxSAT solver. This can be much less time consuming than building a custom solution to one's optimization problem. In fact, a well engineered MaxSAT solver can often be more efficient than a custom solution. MaxSAT also offers an alternative to integer programming (IP) in many AI applications. In this tutorial we will introduce MaxSAT, give an overview of the different techniques have been developed for solving MaxSAT (with a focus on which techniques tend to be more effective on which types of problems), and explain via case studies how MaxSAT has been used to solve problems from different areas of AI. After this tutorial you should be better equipped to assess whether or not MaxSAT would be useful in your work and better able to use modern MaxSAT solvers in your work. The tutorial assumes no background knowledge beyond what a new graduate student in Computer Science would possess.

Tutorial Material

Slides from the tutorial (preliminary version)

Syllabus

  1. Motivation and Basic Concepts
    • Exact Optimization
    • Benefits of MaxSAT
    • MaxSAT: Basic Definitions
    • MaxSAT Solvers: Input Format, Evaluations, and Availability
  2. Algorithms for MaxSAT Solving
    • Branch and Bound
    • MaxSAT by Integer Programming
    • SAT-Based MaxSAT Solving
      • Iterative Search
      • Core-based Approaches
    • SAT-IP Hybrid Algorithms for MaxSAT
    • Iterative Use of SAT Solvers for MaxSAT
  3. Modelling and Applications
    • Representing High-Level Soft Constraints in MaxSAT
    • MaxSAT-based Cost-optimal Correlation Clustering
    • Heuristics for Planning using MaxSAT
  4. Summary and Further Reading

Presenter Biographies

Fahiem Bacchus (webpage) is a professor of computer science at the University of Toronto. His research fits broadly in the area of knowledge representation and reasoning, a subfield of artificial intelligence. He has made a number of key contributions during his career, including the development of 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 the program chair of several major AI conferences, including Uncertainty in AI (UAI), the International Conference on Automated Planning and Scheduling (ICAPS) and the International Conference on Theory and Applications of Satisfiability Testing (SAT); and will serve as conference chair of IJCAI-17. Fahiem is also a Fellow of the Association for the Advancement of AI (AAAI).

Matti Järvisalo (webpage) is academy research fellow and adjunct professor at the Department of Computer Science, University of Helsinki, Finland, where he leads the Constraint Reasoning and Optimization group. His research record lists over 60 refereed publications with a main focus on theoretical and algorithmic aspects of Boolean satisfiability (SAT) and optimization and applications of SAT-based techniques in solving various hard search and optimization problems in AI. He has served as program chair for the International Conference on Theory and Applications of Satisfiability Testing (SAT).