Automated Reasoning - Assignment 1 solution

Foreword
In the explanation of our solutions to the given problems we are using two notations. The reason of this choice is that the notation seen in class (Notation 2 ) is not always applicable in a straightforward way for some of the conditions that we came up with during the resolution of the problems. For example, when
we are dealing with "big condition" composed by combinations of "smaller propositional formulas", the notation seen in class is not suitable, so we will use Notation 1.
Example:
Notation 1:
A1  0 AND A2  0 AND A3  0
Notation 2:
^3
i=1
Ai  0
Problem 1
Since each truck delivers a certain number of pallets of obscure building blocks, we denote the number of items of a certain J-building block delivered by truck 1 as J1 where J is the item and 1 is the truck
number. Hence, in the given scenario:

Number of pallets of nuzzles delivered by truck 1= N1
Number of pallets of prittles delivered by truck 1= P1
Number of pallets of skipples delivered by truck 1= S1
Number of pallets of crottles delivered by truck 1= C1
Number of pallets of dupples delivered by truck 1= D1

We assign variables N2; P2; S2;C2;D2 to truck 2 and similarly for trucks 3,4,5 and 6.
The conditions of delivery state that the following need to be delivered:
 Four pallets of nuzzles, each of weight 700 kg.
 A number of pallets of prittles, each of weight 800 kg.
 Eight pallets of skipples, each of weight 1000 kg.
 Ten pallets of crottles, each of weight 1500 kg.
 Five pallets of dupples, each of weight 100 kg.
From the conditions above,
4  700 + X  800 + 8  100 + 10  1500 + 5  100  6  7800
where X is the total number of pallets of prittles.
1
Every truck has a capacity of 7800 kg:
Notation 1:
N1  700 + P1  800 + S1  1000 + C1  1500 + D1  100  7800
N2  700 + P2  800 + S2  1000 + C2  1500 + D2  100  7800
N3  700 + P3  800 + S3  1000 + C3  1500 + D3  100  7800
N4  700 + P4  800 + S4  1000 + C4  1500 + D4  100  7800
N5  700 + P5  800 + S5  1000 + C5  1500 + D5  100  7800
N6  700 + P6  800 + S6  1000 + C6  1500 + D6  100  7800
Notation 2:
^6
i=1
Ni  700 + Pi  800 + Si  1000 + Ci  1500 + Di  100  7800
Every truck can carry at most 8 pallets:
Notation 1:
N1 + P1 + S1 + C1 + D1  8
N2 + P2 + S2 + C2 + D2  8
N3 + P3 + S3 + C3 + D3  8
N4 + P4 + S4 + C4 + D4  8
N5 + P5 + S5 + C5 + D5  8
N6 + P6 + S6 + C6 + D6  8
Notation 2:
^6
i=1
Ni + Pi + Si + Ci + Di  8
Since prittles and crottles are an explosive combination, they are not allowed to be put in the same truck.
Hence, the number of pallets of prittles in a truck is 0 or the number of pallets of crottles in a truck is 0 or both the number of pallets of prittles and crottles are 0.
Notation 1:
(P1 = 0) OR (C1 = 0)
(P2 = 0) OR (C2 = 0)
(P3 = 0) OR (C3 = 0)
(P4 = 0) OR (C4 = 0)
(P5 = 0) OR (C5 = 0)
(P6 = 0) OR (C6 = 0)
Notation 2:
^6
i=1
Pi = 0 _ Ci = 0
Since only two of the six trucks have facility for cooling skipple, we can say that only two trucks can have the number of skipples greater or equal to 1. This condition can be expressed by:
((S1  1)AND(S2  1)AND(S3 = 0)AND(S4 = 0)AND(S5 = 0)AND(S6 = 0)) OR
((S1  1)AND(S2 = 0)AND(S3  1)AND(S4 = 0)AND(S5 = 0)AND(S6 = 0)) OR
...
((S1 = 0)AND(S2 = 0)AND(S3 = 0)AND(S4 = 0)AND(S5  1)AND(S6  1))
2
We have 15 combinations to express that only 2 of the trucks are allowed to carry skipples.
The nal condition is that no 2 or more pallets of dupples can be in the same truck as they are very valuable. Hence, each truck may carry at most 1 dupple.
Notation 1:
(D1  1)AND(D2  1)AND(D3  1)AND(D4  1)AND(D5  1)AND(D6  1)
Notation 2:
^6
i=1
Di  1
These formulas are expressed in SMT syntax and by using Yices, we obtain the maximum number of pallets of prittles equals to 18. The contents of each truck are shown in Table 1.
Item Truck 1 Truck 2 Truck 3 Truck 4 Truck 5 Truck 6
Nuzzles 2 0 1 0 1 0
Prittles 0 7 0 7 0 4
Skipples 0 0 0 0 4 4
Crottles 4 0 4 0 2 0
Dupples 1 1 1 1 1 0
Table 1: Results
Remarks:
By varying in the conditions of the code the number of X (which is the number of pallets of prittles, as shown in the rst condition), it is found that for X  19 the set of conditions are unsatis able.
Therefore, the maximum number of pallets of prittles is 18.

Problem 2
After an accurate analysis of the text we decided to choose the logic QF UFLRA (the logic for Linear Real Arithmetic) to solve this problem using Yices' libraries. This choice is mainly guided by the fact
that, at some point in the problem resolution, we have to nd the center of rectangular components and these calculations could result in a non-integer number. Moreover, since the execution of programs to
verify satis ability is typically faster when dealing with real numbers instead of integers and because we had no restriction in using one speci c type between the two, we opted for reals. In order to solve the problem we de ne for every regular component for k from 1 to 8:
 an initial point on the x-coordinate "rkxi";
 an initial point on the y-coordinate "rkyi";
 a nal point on the x-coordinate "rkxf";
 a nal point on the y-coordinate "rkyf";
And for every power component for j from 1 to 3:
 an initial point on the x-coordinate "pj xi";
 an initial point on the y-coordinate "pj yi";
 a nal point on the x-coordinate "pj xf";
 a nal point on the y-coordinate "pj yf";
 the x-coordinate of the center of the component "pj xc";
 the y-coordinate of the center of the component "pj yc";

Then we set the value of the initial point of every component on the Cartesian coordinates to be greater or equal than zero for every component (both regular and power)
Notation 1:
rkxi  0 AND rkyi  0 AND pjxi  0 AND pjyi  0
Notation 2:
^8
k=1
rkxi  0;
^8
k=1
rkyi  0;
^3
j=1
pjxi  0;
^3
j=1
pjyi  0
After that, we write the conditions for the constraint which states that all the components must stay onba 29x22 chip and the components can be rotated in order to be on the chip (we present only the following condition which is about regular components for brevity, in the code similar conditions are written also
for every power component where there will be pj instead of rk):
(rkxi  29 􀀀W AND rkxf = rkxi +W AND rkxf  29 AND
rkyi  22 􀀀 H AND rkyf = rkyi + H AND rkyf  22) OR
(rkxi  29 􀀀 H AND rkxf = rkxi + H AND rkxf  29 AND
rkyi  22 􀀀W AND rkyf = rkyi +W AND rkyf  22)
where W and H are respectively the width and the height of each component.
Since the components can not overlap (except for their borders) we de ne a series of conditions to avoid that more than one component has the same x or y. To do that we compare the coordinates of a component with the ones of all the other components:
(rkxi  r1xf) OR (rkxf  r1xi) OR (rkyi  r1yf) OR (rkyf  r1yi)
Here we show the particular condition on the "regular component 1" compared to the other k-regularbcomponents. In the code this condition on r1 xf is extended also to the j -power components. Moreover, as previously stated, this series of conditions are written for every component but the repetition of com-
parison between two components has been avoided so, since we have a total of 11 components, than we will have 55 condition like the one presented above, to respect the non-overlap constraint.
Because of the fact that we want that at least one point of a regular component is in common with a point of a power component, we wrote the following condition:
((r1yi = p1yf) AND ((p1xf  r1xi AND p1xf  r1xf) OR (p1xi  r1xf AND p1xi  r1xi)) OR
((r1yf = p1yi) AND ((p1xf  r1xi AND p1xf  r1xf) OR (p1xi  r1xf AND p1xi  r1xi)) OR
((r1xi = p1xf) AND ((p1yf  r1yi AND p1yf  r1yf) OR (p1yi  r1yf AND p1yi  r1yi)) OR
((r1xi = p1xf) AND ((p1yf  r1yi AND p1yf  r1yf) OR (p1yi  r1yf AND p1yi  r1yi))
As before, the condition is extended comparing all the other power components (number 2 and 3) with the regular component 1. Then the condition is applied to all the other regular components.
Finally, to ensure that the position of centers of power components di er at least 17 in either the x direction or the y direction (or both), rst we calculate the x and y coordinates of each component:
Notation 1:
pjxc = (pjxi + pjxf)=2 AND pjyc = (pjyi + pjyf)=2
Notation 2:
^3
j=1
pjxc = (pjxi + pjxf)=2;
^3
j=1
pjyc = (pjyi + pjyf)=2
Then we check that the distances with the other centers is greater or equal to 17:
p1xc 􀀀 p2xc  17 OR p2xc 􀀀 p1 xc  17 OR p1yc 􀀀 p2yc  17 OR p2yc 􀀀 p1yc  17
The same is done to compare the center of power components 1-3 and 2-3.
Expressing these conditions and formulas in SMT syntax and using the Yices' libraries we get the results shown in Table 2 and illustrated in Figure 1.

Item xi xf yi yf xc yc
p1 21 23 0 4 22 2
p2 0 2 7 11 1 9
p3 18 20 17 21 19 19
r1 2 11 0 7 - -
r2 23 29 0 12 - -
r3 11 21 0 7 - -
r4 0 18 17 22 - -
r5 2 22 7 11 - -
r6 2 12 11 17 - -
r7 12 20 11 17 - -
r8 20 28 12 22 - -
Table 2: Results.
Figure 1: Graphical representation of the results

Problem 3
To solve this problem, we use 3 variables Jnt, Jns and Jne where n is the job number for each of the 12 jobs. Jnt is the running time of job n, Jns is the start time of job n and Jne is the end time of job n.
For example, J1t is the duration of job 1. J1s is the start time of job 1 and J1e is the end time of job 1.
We initialize each of the jobs with their corresponding lengths:
Notation 1:
J1t = 1
J2t = 2
J3t = 3
...
J12t = 12
5
Notation 2:
^12
n=1
Jnt = n
According to the rst requirement, all jobs run without interrupt.
Hence, we assign the end time of each job to the sum of its start time and its running time.
Notation 1:
J1e = J1s + J1t
J2e = J2s + J2t
...
J12e = J12s + J12t
Notation 2:
^12
n=1
Jne = Jns + Jnt
The second requirement states that job 3 may start only if job 1 and 2 have been nished. Hence, start time of job 3 is greater or equal to the end times of jobs 1 and 2. This requirement can be formulated
as,b(J3s  J1e) AND (J3s  J2e) Job 5 may only start if jobs 3 and 4 have been nished. Therefore, start time of job 4 is greater than or equal to the end times of jobs 3 and 4.
(J5s  J3e) AND (J5s  J4e)
Job 7 may only start if jobs 3, 4 and 6 have been nished. Start time of job 7 is greater than or equal to the end times of jobs 3,4 and 6.
(J7s  J3e) AND (J7s  J4e) AND (J7s  J6e)
Job 9 may only start if jobs 5 and 8 have been nished. Start time of job 9 is greater than or equal to the end times of jobs 5 and 8.
(J9s  J5e) AND (J9s  J8e)
Job 11 may only start if job 10 has been nished. Hence, start time of job 11 is greater than or equal to the end time of job 10.
(J11s  J10e)
Job 12 may only start if jobs 9 and 11 have been nished:
(J12s  J9e) AND (J12s  J11e)
Since jobs 5,7 and 10 require a special equipment of which only one copy is available, no two of these jobs may run at the same time.
Hence, start of job 5 is greater than end time of job 7 or end time of job 5 is smaller than the start time of job 7  start of job 5 is greater than end time of job 10 or end time of job 5 is smaller than the start time of job 10
 start of job 7 is greater than end time of job 10 or end time of job 7 is smaller than the start time of job 10
((J5s  J7e) OR (J5e  J7s)) AND
((J5s  J10e) OR (J5e  J10s)) AND
((J10s  J7e) OR (J10e  J7s))
6
Job Start time End time
J1 1 2
J2 0 2
J3 2 5
J4 0 4
J5 10 15
J6 0 6
J7 15 22
J8 7 15
J9 15 24
J10 0 10
J11 10 21
J12 24 36
Table 3: Results
We express these requirements and formulas in SMT syntax and using the Yices' libraries and we obtain the minimal running time, tm = 36. The running time of each job is shown in Table 3.
Remarks:
By varying tm, which is equal to the end time of the last job (which is job 12 in this case) it is foundbthat for tm  35 the set of equations and inequalities are unsatis able. Therefore, the minimal running time is 36.

Problem 4

In order to solve this problem we decided to use NuSMV because, while reading the text of the problem, it is easy to identify all the elements that are part of a Reachability problem. In particular for the resolution of the problem we de ne:
 Initial states: the seven integer variables a1, ... , a7 which has initial values ai = i. In NuSMV
syntax:
INIT
a1 = 1 & a2 = 2 & a3 = 3 & a4 = 4 & a5 = 5 & a6 = 6 & a7 = 7
 Transition relations: during the execution of the code one of the ai is choosen and it is set to ai = ai􀀀1 + ai+1 while the other variables remain unchanged. In NuSMV syntax:
TRANS
((next(a1) = a1) & (next(a2) = a1 + a3) & (next(a3) = a3) & (next(a4) = a4) & (next(a5) = a5)
& (next(a6) = a6) & (next(a7) = a7)) j
((next(a1) = a1) & (next(a2) = a2) & (next(a3) = a2 + a4) & (next(a4) = a4) & (next(a5) = a5)
& (next(a6) = a6) & (next(a7) = a7)) j
((next(a1) = a1) & (next(a2) = a2) & (next(a3) = a3) & (next(a4) = a3 + a5) & (next(a5) = a5)
& (next(a6) = a6) & (next(a7) = a7)) j
((next(a1) = a1) & (next(a2) = a2) & (next(a3) = a3) & (next(a4) = a4) & (next(a5) = a4 + a6)
& (next(a6) = a6) & (next(a7) = a7)) j
((next(a1) = a1) & (next(a2) = a2) & (next(a3) = a3) & (next(a4) = a4) & (next(a5) = a5) &
(next(a6) = a5 + a7) & (next(a7) = a7)) j
((next(a1) = a1) & (next(a2) = a2) & (next(a3) = a3) & (next(a4) = a4) & (next(a5) = a5) &
(next(a6) = a6) & (next(a7) = a7))
 Final states: we want to see if it is possible that after a certain number of steps one variable is greater or equal to 50 and at least another variable has the same value. Reachability in NuSMV is checked by looking for a counterexample for LTLSPEC G !P where P is the formula that expresses the nal states and G means that the property P holds globally. So, in our case, we de ne:
7
LTLSPEC G !(
(( a2  50 ) & (( a2 = a3 ) j ( a2 = a4 ) j ( a2 = a5 ) j ( a2 = a6 ))) j
(( a3  50 ) & (( a3 = a2 ) j ( a3 = a4 ) j ( a3 = a5 ) j ( a3 = a6 ))) j
(( a4  50 ) & (( a4 = a2 ) j ( a4 = a3 ) j ( a4 = a5 ) j ( a4 = a6 ))) j
(( a5  50 ) & (( a5 = a3 ) j ( a5 = a4 ) j ( a5 = a2 ) j ( a5 = a6 ))) j
(( a6  50 ) & (( a6 = a3 ) j ( a6 = a4 ) j ( a6 = a5 ) j ( a2 = a6 )))
)
Executing the above code using the NuSMV, we get FALSE with a counterexample ai = aj6=i  50.
Remarks:
1. We noticed a great dissimilarity of time execution and a di erence in the results when changing the range of validity of the ai variables, de ned in NuSVM syntax:
VAR
a1 : 1..N;
a2 : 2..N;
a3 : 3..N;
a4 : 4..N;
a5 : 5..N;
a6 : 6..N;
a7 : 7..N;
Where N is the maximum value of the range.
We observed that if we set N = 50, than we get a2 = a5 = 50 in a couple of seconds;
 if we set 50 < N  65, than we get a2 = a5 = 51 within a minute;
 if we set N 65, than we still get a2 = a5 = 51 but the time of execution is greater than a minute and it keeps growing and growing.
All the above results (which are displayed as counterexamples in the console) are obtained in the same states:
􀀀 State : 1:10 < 􀀀
a2 = 50
􀀀 State : 1:11 < 􀀀
a5 = 50
(The same happens for N 50 where a2 and a5 would be 51)
Moreover we noticed that reducing the number of N only for a1 and a7 does not make any di erence for both the results and the execution time since these variable always have the same value (even if they are stored as constants by doing a1 : 1..1; a7 : 7..7;).
2. In the transition relations, the relations (next(a1) = a1) and (next(a7) = a7) are inserted because the code is not working otherwise.
Furthermore the last relation:
((next(a1) = a1) & (next(a2) = a2) & (next(a3) = a3) & (next(a4) = a4) & (next(a5) = a5) & (next(a6) = a6) & (next(a7) = a7)) is added to avoid deadlock. Even so, the code works and gives the same results also without this
relation.
Powered by