Strimko by Resolution

An Intro-AI Project


Develop a Strimko solver by repeated and systematic application of the resolution inference procedure.


Knowledge representation (propositional logic), logical inference (resolution), backtracking search, Python programming


Undergraduate students in an introductory AI class.


Being meant for undergraduates, this is a fairly straighforward project. The basic project (without extra credits) should not take more than a week between assignment and due date.


This project allows students to get an integrated view of logical inference and backtracking search in a small and manageable problem (Strimko). It also encourages goal-oriented research into an advanced topic. By avoiding the use of a black-box SAT solver in the base project, the students get a "look under the hood" of logical reasoning.


Some Strimko puzzles cannot be represented due to limitations in the GUI. However, the solver (when completed) will work for all Strimko puzzles. The demo version does not include backtracking search.


Students should be able to translate formal pseudocode as well as less formal instruction into program, and also follow pseudocode logic to be able to answer questions about it. Knowledge of Python required.


An in-class demo variant could be developed that lists the disjunctions on the GUI, and highlights reduction by resolution, guesses made for backtracking, etc., to demonstrate inferences incrementally.

Project Description
Base code (for students)
Demo version (an extended version could be used in class; not available to students)