Combinatorial Problem Solving with SAT: The Art of Encoding Prof. Mateu Villaret, Universitat de Girona.

This is the second, CS-focused talk of our visiting Senior Global Fellow, Prof. Mateu Villaret, Universitat de Girona.

SAT, the NP-complete problem par excellence, has become a Swiss Army knife for tackling combinatorial problems. The idea is simple: encode a problem as a SAT formula and ask the solver for an assignment whose solution corresponds to a solution of the original problem. This approach has a long history of success. But what lies beneath modern SAT solvers? And, perhaps more importantly, how can we design efficient encodings that allow them to solve complex combinatorial problems effectively?