Logic Puzzle Solvers in Python

A collection of classic logic-based AI puzzle solvers, built from scratch using propositional logic and a custom model-checking engine.
This project demonstrates how logical reasoning can be automated to solve puzzles such as Clue-style deduction, Knights and Knaves, and other inference challenges.

---

Files

.
├── logic.py         # Propositional logic system and model checker
├── mastermind.py    # Clue-inspired deduction puzzle
├── harrison.py      # Simple logical inference example
├── puzzle.py       # Knights and Knaves puzzles
├── requirements.txt # Dependencies
└── README.md        # Documentation

---

Descriptions

1. logic.py

Defines the propositional logic framework:

• Symbol → Represents logical statements
• And, Or, Not, Implication → Logical connectives
• model_check → Checks if a statement follows from a knowledge base

This file is the foundation for all the puzzles.

---

2. mastermind.py

A deduction puzzle inspired by Clue (the board game).

• Characters: Colonel Mustard, Prof. Plum, Ms. Scarlet
• Weapons: Knife, Wrench, Revolver
• Rooms: Library, Ballroom, Kitchen

The program builds a knowledge base of facts:

• Exactly one suspect, one weapon, and one room are correct
• Known false leads are eliminated
• Guesses and revealed cards are encoded as logical statements

The solver checks which possibilities are YES, NO, or MAYBE.

---

3. harry.py

A simple logic inference example:

• If it’s not raining, then Hagrid must be around
• Either Hagrid or Dumbledore is present (but not both)
• Explicitly assumes Hagrid is present

The program uses the knowledge base to check if hagrid is logically entailed.

---

4. puzzle.py

Implements Knights and Knaves puzzles:

• Each character is either a Knight (always tells the truth) or a Knave (always lies).
• Uses logical constraints to represent each puzzle.

Puzzles included:

• Puzzle 0 → A says “I am both a knight and a knave.”
• Puzzle 1 → A says “We are both knaves.”
• Puzzle 2 → A says “We are the same kind.”, B says “We are of different kinds.”
• Puzzle 3 → A, B, and C make a series of statements about each other.

The solver prints which assignments of Knight/Knave are consistent.

---

Installation

Clone the repository:

git clone https://github.com/your-username/logic-puzzles.git
cd logic-puzzles

Install dependencies:

pip install -r requirements.txt

---

Usage

Run any puzzle:

python mastermind.py
python harrison.py
python puzzle.py

---

Example Output

Running mastermind.py:

ColMustard: NO
ProfPlum: YES
MsScarlet: NO
knife: NO
wrench: MAYBE
revolver: NO
library: MAYBE
ballroom: NO
kitchen: NO

---

Running knight.py:

Since the puzzles aren’t yet fully implemented (the # TODO parts), the script prints:

Puzzle 0
    Not yet implemented.
Puzzle 1
    Not yet implemented.
Puzzle 2
    Not yet implemented.
Puzzle 3
    Not yet implemented.

Once you fill in the knowledge0, knowledge1, etc., it will instead list which symbols (like A is a Knight, B is a Knave, etc.) are entailed by the logic. For example, after implementation, it might look like:

Puzzle 0
    A is a Knave
Puzzle 1
    A is a Knave
    B is a Knight
Puzzle 2
    A is a Knight
    B is a Knave
Puzzle 3
    A is a Knight
    B is a Knave
    C is a Knight

---

Running harry.py:

This one is simpler. With your knowledge base:

knowledge_base = And(
    Implication(Not(rain), hagrid),
    Or(hagrid, dumbledore),
    Not(And(hagrid, dumbledore)),
    hagrid
)

You are checking:

print(model_check(knowledge_base, hagrid))

Output:

True

Because the knowledge base explicitly includes hagrid, so the model checker confirms it is logically entailed.

---

License

This project is licensed under the MIT License.

---