Many important problems from combinatorial problems to industrial domains are computationally hard and often exponential in the worst case. Yet, in practice, many instances of these problems can be solved efficiently by modern constraint solving tools.

In this talk, we introduce Boolean Satisfiability (SAT) and its optimization counterpart, Maximum Satisfiability (MaxSAT), as powerful frameworks for solving decision and optimization problems. We discuss the evolution of SAT and MaxSAT solvers and present some of the key ideas behind their success, such as Conflict-Driven Clause Learning and core-guided optimization. We also briefly survey applications of SAT and MaxSAT across a wide range of domains, including verification, planning, and mathematics. These successes suggest that SAT and MaxSAT solvers have become practical tools for tackling complex real-world problems, even when those problems are hard in theory.

 

References

Fahiem Bacchus, Matti Järvisalo, Ruben Martins: Maximum Satisfiability. Handbook of Satisfiability 2021: 929-991.

João Marques-Silva, Inês Lynce, Sharad Malik: Conflict-Driven Clause Learning SAT Solvers. Handbook of Satisfiability 2021: 133-182.

Ruben Martins, Saurabh Joshi, Vasco Manquinho, Inês Lynce: Incremental Cardinality Constraints for MaxSAT. CP 2014: 531-548.

Ruben Martins, Vasco Manquinho, Inês Lynce: Open-WBO: A Modular MaxSAT Solver. SAT 2014: 438-445.

Bernardo Subercaseaux, John Mackey, Marijn J. H. Heule, Ruben Martins: Automated Mathematical Discovery and Verification: Minimizing Pentagons in the Plane. CICM 2024: 21-41.