Using smt solver and logic puzzles for teaching computational logics in discrete mathematics cla

Abstract

Computational logics is one of the core languages for undergraduate students to build the fundamental knowledge and understanding of the computer science principles. However, unlike other beginnerlevel programming language courses, most students learn computational logics only with deduction or paper-and-pencil problem solving without any programming experiences. This poster shows our case of providing a SMT-solver (e.g., Z3) and programming problems of writing logic puzzle solvers (e.g., Sudoku, Numbrix) as effective learning materials that beginnerlevel students can understand and practice computational logics as rigorous programming languages. These problems involve students modeling a problem as a satisfiability problem, finding and specifying constraints of a problem as predicate logic formulas, and calling a SMT solver from the programs, and other relevant problem-solving activities. We present a set of SMT-solver-based programming assignments (with different difficulty-levels) designed for beginner-level computer science course, instructions for students to equip basic skills for using Z3, useful set-up to challenge and support students at the same time.We also discuss our teaching experiences, open issues and future work.