brain_check.py

brain_check.py

# A numeric lock has a 3 digit key
# "682" - One number is correct and well placed
# "614" - One number is correct but wrongly placed
# "206" - Two number are correct but wrongly placed
# "738" - Nothing is correct
# "780" - One number is correct but wrongly placed

from z3 import *

# Create three integer variables for the lock digits
d1, d2, d3 = Ints('d1 d2 d3')

# Constraint for each digit to be between 0 and 9
range_constraint = And([And(d >= 0, d <= 9) for d in [d1, d2, d3]])

# Define the constraints based on the clues

# "682" - One number is correct and well placed
clue1 = Or(
            And(d1 == 6, d2 != 8, d3 != 2), 
            And(d1 != 6, d2 == 8, d3 != 2), 
            And(d1 != 6, d2 != 8, d3 == 2)
        )

# "614" - One number is correct but wrongly placed
clue2 = Or(
            And(d1 != 6, Or(d2 == 6, d3 == 6)), 
            And(d2 != 1, Or(d1 == 1, d3 == 1)), 
            And(d3 != 4, Or(d1 == 4, d2 == 4))
        )

# "206" - Two numbers are correct but wrongly placed
clue3 = Or(
            # 2 and 0 are correct but wrongly placed
            And(d1 != 2, d2 != 0, d3 != 6, 
                Or(d1 == 0, d1 == 6), 
                Or(d2 == 2, d2 == 6), 
                Or(d3 == 2, d3 == 0)),  
            # 2 and 6 are correct but wrongly placed
            And(d1 != 2, d2 != 0, d3 != 6, 
                Or(d1 == 2, d1 == 0), 
                Or(d2 == 6, d2 == 0), 
                Or(d3 == 6, d3 == 2)),  
            # 6 and 0 are correct but wrongly placed
            And(d1 != 2, d2 != 0, d3 != 6, 
                Or(d1 == 6, d1 == 2), 
                Or(d2 == 0, d2 == 2), 
                Or(d3 == 0, d3 == 6))   
        )

# "738" - Nothing is correct
clue4 = And(d1 != 7, d2 != 3, d3 != 8)

# "780" - One number is correct but wrongly placed
clue5 = Or(
            # 7 is present but not in position 1
            And(d1 != 7, Or(d2 == 7, d3 == 7), d1 != 8, d2 != 8, d3 != 8, d1 != 0, d2 != 0, d3 != 0), 
            # 8 is present but not in position 2
            And(d2 != 8, Or(d1 == 8, d3 == 8), d1 != 7, d2 != 7, d3 != 7, d1 != 0, d2 != 0, d3 != 0),  
            # 0 is present but not in position 3
            And(d3 != 0, Or(d1 == 0, d2 == 0), d1 != 7, d2 != 7, d3 != 7, d1 != 8, d2 != 8, d3 != 8)   
        )


# Combine all constraints
constraints = And(range_constraint, clue1, clue2, clue3, clue4, clue5)

# Solve the constraints
solver = Solver()
solver.add(constraints)

# Check if a solution exists and print it
if solver.check() == sat:
    model = solver.model()
    solution = ''.join([str(model[d]) for d in [d1, d2, d3]])
    print("The code for the lock is:", solution)
else:
    print("No solution found")

# The code for the lock is: 062