Maximum Satisfiability: Beyond Decision Problems

Ruben Martins

In recent years, Boolean Satisfiability (SAT) solvers have been successfully used in many practical applications, including planning, hardware and software verification, and computational biology. However, not all real world problems lead to Boolean constraints which can actually be simultaneously satisfied. Although these problems cannot be fully resolved, many applications, such as software package upgrades, error localization in C code, and hardware debugging, can benefit from knowing the maximum number of satisfied constraints. Such problems are known as Maximum Satisfiability (MaxSAT) problems, the optimization counterpart to SAT as a decision problem. In this talk, we present algorithms for solving the MaxSAT problem which are particularly effective for solving real world problems. In particular, we will focus on a new technique based on partitioning that significantly improves the performance of MaxSAT algorithms. Using partitioning enables our solver to solve 50% more instances than without partitioning. As a result of the algorithmic advances, MaxSAT solvers are nowadays powerful tools that can be used in many applications domains. For example, we will show how MaxSAT can be used to solve hardware debugging problems. Moreover, we will also discuss how SMT solvers can be turned into MaxSMT solvers by using the presented MaxSAT algorithms.