Cardiff School of Computer Science and Informatics Coursework Assessment Pro-forma
Module Code: Module Title: Lecturer: Assessment Title:
Date Set:
Submission date and Time: Return Date:
Solutions
Part 1: Scheduling
CMT215
Automated Reasoning
Hiroyuki Kido
Implementation and evaluation of case study
4th March 2021
29th April at 9:30AM
27th May 2021
Here is a sample file of P1_[Student number].txt.
(declare-fun S (Int) Int) ; S maps job #i into its start time.
(declare-fun E (Int) Int) ; E maps job #i into its end time.
(declare-fun P (Int) Int) ; P maps job #i into the person who executes it.
(assert
(and
; (1) Each job should be executed by one of three persons A, B, C.
(or (= (P 1) 1) (= (P 1) 2) (= (P 1) 3))
(or (= (P 2) 1) (= (P 2) 2) (= (P 2) 3))
(or (= (P 3) 1) (= (P 3) 2) (= (P 3) 3))
(or (= (P 4) 1) (= (P 4) 2) (= (P 4) 3))
(or (= (P 5) 1) (= (P 5) 2) (= (P 5) 3))
(or (= (P 6) 1) (= (P 6) 2) (= (P 6) 3))
(or (not (= (P 1) 1)) (not (= (P 1) 2)))
(or (not (= (P 1) 1)) (not (= (P 1) 3)))
(or (not (= (P 1) 2)) (not (= (P 1) 3)))
(or (not (= (P 2) 1)) (not (= (P 2) 2)))
(or (not (= (P 2) 1)) (not (= (P 2) 3)))
(or (not (= (P 2) 2)) (not (= (P 2) 3)))
(or (not (= (P 3) 1)) (not (= (P 3) 2)))
(or (not (= (P 3) 1)) (not (= (P 3) 3)))
(or (not (= (P 3) 2)) (not (= (P 3) 3)))
(or (not (= (P 4) 1)) (not (= (P 4) 2)))
(or (not (= (P 4) 1)) (not (= (P 4) 3)))
(or (not (= (P 4) 2)) (not (= (P 4) 3)))
(or (not (= (P 5) 1)) (not (= (P 5) 2)))
(or (not (= (P 5) 1)) (not (= (P 5) 3)))
(or (not (= (P 5) 2)) (not (= (P 5) 3)))
(or (not (= (P 6) 1)) (not (= (P 6) 2)))
(or (not (= (P 6) 1)) (not (= (P 6) 3)))
(or (not (= (P 6) 2)) (not (= (P 6) 3)))
; (2) Each person can handle at most one job each time.
(implies (= (P 1) (P 2)) (or (>= (S 1) (E 2)) (>= (S 2) (E 1))))
1
(implies (= (P 1) (P 3)) (or (>= (S 1) (E 3)) (>= (S 3) (E 1))))
(implies (= (P 1) (P 4)) (or (>= (S 1) (E 4)) (>= (S 4) (E 1))))
(implies (= (P 1) (P 5)) (or (>= (S 1) (E 5)) (>= (S 5) (E 1))))
(implies (= (P 1) (P 6)) (or (>= (S 1) (E 6)) (>= (S 6) (E 1))))
(implies (= (P 2) (P 3)) (or (>= (S 2) (E 3)) (>= (S 3) (E 2))))
(implies (= (P 2) (P 4)) (or (>= (S 2) (E 4)) (>= (S 4) (E 2))))
(implies (= (P 2) (P 5)) (or (>= (S 2) (E 5)) (>= (S 5) (E 2))))
(implies (= (P 2) (P 6)) (or (>= (S 2) (E 6)) (>= (S 6) (E 2))))
(implies (= (P 3) (P 4)) (or (>= (S 3) (E 4)) (>= (S 4) (E 3))))
(implies (= (P 3) (P 5)) (or (>= (S 3) (E 5)) (>= (S 5) (E 3))))
(implies (= (P 3) (P 6)) (or (>= (S 3) (E 6)) (>= (S 6) (E 3))))
(implies (= (P 4) (P 5)) (or (>= (S 4) (E 5)) (>= (S 5) (E 4))))
(implies (= (P 4) (P 6)) (or (>= (S 4) (E 6)) (>= (S 6) (E 4))))
(implies (= (P 5) (P 6)) (or (>= (S 5) (E 6)) (>= (S 6) (E 5))))
; (3) Each job i has running time 3+i if person A or B executes it,
; and 4+i otherwise.
(ite (or (= (P 1) 1) (= (P 1) 2)) (= 4 (- (E 1) (S 1))) (= 5 (- (E 1) (S 1))))
(ite (or (= (P 2) 1) (= (P 2) 2)) (= 5 (- (E 2) (S 2))) (= 6 (- (E 2) (S 2))))
(ite (or (= (P 3) 1) (= (P 3) 2)) (= 6 (- (E 3) (S 3))) (= 7 (- (E 3) (S 3))))
(ite (or (= (P 4) 1) (= (P 4) 2)) (= 7 (- (E 4) (S 4))) (= 8 (- (E 4) (S 4))))
(ite (or (= (P 5) 1) (= (P 5) 2)) (= 8 (- (E 5) (S 5))) (= 9 (- (E 5) (S 5))))
(ite (or (= (P 6) 1) (= (P 6) 2)) (= 9 (- (E 6) (S 6))) (= 19 (- (E 6) (S 6))))
; (4) Job 3 should be executed by B after jobs 5 and 6 have been completed.
(= (P 3) 2)
(>= (S 3) (E 5))
(>= (S 3) (E 6))
; (5) Each job should be done in time 0 to 15.
(>= (S 1) 0)
(>= (S 2) 0)
(>= (S 3) 0)
(>= (S 4) 0)
(>= (S 5) 0)
(>= (S 6) 0)
(<= (E 1) 15)
(<= (E 2) 15)
(<= (E 3) 15)
(<= (E 4) 15)
(<= (E 5) 15)
(<= (E 6) 15)
))
(check-sat)
(get-model)
;(model
; (define-fun P ((x!0 Int)) Int
; (ite(=x!04)1
; (ite(=x!05)1
; (ite(=x!06)2
; (ite(=x!03)2
; 3)))))
; (define-fun S ((x!0 Int)) Int
; (ite (= x!0 1) 10
; (ite(=x!02)4
; (ite(=x!03)9
; (ite(=x!04)8
; 0)))))
; (define-fun E ((x!0 Int)) Int
2
; (ite (= x!0 2) 10 ; (ite(=x!05)8 ; (ite(=x!06)9 ; 15))))
😉
; Job #1 is executed by person B from time 0 to time 5.
; Job #2 is executed by person C from time 15 to time 20.
; Job #3 is executed by person C from time 0 to time 6.
; Job #4 is executed by person A from time 9 to time 17.
; Job #5 is executed by person A from time 0 to time 9.
; Job #6 is executed by person C from time 6 to time 15.
; Job #7 is executed by person B from time 6 to time 16.
Here is a sample file of P1_[Student number].py. # Import z3 module to use z3 API in python.
from z3 import *
# There are 6 jobs.
jobs = [i+1 for i in range(6)]
# There are 3 persons.
persons = [i+1 for i in range(3)]
# Time
time = 15
# Declare function (#job -> #start time).
s = Function(‘s’, IntSort(), IntSort())
# Declare function (#job -> #end time).
e = Function(‘e’, IntSort(), IntSort())
# Declare function (#job -> #person).
p = Function(‘p’, IntSort(), IntSort())
# Create a Z3 solver instance.
slv = Solver()
for i in jobs:
# Job #i has running times i+3 if person A or B executes it.
# Job #i has running times i+4 if person C executes it.
slv.add(If(Or(p(i)==1,p(i)==2),e(i)-s(i)==i+3,e(i)-s(i)==i+4))
# Each job should be executed by one of three persons A, B, C.
constraint=[]
for j in persons:
constraint.append(p(i)==j)
# Assert a constraint.
slv.add(Or(constraint))
for j in persons:
for k in persons:
if j != k:
slv.add(Or(Not(p(i)==j),Not(p(i)==k)))
# Each person can handle at most one job each time.
for j in jobs:
if i != j:
slv.add(Implies(p(i)==p(j),Or(s(i)>=e(j),s(j)>=e(i))))
3
# Each job should be done in time 0 to 15.
slv.add(s(i)>=0)
slv.add(e(i)<=time)
# Job 3 should be executed by B after jobs 5 and 6 have been completed.
slv.add(p(3)==2)
slv.add(s(3)>=e(5))
slv.add(s(3)>=e(6))
# Print all constraints.
print(slv)
# Solve the asserted constraints.
r = slv.check()
# Exit from the program if unsatisfiable.
if r == unsat:
print(r)
exit()
# Find a solution (i.e. definitions of the function s,e and p).
m = slv.model()
# Display the solution in the symbolic expression (i.e. SMT-LIB2 format).
print(m.sexpr())
# Visualise the solution.
for j in persons:
result=[0]*time
for k in range(time):
for i in jobs:
# Obtain a value returned by the functions.
# Return Z3 integer numerals as Python long (bignum)
# numerals.
person = m.evaluate(p(i)).as_long()
start = m.evaluate(s(i)).as_long()
end = m.evaluate(e(i)).as_long()
if person==j and start<=k and k