Bring light into your math problems by modeling them and letting a solver do the heavy lifting. In this blog post we will show you a clever way to solve a riddle. For that end, we will model it as a satisfiability modulo theories (SMT) problem and let a theorem prover hand us the solution. You might know the riddle in question, it is about figuring out how fast four persons can cross a bridge at night. If you think you already know the answer, how can you be sure that there is not a faster possibility? Let’s find out!
Let’s first take a look at the riddle we are going to solve, a variant of the well-known bridge and torch problem: Imagine four people are standing in front of a bridge at night. They have only one flashlight, and the bridge can carry only two people at a time. The people go at different speeds. When two of them cross the bridge, the faster one adjusts their speed to the slower one. The first one needs 1 minute for crossing the bridge, the second one 2 minutes, the third 5 minutes and the last one needs 10 minutes. When two persons cross the bridge and they are not the last two, one has to go back to hand over the flashlight. What is the fastest way for all of them to cross the bridge safely?
To learn all you need for solving our riddle check out the first post of this blog series, where you can get experience by modeling your first hands-on SMT example and playing around with a solver.
Modeling the Riddle
We will model the riddle in SMT-LIB language and use the Z3 theorem prover by Microsoft (you can find an online version of Z3 on https://compsys-tools.ens-lyon.fr/z3). Similar to a coding problem there are many possibilities on how to tackle the problem at hand. We will take a look at one of them:
We have four persons, let’s identify them by calling them A, B, C and D, where A and B are the first two to cross the bridge. One of them goes back to hand over the flashlight. Then C and either D or the returning one go. Now already three people are standing on the other side of the bridge. One of them brings back the flashlight again. Then there are only two left to cross the bridge. Note that until we assign conditions to our four persons, we can pick from them since they are the same to us. Hence, we can fix A and B arbitrarily as the first two walkers and C to be the third.
We need to figure out the time mapped to each of our persons. For simplicity, we can just represent a person as the corresponding time. Thus, let’s declare them as integers.
(declare-const A Int)
(declare-const B Int)
(declare-const C Int)
(declare-const D Int)
Each person is mapped to either 1, 2, 5 or 10, but each time only occurs once. For modeling this we can use the built-in predicate distinct, which ensures that among the arguments it receives none occurs more than once.
(assert (or (= A 1) (= A 2) (= A 5) (= A 10)))
(assert (or (= B 1) (= B 2) (= B 5) (= B 10)))
(assert (or (= C 1) (= C 2) (= C 5) (= C 10)))
(assert (or (= D 1) (= D 2) (= D 5) (= D 10)))
(assert (distinct A B C D))
Next, we model the order in which they cross the bridge by representing the walkers again as integers to match the type of our persons. In total, we need variables to denote the first two, the first returner, the second two, the second returner and the last two crossing the bridge. We consolidate two persons who cross the bridge together to an array of integers. Since we want to map positions of integer type to integer values, the requested type is (Array Int Int).
(declare-const firstWalkers (Array Int Int))
(declare-const firstReturner Int)
(declare-const secondWalkers (Array Int Int))
(declare-const secondReturner Int)
(declare-const thirdWalkers (Array Int Int))
The first walkers are just A and B like explained above since we did not constrain A, B, C, nor D on the order yet. As a result, the first returner is one of A and B. Remark: One can use array entries by selecting the array at the desired position.
(assert (= (select firstWalkers 0) A))
(assert (= (select firstWalkers 1) B))
(assert (or (= firstReturner A) (= firstReturner B)))
Now, two of C, D and the first returner will cross. Since C and D are both not constrained yet, the two possibilities are whether or not the first returner is among the second walkers. Therefore, one of C and D is chosen for sure. Let’s pick C and either D or the first returner to go with C.
(assert (= (select secondWalkers 0) C))
(assert (or (= (select secondWalkers 1) firstReturner) (= (select secondWalkers 1) D)))
What are the options for the second returner, i.e. who is already on the other side of the bridge? C for sure, we just sent them over. If we sent the first returner with C, then also A or B could return the flashlight. Otherwise, the possible carriers are D and the one of A and B who did not go back the first time because then the first returner still waits on the other side for the flashlight. Remark: The predicate ite (short for “if-then-else”) takes as first argument a boolean condition and as second and third argument the expressions which the “if-then-else” term evaluates to, depending on the condition.
(assert
(or
(= secondReturner C)
(ite
(= (select secondWalkers 1) firstReturner)
(or
(= secondReturner A)
(= secondReturner B)
)
(ite
(= firstReturner A)
(or
(= secondReturner B)
(= secondReturner D)
)
(or
(= secondReturner A)
(= secondReturner D)
)
)
)
)
)
Finally, only two people still need to cross the bridge: the one we left there and the one we just sent back with the flashlight. The person waiting for the flashlight is either D or the first returner depending on who of them was one of the second walkers.
(assert (= (select thirdWalkers 0) secondReturner))
(assert
(ite
(= (select secondWalkers 1) firstReturner)
(= (select thirdWalkers 1) D)
(= (select thirdWalkers 1) firstReturner)
)
)
At this point, the four persons all crossed the bridge safely carrying the flashlight. Remember that the reasoning about your models is one of the most important aspects of modeling. A wrong specification leads to wrong outcomes. So, please be always sure to specify problems correctly by arguing logically about the model.
Let’s now compute the essence of the riddle: the minimum total time. In order to assemble the total time, we add up maximums of each two-person walks and the single returners. For deciding the maximum of two integers, we can just define a simple function ourselves. Functions can be defined using the predicate define-fun. The first argument is the function name that can be used as a predicate afterwards. We pick “max”. The input parameters are the second argument. They are given by a variable name together with the corresponding type. Since we have more than one, we need to combine them to one argument by enclosing the input parameters with parenthesis. The predicate takes the output types as a third argument and the return value as the fourth one.
(define-fun max ((i Int) (j Int)) Int
(ite
(>= i j)
i
j
)
)
(declare-const time Int)
(assert
(=
time
(+
(max
(select firstWalkers 0)
(select firstWalkers 1)
)
firstReturner
(max
(select secondWalkers 0)
(select secondWalkers 1)
)
secondReturner
(max
(select thirdWalkers 0)
(select thirdWalkers 1)
)
)
)
)
Together with (minimize time), (check-sat) and (get-model), we have finished formalizing the bridge riddle. Please find the whole SMT formula we assembled step by step in our tutorial repository, try it yourself and play around with it in a Z3 online version.
The Solution
Let’s find out what the solver computes as a solution.
Z3 yields the following output for our formula:
sat
(model
(define-fun secondWalkers () (Array Int Int)
(store ((as const (Array Int Int)) 5) 1 10))
(define-fun thirdWalkers () (Array Int Int)
(store ((as const (Array Int Int)) 2) 1 1))
(define-fun firstReturner () Int
1)
(define-fun firstWalkers () (Array Int Int)
(store ((as const (Array Int Int)) 1) 1 2))
(define-fun D () Int
10)
(define-fun time () Int
17)
(define-fun secondReturner () Int
2)
(define-fun C () Int
5)
(define-fun B () Int
2)
(define-fun A () Int
1)
)
First, the output tells us sat (short for satisfiable). Hence, there is at least one solution that satisfies our formula. Let’s take a look at the witnessing model Z3 gives us. Remark: The variables are given as predicates with zero input parameters, so we have to look at the fourth argument of define-fun to view the computed value of the variable. For instance, (define-fun c () Int 5) means that c is the person who needs 5 minutes to cross the bridge.
The interpretation of the variable time is indeed 17, as promised in the teaser in the first post of this blog series. But how can they cross the bridge that fast? The variable firstWalkers evaluates to an array with default value 1 (((as const (Array Int Int)) 1)) with value 2 stored at position 1 ((store X 1 2)). Hence, the first two positions of the array, 0 and 1, are filled with 1 and 2. The firstReturner evaluates to 1. In this manner we can see that first 1 and 2 cross the bridge, 1 returns and hands the flashlight over to 5 and 10, who cross the bridge next. Then 2 accepts the flashlight from them and goes back to 1 such that they can both cross the bridge again, yielding 2 + 1 + 10 + 2 + 2 = 17 minutes in total to cross the bridge.
Outlook
It is fun to play around with SMT formulas to see what they can do. It is even more fun to utilize solvers such as Z3 to do the heavy lifting for your real-world math problems. We at Symflower use SMT solvers to aid our symbolic execution, which finds possible execution paths through functions, gathers constraints for each path and lets solvers determine the input and output values to generate high-coverage test suites for software. As a result, Symflower finds problems in software without human interaction.
Check out the inner workings of our symbolic execution and how Symflower utilizes SMT to autonomously generate test values in our blog post series about Symflower’s Core Technology and register for our newsletter to not miss out on any upcoming posts!