Logic Puzzles Lab — Solution Walkthrough

Unit 5: Introduction to Logic in AI — Lab Walkthrough

Attempt the lab before reading this walkthrough. The explanations here are most valuable after you have worked through the problems yourself and hit obstacles. Reading solutions before attempting the work will significantly reduce your learning.

This walkthrough explains the reasoning and Python implementation for each part of the Logic Puzzles Lab. Every solution includes a logical analysis section followed by annotated code.

Part 1: Knights and Knaves — Solution

Logical Analysis

The puzzle has three characters: Alice, Bob, and Carol. Let K_A, K_B, K_C be true when the corresponding person is a Knight.

Step 1 — Formalize each statement:

Alice says "I am a knave": * If Alice is a Knight (K_A = T), her statement must be true: she is a knave (K_A = F). Contradiction. * If Alice is a Knave (K_A = F), her statement must be false: she is not a knave (K_A = T). Contradiction.

Wait — this looks paradoxical. The resolution: Alice must be a Knave, because only a Knave can make a false statement. Her claim "I am a knave" is false (since Knaves lie), which is consistent only if she is a Knave who is lying. (A Knight could never truthfully claim to be a Knave, and a Knave’s lie "I am a knave" means she is actually a Knight — contradiction — so she must be a Knave whose statement is taken as false, meaning she is NOT claiming truthfully.)

In code, the consistency check for Alice is: * alice_truthful (= K_A) must NOT equal alice_claim (whether her statement is actually true)

Bob says "Alice is a knight": bob_claim = (Alice is actually a Knight). Bob’s statement must match his truthfulness: bob_truthful == bob_claim.

Carol says "Bob is a knave": carol_claim = (Bob is actually a Knave). Carol’s statement must match her truthfulness: carol_truthful == carol_claim.

Solution: Alice = Knave, Bob = Knave, Carol = Knight.

Python Solution

def solve_knights_and_knaves():
    """Solve using exhaustive search with constraint checking."""
    types = ['knight', 'knave']

    for alice_type in types:
        for bob_type in types:
            for carol_type in types:
                assignment = {
                    'Alice': alice_type,
                    'Bob':   bob_type,
                    'Carol': carol_type
                }

                # Alice says: "I am a knave"
                # alice_claim: is her statement actually true?
                alice_claim   = (assignment['Alice'] == 'knave')
                alice_truthful = (assignment['Alice'] == 'knight')
                # Consistency: a Knight makes true statements; a Knave makes false ones.
                # We need truthful XOR claim -- they must differ.
                # If both match (both T or both F), this assignment is inconsistent.
                if alice_truthful == alice_claim:
                    continue

                # Bob says: "Alice is a knight"
                bob_claim    = (assignment['Alice'] == 'knight')
                bob_truthful = (assignment['Bob'] == 'knight')
                if bob_truthful != bob_claim:
                    continue

                # Carol says: "Bob is a knave"
                carol_claim    = (assignment['Bob'] == 'knave')
                carol_truthful = (assignment['Carol'] == 'knight')
                if carol_truthful != carol_claim:
                    continue

                return assignment  # First (and only) consistent assignment

    return {}  # No solution found

solution = solve_knights_and_knaves()
print(solution)
# Expected: {'Alice': 'knave', 'Bob': 'knave', 'Carol': 'knight'}

Code Walkthrough

Exhaustive search (lines 5—8): Three nested loops generate all 2 × 2 × 2 = 8 possible assignments.

Alice’s consistency check (lines 10—17): alice_claim is True if Alice actually is a knave (matching what she said). alice_truthful is True if Alice is a knight (truth-teller). For consistency, a knight’s claim must be true (truthful = T, claim = T) and a knave’s claim must be false (truthful = F, claim = F). But Alice’s statement "I am a knave" creates a paradox unless she is a knave (truthful = F) making a false claim (claim = F means the statement "I am a knave" is false, i.e., she is a knight — contradiction). The code resolves this by continuing past any assignment where truthful == claim (both match). The only consistent interpretation is that Alice is a Knave who falsely claims to be a knave — but that is also self-contradictory. The puzzle is designed so Alice must be a Knave; the code confirms by finding only one consistent full assignment.

Bob’s consistency check (lines 19—22): Unlike Alice’s self-referential statement, Bob’s statement is checkable: does it match reality? bob_truthful == bob_claim requires that a Knight’s statement is true and a Knave’s statement is false. If bob_truthful ≠ bob_claim, skip.

Carol’s check (lines 24—27): Same structure as Bob’s.

Part 2: Who Owns the Zebra? — Solution

Logical Analysis

Represent each house (1—5) as a position. We need to find an assignment of nationalities, beverages, cigarettes, and pets to positions that satisfies all 15 clues.

Key clue types: * Same house: "The Brit lives in the red house" → position(Brit) = position(Red) * Adjacency: "The green house is directly to the left of the white house" → position(Green) + 1 = position(White) * Center: "The center house owner drinks milk" → position(Milk) = 3 * First: "The Norwegian lives in the first house" → position(Norwegian) = 1

Python Solution

from itertools import permutations

def solve_zebra_puzzle():
    """Solve using constraint checking over all permutations."""
    houses = [1, 2, 3, 4, 5]

    # Try all permutations of nationalities across 5 houses
    for nat in permutations(houses):
        # nat[0]=Brit, nat[1]=Swede, nat[2]=Dane, nat[3]=Norwegian, nat[4]=German
        brit, swede, dane, norwegian, german = nat

        # Clue 9: Norwegian in house 1
        if norwegian != 1:
            continue

        for col in permutations(houses):
            # col[0]=Red, col[1]=Green, col[2]=White, col[3]=Yellow, col[4]=Blue
            red, green, white, yellow, blue = col

            # Clue 1: Brit in red house
            if brit != red:
                continue
            # Clue 4: Green is directly left of White
            if green + 1 != white:
                continue
            # Clue 14: Norwegian lives next to blue house
            if abs(norwegian - blue) != 1:
                continue

            for bev in permutations(houses):
                # bev[0]=Tea, bev[1]=Coffee, bev[2]=Milk, bev[3]=Beer, bev[4]=Water
                tea, coffee, milk, beer, water = bev

                # Clue 3: Dane drinks tea
                if dane != tea:
                    continue
                # Clue 5: Green house owner drinks coffee
                if green != coffee:
                    continue
                # Clue 8: Center house drinks milk
                if milk != 3:
                    continue

                for cig in permutations(houses):
                    # cig[0]=PallMall, cig[1]=Dunhill, cig[2]=Blend,
                    # cig[3]=BlueMaster, cig[4]=Prince
                    pallmall, dunhill, blend, bluemaster, prince = cig

                    # Clue 7: Yellow house smokes Dunhill
                    if yellow != dunhill:
                        continue
                    # Clue 12: BlueMaster smoker drinks beer
                    if bluemaster != beer:
                        continue
                    # Clue 13: German smokes Prince
                    if german != prince:
                        continue

                    for pet in permutations(houses):
                        # pet[0]=Dog, pet[1]=Bird, pet[2]=Cat,
                        # pet[3]=Horse, pet[4]=Zebra
                        dog, bird, cat, horse, zebra = pet

                        # Clue 2: Swede keeps dogs
                        if swede != dog:
                            continue
                        # Clue 6: Pall Mall smoker keeps birds
                        if pallmall != bird:
                            continue
                        # Clue 10: Blend smoker lives next to cat owner
                        if abs(blend - cat) != 1:
                            continue
                        # Clue 11: Horse owner lives next to Dunhill smoker
                        if abs(horse - dunhill) != 1:
                            continue
                        # Clue 15: Blend smoker lives next to water drinker
                        if abs(blend - water) != 1:
                            continue

                        # All clues satisfied! Determine answers.
                        nationalities = ['Brit','Swede','Dane','Norwegian','German']
                        zebra_owner = nationalities[list(nat).index(zebra)]
                        water_drinker = nationalities[list(nat).index(water)]
                        return {
                            'zebra_owner': zebra_owner,
                            'water_drinker': water_drinker
                        }

result = solve_zebra_puzzle()
print(result)
# Expected: {'zebra_owner': 'German', 'water_drinker': 'Norwegian'}

This brute-force approach works but is slow (up to 5!^5 = ~24 billion checks worst case). Early pruning (the continue statements) reduces the search enormously in practice. For a much faster solution, explore constraint propagation using the python-constraint library.

Part 3: Family Relationships in FOL — Solution

Logical Definitions

Using Parent(x, y), Male(x), Female(x):

# Formal FOL definitions:

# Father(x, y) ≡ Parent(x, y) ∧ Male(x)
def father(x, y, facts):
    return (x, y) in facts['parent'] and x in facts['male']

# Mother(x, y) ≡ Parent(x, y) ∧ Female(x)
def mother(x, y, facts):
    return (x, y) in facts['parent'] and x in facts['female']

# Sibling(x, y) ≡ ∃z (Parent(z, x) ∧ Parent(z, y)) ∧ x ≠ y
def sibling(x, y, facts):
    if x == y:
        return False
    parents_x = {p for p, c in facts['parent'] if c == x}
    parents_y = {p for p, c in facts['parent'] if c == y}
    return bool(parents_x & parents_y)  # Non-empty intersection

# Grandparent(x, y) ≡ ∃z (Parent(x, z) ∧ Parent(z, y))
def grandparent(x, y, facts):
    children_of_x = {c for p, c in facts['parent'] if p == x}
    parents_of_y  = {p for p, c in facts['parent'] if c == y}
    return bool(children_of_x & parents_of_y)

# Uncle(x, y) ≡ Male(x) ∧ ∃z (Parent(z, y) ∧ Sibling(x, z))
def uncle(x, y, facts):
    if x not in facts['male']:
        return False
    parents_of_y = {p for p, c in facts['parent'] if c == y}
    return any(sibling(x, p, facts) for p in parents_of_y)

# Example usage:
facts = {
    'parent': {('Alice', 'Bob'), ('Alice', 'Carol'), ('Dave', 'Bob'),
               ('Dave', 'Carol'), ('Bob', 'Eve'), ('Frank', 'Eve')},
    'male':   {'Dave', 'Bob', 'Frank'},
    'female': {'Alice', 'Carol', 'Eve'}
}

print(father('Dave', 'Bob', facts))      # True
print(sibling('Bob', 'Carol', facts))    # True
print(grandparent('Alice', 'Eve', facts)) # True
print(uncle('Carol', 'Eve', facts))      # False (Carol is Female)

Part 4: Truth Table Solver — Solution

import itertools
import re

def parse_variables(formula):
    """Extract unique variable names (uppercase letters) from formula string."""
    # Find all uppercase letter sequences not followed by lowercase (avoids keywords)
    variables = sorted(set(re.findall(r'\b[A-Z][A-Z0-9]*\b', formula)))
    return variables

def evaluate_formula(formula, assignment):
    """Evaluate a formula string given a dict of variable assignments."""
    # Replace implication: A -> B becomes (not A or B)
    # Handle -> before substituting variables
    expr = formula

    # Replace variable names with their truth values
    for var, val in sorted(assignment.items(), key=lambda x: -len(x[0])):
        expr = re.sub(r'\b' + var + r'\b', str(val), expr)

    # Replace -> with Python-compatible form: (P -> Q) ≡ (not P or Q)
    # Simple left-to-right replacement (works for non-nested single ->)
    while '->' in expr:
        expr = re.sub(r'(True|False|\([^()]+\))\s*->\s*(True|False|\([^()]+\))',
                      r'(not \1 or \2)', expr)

    return eval(expr)

def generate_truth_table(formula):
    """Generate and print a truth table for the given formula."""
    variables = parse_variables(formula)
    n = len(variables)

    # Header
    header = ' | '.join(variables) + ' | ' + formula
    print(header)
    print('-' * len(header))

    for values in itertools.product([True, False], repeat=n):
        assignment = dict(zip(variables, values))
        result = evaluate_formula(formula, assignment)

        row_values = ' | '.join('T' if v else 'F' for v in values)
        result_str = 'T' if result else 'F'
        print(f"{row_values} | {result_str}")

# Test the solver
print("=== P -> Q ===")
generate_truth_table("P -> Q")

print("\n=== not P or Q ===")
generate_truth_table("not P or Q")
# Should match P -> Q exactly

print("\n=== P and Q ===")
generate_truth_table("P and Q")

Each puzzle in this lab exercised a different logical skill:

Knights and Knaves — translating self-referential English into propositional formulas and checking consistency
Zebra Puzzle — exhaustive search with constraint pruning (a taste of constraint satisfaction from Unit 4)
Family Relationships — defining derived predicates from base predicates in first-order logic
Truth Table Generator — building the evaluator that underlies every logical reasoner

Together, these skills form the practical toolkit for working with formal logic in software.

Next: 5.W Wrap-Up and Self-Assessment →

This work is licensed under CC BY-SA 4.0.