IA085: Satisfiability and Automated Reasoning
Seminar 4
Exercise 1 Consider an alphametics summation puzzle such as the follow-
ing:
S E N D
+ M O R E
= M O N E Y
where each letter corresponds to a decimal digit, different letters represent
different digits, and the leading digits (here S and M) cannot be zero.
Using pySMT, write a function solve_sum that receives three strings
corresponding to the three rows of the puzzle and finds its solution, if one
exists.
Exercise 2 It is possible to represent a function of one variable f : Z → Z
symbolically by a term with one free variable x of sort Int whose evaluation
gives the result of the function.
Using pySMT, write a function is_injective that given a term t representing
a function f decides whether the function is injective. Hint: The method t.substitute() might
come in handy.With suitable implementation, your the following code should output
True, True, False, False:
from pysmt.shortcuts import Symbol, Ite
from pysmt.typing import INT
x = Symbol("x", INT)
def is_injective(t):
pass
print(is_injective(x + 1)) # True
print(is_injective(x * 2)) # True
print(is_injective(Ite(x >= 0, x, -x))) # False
print(is_injective(x * x)) # False
Exercise 3 Consider the following symbolic transition system S =
(X, I, T):
X = {x, y}
I = x = 0 ∧ y = 10
T = (x ̸= 3 ∧ (x′
= x + 1)) ∨ (x = 3 ∧ (x′
= 0)) ∧
(x ̸= 2 ∧ (y′
= y + 4)) ∨ (x = 2 ∧ (y′
= y − 13))
Implement bounded model checking algorithm using pySMT and use it to
show that the transition system does not satisfy the property P = y ≥ 0.
ia085: satisfiability and automated reasoning 2
In other words, iteratively check satisfiability of the following formula
with increasing k:
I(X1) ∧
1≤i≤k−1
T(Xi, Xi+1) ∧ ¬P(Xk)
In the notation above, the set of variables Xk is a new copy of the set of
variables X that represents the system state in the time k. The formula
I(Xi) is the formula I with all variables X replaced by Xk and similarly for
T(Xi, Xi+1) and P(Xi).
The formula states that there is a sequence of k successor states that starts
with an initial state and ends with a state that does not satisfy the property.
If any of the formulas for k ≥ 1 is satisfiable, the system does not satisfy
the property.
bonus: How can you use incremental api of the smt solver to make the
algorithm faster?
Exercise 4 Consider the following symbolic transition system S =
(X, I, T): The system differs from the previous
one in the last subformula of T.
X = {x, y}
I = x = 0 ∧ y = 10
T = (x ̸= 3 ∧ (x′
= x + 1)) ∨ (x = 3 ∧ (x′
= 0)) ∧
(x ̸= 2 ∧ (y′
= y + 4)) ∨ (x = 2 ∧ (y′
= y − 11))
Implement k-induction algorithm using pySMT and use it to show that the
transition system satisfies the property P = y ≥ 0.
In other words, iteratively check satisfiability of the following two formulas
with increasing k:
φbase = I(X1) ∧
1≤i≤k−1
T(Xi, Xi+1) ∧
1≤i≤k
¬P(Xi) (1)
φind =
1≤i≤k
T(Xi, Xi+1) ∧
1≤i≤k
P(Xk) ∧ ¬P(Xk+1) (2)
If the first formula is unsat, then the first k states of the system satisfy
the property. If the second formula is unsat, then if any k successor states
satisfy the property, also the next state must satisfy the property.
If both of the formulas are unsatisfiable for some k ≥ 1, the system does
satisfy the property.
bonus: Strengthen the assumption of the formula φind so that the first k
states have to be parwise distinct. Think about how to change the transition
system so that the property cannot be proven without the strengthening and
can be proven with it.
bonus: How can you use incremental api of the smt solver to make the
algorithm faster?