Help with CS50AI Project 1 Knights Puzzle 3

Question

I've been struggling with puzzle 3 of Knights assignment. Any help would be appreciated. Seems like the issue is in depicting the statement B says "A said 'I am a knave'."Below is my code

# Puzzle 3
# A says either "I am a knight." or "I am a knave.", but you don't know which.
# B says "A said 'I am a knave'."
# B says "C is a knave."
# C says "A is a knight."
knowledge3 = And(

    # A says either "I am a knight." or "I am a knave.", but you don't know which.
    Implication(AKnight, And(Or(AKnave, AKnight), Not(And(AKnave, AKnight)))),
    Implication(AKnave, Not(And(Or(AKnave, AKnight), Not(And(AKnave, AKnight))))),

    # B says "A said 'I am a knave'."
    Implication(BKnight, Or((Implication(AKnight, AKnave)), (Implication(AKnave, Not(AKnave))))),
    Implication(BKnave, Not(Or((Implication(AKnight, AKnave)),(Implication(AKnave, Not(AKnave)))))),

    # B says "C is a knave."
    Implication(BKnight, CKnave),
    Implication(BKnave, Not(CKnave)),

    # C says "A is a knight."
    Implication(CKnight, AKnight),
    Implication(CKnave, Not(AKnight)),

    # A is either a Knight or Knave, not both
    Or(AKnave, AKnight), Not(And(AKnave, AKnight)),

    # B is either a Knight or Knave, not both
    Or(BKnave, BKnight), Not(And(BKnave, BKnight)),

    # C is either a Knight or Knave, not both
    Or(CKnave, CKnight), Not(And(CKnave, CKnight))
    )

Answer 1

When embedded in model-checking code provided in the project handout, the output of the solution provided by the OP is:

A is a Knight
A is a Knave
B is a Knight
B is a Knave
C is a Knight
C is a Knave

I believe that there are 3 issues with that solution.

1. Missing general information

The fact that A must be either a knight or a knave doesn't seem to be encoded in the knowledge base. The same applies to B and C.

This is general knowledge that's common to all puzzles in the project.

2. Encoding of 'A says either "I am a knight." or "I am a knave.", but you don't know which.'

# A says either "I am a knight." or "I am a knave.", but you don't know which.
Implication(AKnight, And(Or(AKnave, AKnight), Not(And(AKnave, AKnight)))),
Implication(AKnave, Not(And(Or(AKnave, AKnight), Not(And(AKnave, AKnight))))),

The above encoding is equivalent to A saying "I am a knave or a knight, but not both". Which is different from the problem statement 'A says either "I am a knight." or "I am a knave.", but you don't know which.'

The difference seem to be subtle but it turns out to be a game changer.

The statement "I am a knave or a knight, but not both" is always true. So one can infer that A must be a knight on the spot without checking any other statements.

'A says either "I am a knight." or "I am a knave.", but you don't know which.' is quite different though. Neither a knight or a knave could say "I am a knave." so we can immediately conclude that A actually said "I am a knight.". Which could be the case both if A is a knight or if A is a knave.

The above difference in conclusions shows that the encoding of the statement 'A says either "I am a knight." or "I am a knave.", but you don't know which.' is not accurate.

3. Encoding of 'B says "A said 'I am a knave'."'

# B says "A said 'I am a knave'."
Implication(BKnight, Or((Implication(AKnight, AKnave)), (Implication(AKnave, Not(AKnave))))),
Implication(BKnave, Not(Or((Implication(AKnight, AKnave)),(Implication(AKnave, Not(AKnave)))))),

The above is equivalent to 'If B is a knight then " (AKnight -> AKnave) OR (AKnave -> ¬AKnight)" and if B is a knave then it's the opposite'. Don't we want both nested implications to be true?

Answer 2

You do not actually need to encode the statement

B Says "A said I am a knave"

Even without it, the answer will be correct as the information is inferrable from the rest of the statements.

And an additional hint- I found the Biconditional symbol really useful!