Solving Combinatorial Problems with SAT
MSc Thesis Defense by: Aaron Barnoff
Date: July 31st, 2026
Time: 11:00am
Location: Virtual
Abstract:
Many combinatorial search problems are difficult because the number of possible objects grows too quickly for naive exhaustive search. Boolean satisfiability (SAT) provides a general framework for such problems: one encodes the desired objects as satisfying assignments of a propositional formula, and then uses a SAT solver to search for solutions or prove that none exist. This thesis studies SAT-based methods for two combinatorial search problems. The first is the Gerver–Ramsey collinearity problem for north–east lattice walks, where the goal is to determine the maximum length of a walk avoiding k collinear points. We develop SAT encodings for this problem using path constraints, non-collinearity constraints, reachability information, and parallelization. Using these methods, we enumerate all north–east lattice walks avoiding k collinear points for k ≤ 6 and construct a north–east walk with 327 steps avoiding k = 7 collinear points. The second problem concerns the construction of mutually orthogonal Latin squares. We develop a hybrid method that combines SAT solving with the Euler–Parker algorithm for finding orthogonal mates. In this approach, the SAT solver searches for Latin squares satisfying structural constraints, while an external exact-cover solver is used to test completed squares for orthogonal mates. This hybrid method substantially improves performance over a pure SAT approach on the Latin square instances considered.
Keywords: Satisfiability (SAT), Combinatorial Search, Orthogonal Latin Squares
Thesis Committee:
Internal Reader: Dr. Yung H. Tsin
External Reader: Dr. Adrian Zahariuc
Advisors: Dr. Curtis Bright, Dr. Ahmad Biniaz
Chair: Dr. Shaon Shuvo