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.