# 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 unsatisable.

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 satisability is typically faster when dealing with real numbers instead of integers and because we had no restriction in using one specic type between the two, we opted for reals. In order to solve the problem we dene 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 dene 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 dier 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 unsatisable. 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 dene:

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 = ai1 + 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 dene:

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 dierence in the results when changing the range of validity of the ai variables, dened 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 dierence 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.

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 unsatisable.

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 satisability is typically faster when dealing with real numbers instead of integers and because we had no restriction in using one specic type between the two, we opted for reals. In order to solve the problem we dene 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 dene 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 dier 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 unsatisable. 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 dene:

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 = ai1 + 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 dene:

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 dierence in the results when changing the range of validity of the ai variables, dened 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 dierence 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.

You'll get 1 file (164.9KB)