SAT-based Combinatorial Optimisation

Session date: 20 November 2023

Session host: Andre Schidler

Summary:

SAT solvers determine whether a given propositional formula is satisfiable. Today’s highly engineered SAT solvers can determine the satisfiability of huge formulas with millions of constraints and thousands of variables. Further, stating other combinatorial problems in terms of propositional satisfiability allows the use of this great SAT-solving performance for a large range of combinatorial problems.

In this talk, I will discuss how to address combinatorial optimisation problems, using SAT and related solving paradigms (MaxSAT and SMT). This approach has been successfully used for a large number of combinatorial problems. Nonetheless, the approach often struggles to scale to large instances, as the translation into SAT can severely increase the size and complexity of the instance. I will present several methods to overcome scalability issues:

• Refining the translation into a SAT instance;
• Lazily creating the constraints;
• Incorporating SAT solving into large neighborhood search.

The talk does not assume prior knowledge about propositional logic or SAT solving and is targeted at an audience familiar with basic combinatorial optimisation.