Previously, I wrote how to solve sudoku and nonograms with ruby and Z3.
Let's try something much more devious and complex - the Self-Referential Aptitude Test, a 20-question multiple-choice test where answers depend on other answers.
By the way the test is totally solvable by pen and paper, I'd say it should take about half an hour, and no excessive backtracking.
There's going to be a lot of code, but hopefully with my explanations it will all turn to be straightforward.
Basic structure
First, let's setup basic structure. Z3.Int("Q1") to Z3.Int("Q20") will be answers to the questions, with A being 1, B being 2, C being 3, D being 4, and E being 5. I'm going to create a Hash storing question symbols, as we'll be using them a lot.To make the code read more like DSL than a blob of math, I'm going to define a lot of helpers.
answer(10, "A") is expression stating that answer to question 10 is A.
define(10, "A") { expression } means that answer to question 10 can be A only if expression is true. Note that this is implication, not equality, as multiple answers could be valid - see question 19 for most extreme example.
require "z3"
class SelfRefPuzzleSolver
attr_reader :q
def initialize
@solver = Z3::Solver.new
@q = {}
(1..20).each do |i|
@q[i] = Z3.Int("Q#{i}")
@solver.assert @q[i] >= 1
@solver.assert @q[i] <= 5
end
end
def answer(question_number, a)
@q[question_number] == " ABCDE".index(a)
end
def define(question_number, a)
@solver.assert answer(question_number, a).implies(yield)
end
def print_answers!
raise "Something went wrong" unless @solver.satisfiable?
model = @solver.model
(1..20).each do |i|
answer = " ABCDE"[model[q[i]].to_i]
puts "Q#{'%2d' % i}: #{answer}"
end
end
def solve!
# Question code goes here
print_answers!
end
endCode below goes inside solve! method, except for helpers which all go inside the class.
Counting answers
Many questions require counting how many times something is true - mainly how many questions have specific answer.For this we convert Z3 Booleans (which are true or false) into 1s and 0s using statement.ite(if_true, if_false), and then add 1s together with Z3.Add. Z3.Add and friends aren't anything special, and you might just as well use .inject(&:+) etc. if you prefer.
def count(*statements)
Z3.Add(*statements.map{|b| b.ite(1,0)})
end
def count_answers(a, range=1..20)
count(*range.map{|i| answer(i, a)})
endQuestion 1
The first question whose answer is B is question(A) 1
(B) 2
(C) 3
(D) 4
(E) 5
It's important to notice that answer like D means not only that "Q4 is B", but also that "Q1, Q2, and Q3 are not B".
define(1, "A"){ answer(1, "B") }
define(1, "B"){ !answer(1, "B") &
answer(2, "B") }
define(1, "C"){ !answer(1, "B") &
!answer(2, "B") &
answer(3, "B") }
define(1, "D"){ !answer(1, "B") &
!answer(2, "B") &
!answer(3, "B") &
answer(4, "B") }
define(1, "E"){ !answer(1, "B") &
!answer(2, "B") &
!answer(3, "B") &
!answer(4, "B") &
answer(5, "B") }Question 2
The only two consecutive questions with identical answers are questions(A) 6 and 7
(B) 7 and 8
(C) 8 and 9
(D) 9 and 10
(E) 10 and 11
There are shorter ways to write this answer, but let's just do it in the most straightforward way.
(1..20).each_cons(2) from ruby standard library generates a list of consecutive pairs. Then answer can be A if the only pair that's equal is 6 and 7, and so on.
question_pairs = (1..20).each_cons(2)
define(2, "A") {
Z3.And(*question_pairs.map{|i,j| (q[i] == q[j]) == (i == 6) })
}
define(2, "B") {
Z3.And(*question_pairs.map{|i,j| (q[i] == q[j]) == (i == 7) })
}
define(2, "C") {
Z3.And(*question_pairs.map{|i,j| (q[i] == q[j]) == (i == 8) })
}
define(2, "D") {
Z3.And(*question_pairs.map{|i,j| (q[i] == q[j]) == (i == 9) })
}
define(2, "E") {
Z3.And(*question_pairs.map{|i,j| (q[i] == q[j]) == (i == 10) })
}Question 3
The number of questions with the answer E is(A) 0
(B) 1
(C) 2
(D) 3
(E) 4
Since we have a helper for counting how many of specific answer we've got, it's very straighforward:
define(3, "A") { count_answers("E") == 0 }
define(3, "B") { count_answers("E") == 1 }
define(3, "C") { count_answers("E") == 2 }
define(3, "D") { count_answers("E") == 3 }
define(3, "E") { count_answers("E") == 4 }Question 4
The number of questions with the answer A is(A) 4
(B) 5
(C) 6
(D) 7
(E) 8
This is basically the same as previous question.
define(4, "A") { count_answers("A") == 4 }
define(4, "B") { count_answers("A") == 5 }
define(4, "C") { count_answers("A") == 6 }
define(4, "D") { count_answers("A") == 7 }
define(4, "E") { count_answers("A") == 8 }Question 5
The answer to this question is the same as the answer to question
(A) 1
(B) 2
(C) 3
(D) 4
(E) 5
Nothing complex here. Z3 has no problem with defining Q5 in terms of Q5.
define(5, "A") { q[5] == q[1] }
define(5, "B") { q[5] == q[2] }
define(5, "C") { q[5] == q[3] }
define(5, "D") { q[5] == q[4] }
define(5, "E") { q[5] == q[5] }Question 6
The answer to question 17 is(A) C
(B) D
(C) E
(D) none of the above
(E) all of the above
A small trick here is that "none of the above" means "Q17 is A or B", and "all of the above" is nonsensical.
define(6, "A") { answer(17, "C") }
define(6, "B") { answer(17, "D") }
define(6, "C") { answer(17, "E") }
define(6, "D") { answer(17, "A") | answer(17, "B") }
define(6, "E") { false }Question 7
Alphabetically, the answer to this question and the answer to the following question are(A) 4 apart
(B) 3 apart
(C) 2 apart
(D) 1 apart
(E) the same
Answers are already encoded as numbers, so just subtracting them will get us alphabetic distance, but it has direction (like 3 or -3) while we want just magnitude (3 in both cases). We could either get absolute value with small helper or just spell out both cases. I'll use abs helper function.
def abs(x)
(x >= 0).ite(x, -x)
endThen the code becomes:
distance_7_8 = abs(q[7] - q[8])
define(7, "A") { distance_7_8 == 4 }
define(7, "B") { distance_7_8 == 3 }
define(7, "C") { distance_7_8 == 2 }
define(7, "D") { distance_7_8 == 1 }
define(7, "E") { distance_7_8 == 0 }But this alternative isn't too bad:
distance_7_8 = q[7] - q[8]
define(7, "A") { (distance_7_8 == 4) | (distance_7_8 == -4) }
define(7, "B") { (distance_7_8 == 3) | (distance_7_8 == -3) }
define(7, "C") { (distance_7_8 == 2) | (distance_7_8 == -2) }
define(7, "D") { (distance_7_8 == 1) | (distance_7_8 == -1) }
define(7, "E") { distance_7_8 == 0 }Question 8
The number of questions whose answers are vowels is(A) 4
(B) 5
(C) 6
(D) 7
(E) 8
We could just add A and E answers, or pass custom condition to count helper:
count_vowel_answers = count_answers("A") + count_answers("E")
define(8, "A") { count_vowel_answers == 4 }
define(8, "B") { count_vowel_answers == 5 }
define(8, "C") { count_vowel_answers == 6 }
define(8, "D") { count_vowel_answers == 7 }
define(8, "E") { count_vowel_answers == 8 }Question 9
The next question with the same answer as this one is question(A) 10
(B) 11
(C) 12
(D) 13
(E) 14
Just as with question 1, we need 1+2+3+4+5 implications to cover it fully. This has similar structure to question 1, so maybe we could use a helper to DRY it up a bit. Here's we'll use the explicit version.
define(9, "A") { Z3.And(q[9] == q[10]) }
define(9, "B") { Z3.And(q[9] != q[10],
q[9] == q[11]) }
define(9, "C") { Z3.And(q[9] != q[10],
q[9] != q[11],
q[9] == q[12]) }
define(9, "D") { Z3.And(q[9] != q[10],
q[9] != q[11],
q[9] != q[12],
q[9] == q[13]) }
define(9, "E") { Z3.And(q[9] != q[10],
q[9] != q[11],
q[9] != q[12],
q[9] != q[13],
q[9] == q[14]) }Question 10
The answer to question 16 is(A) D
(B) A
(C) E
(D) B
(E) C
Completely straightforward.
define(10, "A") { answer(16, "D") }
define(10, "B") { answer(16, "A") }
define(10, "C") { answer(16, "E") }
define(10, "D") { answer(16, "B") }
define(10, "E") { answer(16, "C") }Question 11
The number of questions preceding this one with the answer B is(A) 0
(B) 1
(C) 2
(D) 3
(E) 4
This is same as counting E and A, except we limit the count to first 10 questions.
preceding_B_answers = count_answers("B", 1..10)
define(11, "A") { preceding_B_answers == 0 }
define(11, "B") { preceding_B_answers == 1 }
define(11, "C") { preceding_B_answers == 2 }
define(11, "D") { preceding_B_answers == 3 }
define(11, "E") { preceding_B_answers == 4 }Question 12
The number of questions whose answer is a consonant is
(A) an even number
(B) an odd number
(C) a perfect square
(D) a prime
(E) divisible by 5
This definitely demands a helper, and since we know counts will be between 0 and 20, it's just easier to list possible values instead of trying to come with formulas for "perfect square" or "prime".
consonant_answers = count_answers("B") +
count_answers("C") +
count_answers("D")
define(12, "A") {
equals_one_of(consonant_answers, 0, 2, 4, 6, 8, 10, 12, 14, 16, 18, 20)
}
define(12, "B") {
equals_one_of(consonant_answers, 1, 3, 5, 7, 9, 11, 13, 15, 17, 19)
}
define(12, "C") {
equals_one_of(consonant_answers, 0, 1, 4, 9, 16)
}
define(12, "D") {
equals_one_of(consonant_answers, 2, 3, 5, 7, 11, 13, 17, 19)
}
define(12, "E") {
equals_one_of(consonant_answers, 0, 5, 10, 15, 20)
}Question 13
The only odd-numbered problem with answer A is(A) 9
(B) 11
(C) 13
(D) 15
(E) 17
This of course means that problems 1, 3, 5, 7, and 19 can't have answer A.
We can use Range#step to generate list of odd numbers, and use similar code to question 2.
odd_questions = 1.step(19, 2)
define(13, "A") {
Z3.And(*odd_questions.map{|i| answer(i, "A") == (i == 9) })
}
define(13, "B") {
Z3.And(*odd_questions.map{|i| answer(i, "A") == (i == 11) })
}
define(13, "C") {
Z3.And(*odd_questions.map{|i| answer(i, "A") == (i == 13) })
}
define(13, "D") {
Z3.And(*odd_questions.map{|i| answer(i, "A") == (i == 15) })
}
define(13, "E") {
Z3.And(*odd_questions.map{|i| answer(i, "A") == (i == 17) })
}The alternative is to reverse definitions and assert that answer(9, "A") is true if and only if answer(13, "A") etc., while all unlisted odd-numbered answers are not A. In this case we need to use ==, not implies.
@solver.assert !answer(1, "A")
@solver.assert !answer(3, "A")
@solver.assert !answer(5, "A")
@solver.assert !answer(7, "A")
@solver.assert answer(9, "A") == answer(13, "A")
@solver.assert answer(11, "A") == answer(13, "B")
@solver.assert answer(13, "A") == answer(13, "C")
@solver.assert answer(15, "A") == answer(13, "D")
@solver.assert answer(17, "A") == answer(13, "E")
@solver.assert !answer(19, "A")Question 14
The number of questions with answer D is(A) 6
(B) 7
(C) 8
(D) 9
(E) 10
Same as questions 3 and 4.
define(14, "A") { count_answers("D") == 6 }
define(14, "B") { count_answers("D") == 7 }
define(14, "C") { count_answers("D") == 8 }
define(14, "D") { count_answers("D") == 9 }
define(14, "E") { count_answers("D") == 10 }Question 15
The answer to question 12 is(A) A
(B) B
(C) C
(D) D
(E) E
Straightforward:
define(15, "A") { answer(12, "A") }
define(15, "B") { answer(12, "B") }
define(15, "C") { answer(12, "C") }
define(15, "D") { answer(12, "D") }
define(15, "E") { answer(12, "E") }Question 16
The answer to question 10 is(A) D
(B) C
(C) B
(D) A
(E) E
Also straightforward:
define(16, "A") { answer(10, "D") }
define(16, "B") { answer(10, "C") }
define(16, "C") { answer(10, "B") }
define(16, "D") { answer(10, "A") }
define(16, "E") { answer(10, "E") }Question 17
The answer to question 6 is(A) C
(B) D
(C) E
(D) none of the above
(E) all of the above
Same logic as question 6, and notice how they refer to each other:
define(17, "A") { answer(6, "C") }
define(17, "B") { answer(6, "D") }
define(17, "C") { answer(6, "E") }
define(17, "D") { answer(6, "A") | answer(6, "B") }
define(17, "E") { false }Question 18
The number of questions with answer A equals the number of questionswith answer
(A) B
(B) C
(C) D
(D) E
(E) none of the above
We can use the same helper function, and only last case is different:
define(18, "A") { count_answers("A") == count_answers("B") }
define(18, "B") { count_answers("A") == count_answers("C") }
define(18, "C") { count_answers("A") == count_answers("D") }
define(18, "D") { count_answers("A") == count_answers("E") }
define(18, "E") {
Z3.And(
count_answers("A") != count_answers("B"),
count_answers("A") != count_answers("C"),
count_answers("A") != count_answers("D"),
count_answers("A") != count_answers("E"),
)
}Question 19
The answer to this question is:(A) A
(B) B
(C) C
(D) D
(E) E
This is a bit of a fake question as it's obvious that every answer works.
Of course if you want, you can add this do nothing code anyway:
define(19, "A") { answer(19, "A") }
define(19, "B") { answer(19, "B") }
define(19, "C") { answer(19, "C") }
define(19, "D") { answer(19, "D") }
define(19, "E") { answer(19, "E") }Question 20
Standardized test is to intelligence as barometer is to(A) temperature (only)
(B) wind-velocity (only)
(C) latitude (only)
(D) longitude (only)
(E) temperature, wind-velocity, latitude, and longitude
That's the only question that requires outside knowledge and the answer is obviously E.
We could list it the same way as other questions:
define(20, "A") { false }
define(20, "B") { false }
define(20, "C") { false }
define(20, "D") { false }
define(20, "E") { true }Or much more concisely:
@solver.assert answer(20, "E")Z3 is the ultimate TDD
If you wanted to write solver for Self-Referential Aptitude Test, you'd need to write something quite close to code above - syntax would be a bit different, and it would be slightly cleaner as you could use ruby values instead of Z3 expressions, but it wouldn't be much more code.And then you'd need to write the solver itself - but here we don't have to - with fully specified problem Z3 generates the answer. The only thing we wrote were tests and a few lines to print the solution. That's as TDD as it gets.
Q 1: D
Q 2: A
Q 3: D
Q 4: B
Q 5: E
Q 6: D
Q 7: D
Q 8: E
Q 9: D
Q10: A
Q11: B
Q12: A
Q13: D
Q14: B
Q15: A
Q16: D
Q17: B
Q18: A
Q19: B
Q20: EZ3 can do a lot more
I said it before, but I'll repeat it again - Z3 is great for a lot more than just solving puzzles. Puzzles simply make the best tutorial material.If you're interested, you can find more examples in gem's repository. Or just try it yourself.
2 comments:
Can you help me solve this similar puzzle? https://www.brainzilla.com/logic/self-referential-quiz/the-incredible-eight/
Anonymous: That's literally easier version of this one. You can just tweak the code slightly and it will do just fine.
Post a Comment