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.
Zhen Wu Computer Science Department, University of Pittsburgh, Amanda Buddemeyer Learning Research & Development Center and School of Computing and Information, University of Pittsburgh, Erin Walker University of Pittsburgh, Angela Stewart Computer Science Department, University of Pittsburgh
Xiaoxue Du MIT Media Lab, Robert Parks Massachusetts Institute of Technology, Selim Tezel Massachusetts Institute of Technology, Jeff Freilich Massachusetts Institute of Technology, Nicole Pang Massachusetts Institute of Technology, Hal Abelson Massachusetts Institute of Technology, Cynthia Breazeal Massachusetts Institute of Technology