Z3 is one of the latest SMT solver by Microsoft Research. I came to know about the Z3 theorem prover few months back and was super excited to learn about this tool. It is impressively powerful and capable of solving theories built upon arithmetic, fixed-size bit-vectors, extensional arrays, datatypes, uninterpreted functions, and quantifiers. It has API available in Java , Ocaml & Python . It’s python api is easy to use.
In this post I will be discussing an example tutorial on modelling a famous variation of Rivercrossing Puzzle called as Jealous Husband’s Problem.
The puzzle goes like this :
There are 3 couples that wish to cross a river using a boat that needs atleast 1 person to drive it and it can carry atmost 2 person in it. It also has the constraint that no woman can be in the presence of another man unless her husband is also present.
We need to find the minimum steps required to finish the challenge.
Let’s now model this puzzle in a logic system :
Assertions :
- The time increments in step size.
- The position of any person is either left or right in a given step.
- The changed position refers to transition from one side to other.
- There are 3 couples. Let the set of people be S.
Logical statements.
- The Boat should move that is, its position at next time should be different than previous one.
- If Position of a man is not equal to his wife (they are both not on same side) , then position of that wife should also be not equal to position of other men.
- The Boat can carry at most 2 person and it should carry at least 1 person.
Mathematical representation
Following the logical statements described above, here are the mathematical representation statements respectively.
Statement 1.
\( (time < timeMax) \wedge (pos(boat,t) \ne pos(boat,t+1)) \)
Statement 2.
\( (time < timeMax) \wedge \) (
\( ( pos(man1,t) \ne pos(wife1,t) ) \rightarrow ( pos(wife1,t) \ne pos(man2,t)) \vee ( pos(wife1,t) \ne pos(man3,t)) \)
\( ( pos(man2,t) \ne pos(wife2,t) ) \rightarrow ( pos(wife2,t) \ne pos(man1,t)) \vee ( pos(wife2,t) \ne pos(man3,t)) \)
\( ( pos(man3,t) \ne pos(wife3,t) ) \rightarrow ( pos(wife3,t) \ne pos(man1,t)) \vee ( pos(wife3,t) \ne pos(man2,t)) \)
)
Statement 3.
\( \forall (A,B,C) \subset S \mid \)
\( \exists a \in A \mid \) {
\( ( pos(a,t) = pos(boat,t)) \wedge (pos(a,t+1) = pos(boat,t+1) ) \) there should be atleast one position change with boat. \( \wedge \)
\((\exists b \in B \mid (b \ne a ) \wedge (pos(b,t+1) = pos(boat,t+1)) ) \) there maybe another position change of element other than previous one. \( \wedge \) \( (\exists c \in C \mid (c \ne a \wedge c \ne b ) \wedge (pos(c,t+1) = pos(c,t)) ) \) element may remain on the same side. }
Codeout
Let us now write the code !!
(Here Can1 , Can2 ,Can3 correspond to Wife1 , Wife2, Wife3)
first let’s start off by declarations.
then adding clauses one by one.
finally checking our model and printing solution.
here is the output.
here is complete code.
Hope you Enjoyed it.
References
Here are some awesome references definitely worth checking in.
- https://rise4fun.com/Z3/
- http://theory.stanford.edu/~nikolaj/programmingz3.html
- https://yurichev.com/writings/SAT_SMT_by_example.pdf , awesome book for anyone at any level.
- https://stackoverflow.com/questions/26562177/river-crossing-puzzle-in-z3 , the inspiration to this blog.