We are solving math problems on a daily basis since we were little children. Starting with the pressing question of how many sweets we can buy with our weekly pocket money, finding the perfect timetable during our university education or figuring out whether we can afford the loan for our dream house. For example, we at Symflower ask ourselves questions like “What are the different paths through code?” and “How can we find input values for a function to cover all interesting execution paths?”.
All of the above problems can be expressed using mathematical models to determine if and how they can be solved. This article offers an introduction to the basic concepts that you need to devise such models.
A Short Introduction to SAT, SMT and Theorem Provers
Consider a formula containing variables that can each have either the value true or false. In the satisfiability problem (or short SAT) one questions whether there exist truth values for all variables in the formula such that it evaluates to true. The formula is called satisfiable if this is the case, and unsatisfiable otherwise. E.g. a and not b is satisfiable since the assignments a = true and b = false witness (a and not b) = true. An example for an unsatisfiable formula is a and not a. All possible assignments of a to a truth value are a = true and a = false. The formula is false for both of them, hence it cannot be satisfied.
The satisfiability modulo theories (SMT) problem is a generalization of SAT. In addition to the theory of boolean truth values, formulas of different theories such as the theories of integers, arrays or strings are allowed. For example, if we consider the integer variables a and b, is a = a + b satisfiable? Yes, for a = 0 and b = 0 the formula evaluates to true. One can make it unsatisfiable by adding the condition b ≠ 0 to the formula.
To compute solutions to SMT problems you can use a theorem prover. A prominent one is the Z3 theorem prover by Microsoft. Z3 is available as a free online tool, which is perfect to get first hands-on experience with SMT. To get the most out of this article go ahead and play around with the following examples in Z3’s online version.
Putting the Solver to Work
To get started with the solver, let’s see a small example of an equation system. The premise is the following: Someone hires a worker for 30 days. When he works, he earns 7 pfennig per day; when he doesn’t work, he has to pay 5 pfennig per day. After 30 days neither one of them owes the other. How many days did he work and how many did he have off? (Adam Ries, 16th century)
To model this problem in the solver we need to declare variables that represent the number of days he worked and had off. We can do this with the predicate declare-const. The predicate is written first followed by its arguments together in parantheses. When we name the variables workDays and holidays, the declaration looks like this:
(declare-const workDays Int)
(declare-const holidays Int)
Now we have to state what should be satisfied by our variables. Since they stand for a number of days, they should be non-negative:
(>= workDays 0)
(>= holidays 0)
Read this as “workDays is greater than or equal to zero”. Remember, the predicate >= comes before the arguments workDay and 0.
We can teach the solver this fact by using the predicate assert, which assures that its argument results to be true.
(assert (>= workDays 0))
(assert (>= holidays 0))
Now that we have established that our variables are non-negative, let’s state in which relation they are. We know that workDays + holidays = 30 and workDays * 7 = holidays * 5.
(assert (= (+ workDays holidays) 30))
(assert (= (* workDays 7) (* holidays 5)))
Finally, we have to add (check-sat), which examines the satisfiability of this problem, i.e. if there exist values for all variables to prove the assertions. In order to see the values our variables are mapped to in case of satisfiability, we need a subsequent (get-model).
This is now our resulting example for Z3 written in SMT-LIB language:
(declare-const workDays Int)
(declare-const holidays Int)
(assert (>= workDays 0))
(assert (>= holidays 0))
(assert (= (+ workDays holidays) 30))
(assert (= (* workDays 7) (* holidays 5)))
(check-sat)
(get-model)
Go ahead and observe its result using Z3’s online version.
What does the solver tell us? The result is unsat (short for unsatisfiable), which means Z3 has proven that there are no integer values for our variables such that the assertions hold. Did we make a mistake here? We presumed that the numbers of days are within the integers. Let’s try it again without this assumption. This time we allow real values.
(declare-const workDays Real)
(declare-const holidays Real)
(assert (>= workDays 0.))
(assert (>= holidays 0.))
(assert (= (+ workDays holidays) 30.))
(assert (= (* workDays 7.) (* holidays 5.)))
(check-sat)
(get-model)
Look at that, the results are (/ 25.0 2.0) and (/ 35.0 2.0), which are nothing else than fractions. So, “workDays = 25⁄2 = 12.5” and “holidays = 35⁄2 = 17.5” witness the satisfiability of our problem.
Can you adapt the initial premise to the equation system to let Z3 compute a solution within the range of positive integers?
Did you end up with a solution? One option would be to leave the total number of days open in order to get a solvable setting where neither the employer nor the worker owes the other. Like in the following example:
(declare-const workDays Int)
(declare-const holidays Int)
(declare-const sumDays Int)
(assert (>= workDays 0))
(assert (>= holidays 0))
(assert (> sumDays 0))
(assert (= (+ workDays holidays) sumDays))
(assert (= (* workDays 7) (* holidays 5)))
(check-sat)
(get-model)
The setting does not have a unique solution any more. By asserting the sum of days to be greater than Z3’s answer you can get another solution to the problem. Do you see a pattern?
If you are eager to keep playing around with Z3, then you should install Z3 on your computer using the instructions under https://github.com/Z3Prover/z3. Apart from processing files with SMT formulas it offers an API for prominent programming languages such as Java and C++ in order to utilize Z3 in your programming projects.
Outlook to Riddling
The equation system was a small example that we could have also solved by hand. But such models can get difficult very quickly by adding more variables, constraints and complexity. In the second part of this SMT blog series we will model a riddle to let the solver do all the heavy lifting. In the meantime, let’s see if you can solve that riddle faster than the solver:
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?
Do you want a hint? They can manage to cross the bridge within seventeen minutes. How?
Have fun riddling! Register for our newsletter to not miss out on upcoming articles. The next challenge already awaits you on a 40-year-old riddle. Take a look at the second part of this SMT blog series and learn how to find a solution using a solver.