Solving Combinatorial Problems with SAT
MSc Thesis Proposal by: Aaron Barnoff
Date: April 30, 2026
Time: 11:00am
Location: 122 Essex Hall
Abstract:
Many combinatorial search problems are difficult because the number of possibilities grows too quickly for naive exhaustive search. Boolean satisfiability (SAT) is the problem of deciding whether truth values can be assigned to variables so that a logical formula becomes true. Many combinatorial search problems can be translated into propositional logic and then solved using a SAT solver. SAT solvers are off-the-shelf, general-purpose tools for a broad class of search problems, and can sometimes outperform hand-crafted algorithms designed for a particular problem. In this thesis, we investigate how SAT can be used as a general framework for combinatorial search by encoding a problem as a propositional formula and using problem-specific structure to guide the search more effectively. The thesis focuses on two case studies. 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. For this problem, we develop SAT encodings and related techniques that improve the best known lower bound for walks avoiding 7 collinear points. The second is the construction of mutually orthogonal Latin squares of a special form. For this problem, we develop a hybrid method that combines SAT solving with a linear Diophantine system solver, leading to substantially faster solution times than SAT alone.
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