I decided to practice by modeling some simple, hand-solvable problems using z3py. Below is an example:
### Multiple Choice (10 points each, 100 total)
1. The answer to this question is:
A. A
B. B
C. C
D. D
2. The answer to Question 5 is:
A. C
B. D
C. A
D. B
3. Among the following, which question's answer differs from the other three?
A. Question 3
B. Question 6
C. Question 2
D. Question 4
4. Which pair of questions have the same answer?
A. Questions 1 and 5
B. Questions 2 and 7
C. Questions 1 and 9
D. Questions 6 and 10
5. Among the following, which question has the same answer as this question?
A. Question 8
B. Question 4
C. Question 9
D. Question 7
6. Which two questions share the same answer as Question 8?
A. Questions 2 and 4
B. Questions 1 and 6
C. Questions 3 and 10
D. Questions 5 and 9
7. Across these ten questions, which letter is selected the fewest times?
A. C
B. B
C. A
D. D
8. Among the following, which question's answer is not adjacent in the alphabet to the answer of Question 1?
A. Question 7
B. Question 5
C. Question 2
D. Question 10
9. Suppose the statements "Question 1 and Question 6 have the same answer" and "Question X and Question 5 have the same answer" have opposite truth values. Then X equals:
A. Question 6
B. Question 10
C. Question 2
D. Question 9
10. For these ten questions, the difference between the most and fewest occurrences of the letters A, B, C, and D is:
A. 3
B. 2
C. 4
D. 1
Here is the z3py code:
#!/usr/bin/env python3
from z3 import *
LETTER_NAMES = ["A", "B", "C", "D"]
NUM_QUESTIONS = 10
def main():
qs = [Int(f"q{i + 1}") for i in range(NUM_QUESTIONS)]
solver = Solver()
for q in qs:
solver.add(And(q >= 0, q <= 3))
counts = [
Sum([If(q == letter, 1, 0) for q in qs])
for letter in range(len(LETTER_NAMES))
]
# Helper utilities -----------------------------------------------------
def eq_pair(q_idx_a, q_idx_b):
return qs[q_idx_a] == qs[q_idx_b]
def unique_question(unique_idx, group):
"""unique_idx is the question number (1-based) that differs from others in group."""
unique = qs[unique_idx - 1]
others = [qs[g - 1] for g in group if g != unique_idx]
return And(
*[unique != other for other in others],
others[0] == others[1],
others[1] == others[2],
)
def non_adjacent(q_idx_a, q_idx_b):
"""Letters on the two questions are not adjacent (difference != 1)."""
return Abs(qs[q_idx_a] - qs[q_idx_b]) != 1
def max_expr(values):
result = values[0]
for v in values[1:]:
result = If(result >= v, result, v)
return result
def min_expr(values):
result = values[0]
for v in values[1:]:
result = If(result <= v, result, v)
return result
# Question 2
q2_map = {0: 2, 1: 3, 2: 0, 3: 1}
for option, target_letter in q2_map.items():
solver.add(Implies(qs[1] == option, qs[4] == target_letter))
# Question 3
q3_group = [3, 6, 2, 4]
q3_map = {
0: 3,
1: 6,
2: 2,
3: 4,
}
for option, unique_question_number in q3_map.items():
solver.add(
Implies(
qs[2] == option,
unique_question(unique_question_number, q3_group),
)
)
# Question 4
q4_pairs = {
0: (1, 5),
1: (2, 7),
2: (1, 9),
3: (6, 10),
}
for option, (a, b) in q4_pairs.items():
solver.add(Implies(qs[3] == option, eq_pair(a - 1, b - 1)))
# Question 5
q5_map = {
0: 8,
1: 4,
2: 9,
3: 7,
}
for option, target in q5_map.items():
solver.add(Implies(qs[4] == option, eq_pair(target - 1, 4)))
# Question 6
q6_pairs = {
0: (2, 4),
1: (1, 6),
2: (3, 10),
3: (5, 9),
}
for option, (a, b) in q6_pairs.items():
solver.add(
Implies(
qs[5] == option,
And(eq_pair(a - 1, 7), eq_pair(b - 1, 7)),
)
)
# Question 7
q7_letter_map = {
0: 2, # option A claims C is the least frequent
1: 1, # option B claims B is the least frequent
2: 0, # option C claims A is the least frequent
3: 3, # option D claims D is the least frequent
}
for option, letter in q7_letter_map.items():
solver.add(
Implies(
qs[6] == option,
And(
*[
counts[letter] < counts[other]
for other in range(len(LETTER_NAMES))
if other != letter
]
),
)
)
# Question 8
q8_targets = {
0: 7,
1: 5,
2: 2,
3: 10,
}
for option, target in q8_targets.items():
solver.add(Implies(qs[7] == option, non_adjacent(target - 1, 0)))
# Question 9
def xor(a, b):
return Or(And(a, Not(b)), And(Not(a), b))
q9_targets = {
0: 6,
1: 10,
2: 2,
3: 9,
}
s1 = eq_pair(0, 5) # q1 == q6
for option, target in q9_targets.items():
s2 = eq_pair(target - 1, 4) # qX == q5
solver.add(Implies(qs[8] == option, xor(s1, s2)))
# Question 10
diff = max_expr(counts) - min_expr(counts)
q10_map = {
0: 3,
1: 2,
2: 4,
3: 1,
}
for option, value in q10_map.items():
solver.add(Implies(qs[9] == option, diff == value))
# Solve ----------------------------------------------------------------
solutions = []
while solver.check() == sat:
model = solver.model()
answers = [model[q].as_long() for q in qs]
solutions.append(answers)
solver.add(Or([q != model[q] for q in qs]))
print(f"Total solutions: {len(solutions)}")
for idx, answers in enumerate(solutions, 1):
letters = "".join(LETTER_NAMES[a] for a in answers)
print(f"Solution {idx}: {letters}")
if __name__ == "__main__":
main()
The output of the z3py code:
Solved with `solver.py` using Z3.
- Environment: local venv `.venv`, dependency `z3-solver`.
- Result: unique answer string `BCACACDABA`.
Simple python script to verify the result:
#!/usr/bin/env python3
from collections import Counter
ANSWERS = "BCACACDABA" # Questions 1-10
LETTERS = ("A", "B", "C", "D")
POS = {letter: idx for idx, letter in enumerate(LETTERS)}
def check_q2(ans):
mapping = {"A": "C", "B": "D", "C": "A", "D": "B"}
assert ans[4] == mapping[ans[1]]
def check_q3(ans):
mapping = {"A": 3, "B": 6, "C": 2, "D": 4}
group = [3, 6, 2, 4]
unique_q = mapping[ans[2]]
others = [q for q in group if q != unique_q]
unique_letter = ans[unique_q - 1]
other_letters = [ans[q - 1] for q in others]
assert other_letters[0] == other_letters[1] == other_letters[2]
assert unique_letter != other_letters[0]
def check_q4(ans):
mapping = {"A": (1, 5), "B": (2, 7), "C": (1, 9), "D": (6, 10)}
a, b = mapping[ans[3]]
assert ans[a - 1] == ans[b - 1]
def check_q5(ans):
mapping = {"A": 8, "B": 4, "C": 9, "D": 7}
target = mapping[ans[4]]
assert ans[target - 1] == ans[4]
def check_q6(ans):
mapping = {"A": (2, 4), "B": (1, 6), "C": (3, 10), "D": (5, 9)}
a, b = mapping[ans[5]]
assert ans[a - 1] == ans[7] == ans[b - 1]
def check_q7(ans, counts):
mapping = {"A": "C", "B": "B", "C": "A", "D": "D"}
target = mapping[ans[6]]
assert all(
counts[target] < counts[other] for other in LETTERS if other != target
)
def check_q8(ans):
mapping = {"A": 7, "B": 5, "C": 2, "D": 10}
target_letter = ans[mapping[ans[7]] - 1]
assert abs(POS[target_letter] - POS[ans[0]]) != 1
def check_q9(ans):
mapping = {"A": 6, "B": 10, "C": 2, "D": 9}
tgt = mapping[ans[8]]
same_1_6 = ans[0] == ans[5]
same_tgt_5 = ans[tgt - 1] == ans[4]
assert same_1_6 != same_tgt_5
def check_q10(ans, counts):
mapping = {"A": 3, "B": 2, "C": 4, "D": 1}
diff = max(counts.values()) - min(counts.values())
assert diff == mapping[ans[9]]
def main():
ans = list(ANSWERS)
counts = Counter(ans)
check_q2(ans)
check_q3(ans)
check_q4(ans)
check_q5(ans)
check_q6(ans)
check_q7(ans, counts)
check_q8(ans)
check_q9(ans)
check_q10(ans, counts)
print("All constraints satisfied for", ANSWERS)
if __name__ == "__main__":
main()
Questions:
- Is there a efficient way to find all of the valid solutions?
- Any suggestion of the modeling, code structure is highly appreciated.
