Solving Combinatorial Optimization Problems With Boolean Satisfiability Solvers

Abstract

Combinatorial Optimization problems are about making decisions that satisfy constraints and optimize objectives. An example is the hospital staff rostering problem, where we decide which staff members take which shifts. Rosters cannot violate policy constraints, but should minimize costs and maximize quality of care. We can specify the decisions, constraints and objectives in a so-called constraint model. A model is translated for and then solved by some solving algorithm. Boolean Satisfiability (SAT) solvers are extremely efficient, however, the translation of the model is uniquely challenging. This thesis improves the theoretical understanding and practical effectiveness of the translation process for SAT solvers.