slides

brief description

This tutorial overviews the uses of SAT solvers as oracles, when employed for solving a wide range of computational problems, and illustrates their use in several practical applications, including the recent uses in explaining non-interpretable machine learning models.

long description

Propositional satisfiability (SAT) is a success story of computer science. The power of the conflict-driven clause learning (CDCL) paradigm underlying most of the state-of-the-art SAT solvers made them an irreplaceable tool-of-choice suitable for efficient industrial problem solving. Indeed, a SAT solver can be seen as a witness producing NP-oracle, which can be applied to solving decision problems in NP but also beyond NP, e.g. in higher levels of the polynomial hierarchy, as well as function and enumeration problems.

The mission of the tutorial is to give a comprehensive overview of the modern SAT solving technology and how SAT solvers are exploited for constraint problem solving, as well as for solving extensions and generalizations of SAT, i.e. when dealing with optimization and enumeration problems. Additionally, the tutorial will focus on applying SAT solvers as oracles to a variety of strategic practical applications ranging from graph optimization problems, model-based diagnosis to cooperative path-finding as well as verification and explanation of machine learning models. The tutorial will bring together the details of problem encodings into SAT, maximum and minimum satisfiability (MaxSAT/MinSAT), minimal unsatisfiability (MUS computation), quantified Boolean formulas (QBF), but also efficient SAT-based algorithms targeting the aforementioned problems.

outline

  1. Basics of SAT solving, including brief overview of conflict driven clause learning SAT solvers.
  2. Modeling with propositional logic, including encodings of cardinality and pseudo-boolean constraints.
  3. Problem solving with SAT oracles, covering maximum satisfiability, minimal correction subsets, minimal unsatisfiable subsets, quantified boolean formulas, and enumeration problems.
  4. Recent applications: explainable AI, cooperative pathfinding, model-based diagnosis, graph optimization problems, etc.

audience and objectives

IJCAI participants interested in artificial intelligence, constraint programming, and its applications in machine learning. The use of SAT solvers as oracles has enabled impressive inroads in solving a wide range of computational problems. These include well-known function problems, e.g. computing explanations and relaxations of overconstrained formulas, but also solving optimization, quantification and enumeration problems, to name a few. Recent applications of computing with SAT oracles include computing interpretable machine learning models, but also finding explanations for non-interpretable machine learning models. A tutorial on this topic offers advanced training in a range of technologies that finds an ever growing range of practical applications. This tutorial introduces novices to a key topic in AI (SAT and constraint solving, and its applications), it motivates and explains how to use SAT solvers as backend solver(s) in different and emerging areas of AI, and it surveys and provides training in a common practice in AI.

length

The tutorial has a duration of 1/2 day (two 1:45h slots).

presenters

  • Joao Marques-Silva (ANITI, Univ. Toulouse, France)
    Extensive experience in the area of the tutorial. In the mid90s, I invented clause learning, as used in modern SAT solvers. Extensive list of publications in the topic over the last decade.
  • Alexey Ignatiev (Monash University, Australia)
    Applied the SAT technology to solving a variety of practical problems from a number of different domains. Developed a range of highly efficient state-of-the-art algorithms and tools for problem solving with the use of SAT oracles.
  • Antonio Morgado (SAT group, INESC-ID, University of Lisbon)
    Since my PhD worked in the area of Boolean Optimization using SAT solvers as the backend solver. Most active in the area of MaxSAT, with participation in the creation of new algorithms, currently in use within state-of-the-art MaxSAT solvers.