Repository

## PwnFunction/learn-z3

Some challenge solutions solved using z3
155 14 3 0

# 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`

Solution

## Logical Reasoning

John, Aries, and Joseph are brothers with different ages.

1. Aries is the oldest.
2. John is not the youngest.

Who is the youngest brother?

Solution

## 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?

Solution

## 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.

Solution

## 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.

Solution

## 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;
}
``````

Solution

## 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
``````

Solution