This coursework is worth 50% of the total marks available for this mod-

ule.  If coursework is submitted late (and where there are no extenuating circumstances):

1. If the assessment is submitted no later than 24 hours after the deadline, the mark for the assessment will be capped at the minimum pass mark;

2. If the assessment is submitted more than 24 hours after the deadline, a mark of 0 will be given for the assessment.

Your submission must include the official Coursework Submission Cover

sheet, which can be found here:

https://docs.cs.cf.ac.uk/downloads/coursework/Coversheet.pdf

Submission Instructions

All of the files must be submitted via Learning Central. Any code sub- mitted will be run on a system equivalent to that available on the laptops provided to the students on request and must be submitted as stipulated in the instructions above. The code should run without any change.

Any deviation from the submission instructions above  (including the number and types of files submitted) may result in a mark of zero for the assessment or question part.

Staff reserve the right to invite students to a meeting to discuss course- work submissions.

Assignment

The coursework asks you to solve constraint satisfaction problems using the Z3 theorem prover.   It consists of three parts:   (1) rectangle fitting,  (2) program correctness and (3) novel problem.

Part 1: Rectangle Fitting [8 marks]

Provide Z3 or Z3Py code to solve the rectangle fitting problem given as follows. We want to fit five rectangles #1, #2, #3, #4 and #5 into a single rectangle with size of 10  10 (width height). Any solutions to the rectangle fitting problem must satisfy all of the following constraints.

(1) Rectangles #1, #2, #3, #4 and #5 have respectively sizes of 6  6, 2  7, 2  9, 3  6 and 1  10 (width height or height width).

(2) The x and y coordinates of the left lower corner of each rectangle are both equal to or larger than 0.

(3) The x and y coordinates of the right upper corner of each rectangle are both equal to or less than 10.

(4) Any two rectangles do not overlap each other.

In the provided code, you may declare only four functions whose domains and ranges are both the set of integers.

1. Function W maps each rectangle to its width.

2. Function H maps each rectangle to its height.

3. Function X maps each rectangle to the x-coordinate of its left lower corner.

4. Function Y maps each rectangle to the y-coordinate of its left lower corner.

Explain a solution to the rectangle fitting problem. The solution should be obtained by running the code in the command-line interface with either of the following commands.

$  z3  -smt2  P1_[Student  number].txt

$  python  P1_[Student  number].py

Here, P1_[Student number] is your file containing the code. The explana- tion should include the output of the code and information about the exact position of each rectangle. The following is an example explanation for the position of rectangle #1.

; Rectangle #1 has  coordinates  (0,0),  (6,0),  (0,6)  and  (6,6).

As shown above, insert symbol “ ;” (“#” for Z3Py) at the beginning of each line in which your explanation is provided.  All the explanations should be written at the very end of the file containing the code.

Part 2: Program Correctness [14 marks]

Provide Z3 or Z3Py code to establish the possibility that the following pro- gram causes a crash.

1:  a     1

2:  b      1

3:  for i      0 to 15 do

4:       if ?1  then

5:            a     a + i

6:             b      a + b

7:       else if ?2  then

8:             b      b + 2i

9:       else

10:             a      a + b

11:        end if

12:        if b = 1000 then

13:             crash

14:        end if

15:  end for

Here, “   ” is an assignment operator, and “?1” and “?2” are unknown tests that may yield false or true in any situation.

Explain the constraints implemented in the code. The explanation should be commented on right before the corresponding part of the code in the source code file.

Demonstrate a crash by giving values of a and b, for all i specified in the program. All of the values should be obtained by running the provided code in the command-line interface with either of the following commands.

$  z3  -smt2  P2_[Student  number].txt

$  python  P2_[Student  number].py

Here, P2_[Student number] is your file containing the code.   The crash you demonstrate must be different from the crash the following example demonstrates.

a  =  [1,2,3,3,3,17,22,28,35,134,143,153,153,570,583,597]

b  =  [1,1,4,8,14,14,36,64,99,99,242,395,417,417,1000,1597]

The output of the code and all of the values should be written at the very end of the file containing the code.  Do not forget to insert the comment symbol at the beginning of each line in which the explanation, output and values are provided.

Part 3: Novel Problem [28 marks]

Give and explain a problem that is solvable using Z3 or Z3Py. The problem

should be of a different kind from Part 1 and Part 2, whereas it should be of a similar size to them. The explanation should include a clear statement of the problem. It should discuss what the problem is, why it is important, and why it is hard.  The explanation should also include a clear statement of originality in the application of knowledge.  It should discuss the main existing approaches such as ideas, methods or techniques, and their strengths and limitations. It should also discuss the key components of your approach and its strengths and limitations. When you reference published literature, follow the guidance on Referencing in Code1.  The explanation should be commented on at the very beginning of the source code file.

Provide and explain your Z3 or Z3Py code and solution to the problem. The explanation should address declarations and constraints written in the source code file and a solution obtained by running the code in the command-

line interface.  The explanation of the constraints should be commented on right before the corresponding part of the code in the source code file. The output and its explanation should be commented on at the very end of the source code file.

Learning Outcomes Assessed

The coursework will allow the student to demonstrate their knowledge and practical skills and to apply the principles taught in lectures in the context of concrete applications. The coursework contributes to assess the following learning outcomes:

1. The ability to implement and evaluate automated reasoning approaches to solve a given task

2. The ability to explain the basic principles underlying common auto- mated reasoning approaches

Criteria for Assessment

Credit will be awarded against the criteria shown in the marking below.

1. The code gives an output and the output is explained. (3 marks/part)

2. Functions/constants and constraints are correctly encoded. (5 marks/part)

3. Functions/constants and constraints are correctly extracted and ex- plained. (6 marks/part)

4. The statement of the problem is clear. The clarity is assessed against the following aspects:

• What is the problem? (2 marks/part)

• Why is it important? (2 marks/part)

• Why is it hard? (2 marks/part)

5. The originality in the application of knowledge is explained.   It is assessed against the following aspects:

• What are the main existing approaches such as ideas, methods or techniques to the problem? (2 marks/part)

• What are the strengths and limitations of the main existing ap- proaches to the problem? (2 marks/part)