Machine Learning Laboratory Experiences for Introducing Undergraduates to Artificial Intelligence
NSF DUE CCLI-A&I Award Number 0409497

Clue Deduction:
an introduction to satisfiability reasoning

 

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

 

 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.
 

 BACKGROUND
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. A version that is compatible with SATSolver.java usage above is also available.

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.