Using Knot Mosaics to Introduce Undergraduates to SAT
Hannah Miller · 2022
Knot mosaics are combinatorial representations of mathematical knots. Boolean satisfiability (SAT) is an important NP-complete problem, and SAT solvers are practical software implementations to solve SAT problems. SAT solvers are rarely used in undergraduate classes, and the learning curve for SAT is steep. For our contribution, we developed a lecture and a homework assignment for undergraduate students to work with SAT formulas, to draw knot mosaics, and to run SAT solvers for counting knot mosaics. The assignment has been developed over three semesters. The assignment includes a skeleton Python encoding with over 750 lines of Python code and function documentation. We surveyed the students about their experiences with and perceptions of the assignment as well as their comments for improving the assignment. On the survey, students overwhelmingly agreed that they learned about SAT and knots, and the students earned high grades on the assignment, showing that their perception of learning was true. Our future work includes clarifying one of the assignment problems where students struggled.