learn-z3
Some simple example challenges to get started with z3.
Simple Equation
Solve for x
& y
where x + 2y = 7
, x > 2
and y < 10
Logical Reasoning
John, Aries, and Joseph are brothers with different ages.
- Aries is the oldest.
- John is not the youngest.
Who is the youngest brother?
Calculate Distribution
Spend exactly 100 dollars and buy exactly 100 animals.
- Dogs cost 15 dollars
- Cats cost 1 dollar
- Mice cost 25 cents each.
You have to buy at least one of each. How many of each should you buy?
Match Assignment
There is an assignment of unique digits to letters such that the equation send + more = money
holds.
Find an assignment of the digits to make this true.
Magic Square
A square array of numbers, usually positive integers, is called a magic square if the sums of the numbers in each row, each column, and both main diagonals are the same.
Magic square of 15 looks like: 8 1 6 3 5 7 4 9 2
Generate a magic square of 15 with z3.
Simple Weak Hash
Following is a simple hash, find the string s
such that it satifies the statement n == n2
.
private static boolean hash(final String s) {
int n = 7;
final int n2 = 593779930;
for(int i = 0; i < 6; ++i) {
n = n * 31 + s.charAt(i);
}
return n == n2;
}
Sudoku
Solve the following sudoku with z3.
0 0 0 0 9 4 0 3 0
0 0 0 5 1 0 0 0 7
0 8 9 0 0 0 0 4 0
0 0 0 0 0 0 2 0 8
0 6 0 2 0 1 0 5 0
1 0 2 0 0 0 0 0 0
0 7 0 0 0 0 5 2 0
9 0 0 0 6 5 0 0 0
0 4 0 9 7 0 0 0 0