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). |

- Overview
- Objectives
- Prerequisites
- Description
- Syllabus
- Afterword
- Additional Resources
- Acknowledgements

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.

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.

- Gain an understanding of the syntax and semantics of propositional logic, as well as general logic terminology, including "model", "(un)satisfiability", "entailment", "equivalence", "soundness", and "completeness".
- Learn the process of knowledge base conversion to Conjunctive Normal Form (CNF).
- Solve word problems with proof by contradiction (a.k.a. reductio ad absurdum) using resolution theorem proving.
- Represent knowledge so as to complete a program implementation that performs expert reasoning for the game of Clue.
- Compare deductive learning, inductive learning, and knowledge acquisition.

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.

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

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:

- Python: clue-python.pdf, SATSolver.py, clueReasoner.py
- LISP: clue-lisp.pdf, SAT-solver.lisp, clue-reasoner.lisp

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.

- Boolean Satisfiability Problem and Clue(do) articles on Wikipedia
- Boolean Satisfiability
- SATLive! - up-to-date links for the SATisfiability problem
- The International SAT Competitions web page
- zChaff
- SAT4J
- MiniSAT

- Clue(do)

Todd Neller, David Musicant