Summary Clue Deduction - The popular boardgame Clue (a.k.a. Cluedo) serves as a fun focus problem for this introduction to propositional knowledge representation and reasoning.
Topics Syntax and semantics of propositional logic, general logic terminology (e.g. "model", "(un)satisfiability", "entailment", "equivalence", "soundness", and "completeness"), conjunctive normal form, proof by contradiction (a.k.a. reductio ad absurdum) using resolution theorem proving.
Audience Introductory Artificial Intellegence students
Difficulty A subset of three exercises and the main project can be completed within 2 weeks.  The main project can be completed in ~150 lines of Java code.
Strengths Clue Deduction presents a fun application of knowledge representation to complete a program implementation that performs expert reasoning for the game of Clue.  Also, student acquire understanding of fundamental concepts of logical reasoning without the additional complexity of first-order reasoning.
Weaknesses The basic project version requires knowledge of Java or LISP, and the installation of zchaff or another black-box SAT solver.  Many students prefer the advanced project involving the implementation of a SAT solver. 
Dependencies Students must be competent with creation of integer lists, be able to read and comprehend detailed specifications and documentation, and understand the rules of Clue enough to grasp the knowledge communicated in the game.
Variants Advanced projects include (1) the addition of pseudo-Boolean constraints, (2) implementation of a DPLL-style SAT solver, and (3) implementation of a stochastic local search SAT solver (e.g. WalkSAT). 

Clue Deduction: an introduction to satisfiability reasoning

Index:

Overview

The popular boardgame Clue (a.k.a. Cluedo) serves as a fun focus problem for this introduction to propositional knowledge representation and reasoning.  After covering fundamentals of propositional logic, students first solve basic logic problems with and without the aid of a satisfiability solver (e.g. zChaff).  Students then represent the basic knowledge of Clue in order to solve a Clue mystery.  Several possible advanced projects are sketched if students wish to pursue the topic in more depth.  

Objectives

The object of this project is to give the student a deep, experiential understanding of propositional knowledge representation and reasoning through explanation, worked examples, and implementation exercises.

Prerequisites

The student should understand the syntax of Java, Python, or LISP.  Students who program in C++ should be able to follow most of the Java examples.

Along with the project, the student should cover the recommended background reading below.

In support of the exercises and project, one should download and install zChaff, a complete, DPLL-type SAT solver.  If the use of a different SAT solver is desired, one will need to modify SATSolver.java accordingly.

For a more detailed introduction to the logical concepts, we recommend the parallel reading of a good AI textbook section on propositional logic.  For example, one might assign Chapter 7 ("Logical Agents") of:

Stuart Russell and Peter Norvig. Artificial Intelligence: a modern approach, 3rd ed. Prentice Hall, Upper Saddle River, NJ, USA, 2010.

Students are also encouraged to play the game of Clue in order to gain a solid understanding of the game and the knowledge one acquires during play.  One can speed gameplay by dispensing with board movement and allowing each player in turn to make an unrestricted suggestion and/or accusation.

Description

The project is described in the file clue.pdf.  You will need the free Adobe Acrobat Reader to view this file.Get Adobe Reader logo

Example Java code described in the project is available here (see below for Python and LISP):

This code was generated from the same source file that generated clue.pdf using the literate programming tool noweb

We recommend having students do a few of the included logic exercises of Section 7 in order to gain experience with the SATSolver class before beginning work on the ClueReasoner.

Students seeking more extended challenges will also find brief descriptions of related advanced projects including basic SAT solver challenges and extensions for cardinality constraints.

Daniel Le Berre, Lecturer at the faculté Jean Perrin, Université d'Artois, has generously provided a modified SATSolver for using  SAT4J, a library of efficient SAT solvers targeted for first users of SAT "black boxes" in Java.

David Musicant, Associate Professor of Computer Science at Carleton College, has generously provided a LISP port and a Python port of the above project description and source files:

Syllabus

Here is a sample syllabus used in CS 371 - Introduction to AI at Gettysburg College:

First class: Thursday 10/14/04
Preparatory reading: Russell & Norvig Sections 7.1-7.4 (through "A Simple Knowledge Base"), clue.pdf sections 1-2.
Propositional Logic, Syntax, Semantics.
Homework due next class: Represent the knowledge base for one exercise of clue.pdf section 7.

Second class: Tuesday 10/19/04
Truth assignments, models, (un)satisfiability, validity, entailment, equivalence.
Homework due next class: Represent the knowledge base for two more exercises of clue.pdf section 7.

Third class: Thursday 10/21/04
Preparatory reading: Russell & Norvig Section 7.5, clue.pdf sections 3-6.
Conjunctive normal form, resolution theorem proving, proof by contradiction (reductio ad absurdum), SAT solvers
Homework due next class: Resolution proofs and/or satisfying truth assignments for solving the logic problems of the previous homework, use of SATSolver class to check the solutions to these problems.

Fourth class: Tuesday 10/26/04
Preparatory reading: Remainder of clue.pdf.
The Game of Clue, propositional facts in the game, construction of a Clue reasoner.
Homework due next class: Complete implementation of ClueReasoner class, as described in clue.pdf section 8.

The following material is optional to the project:

Fifth class: Thursday 10/28/04
Preparatory reading: Russell & Norvig Section 7.6 ("local search algorithms").
Stochastic local search for boolean satisfiability, WalkSAT, Novelty, Novelty+, in-class simple implementation of WalkSAT.

Afterword

 In his book Machine Learning, Tom Mitchell writes “A computer is said to learn from experience E with respect to some class of tasks T and performance measure P, if its performance at tasks in T, as measured by P, improves with experience E.”  The three “experiences” of deductive learning, inductive learning, and knowledge acquisition can add knowledge to a knowledge base, thus potentially improving (or even making possible) the average expected time performance of the task of answering queries to the knowledge base.  This project and the corresponding reading focus on knowledge acquisition and deductive learning.

Additional Resources

Acknowledgements

 This work was supported by NSF DUE CCLI-A&I Award Number 0409497, and is part of the Machine Learning Laboratory Experiences for Introducing Undergraduates to Artificial Intelligence project.

Todd Neller, David Musicant