Cardiff School of Computer Science and Informatics

Coursework Assessment Pro-forma

Module Code:                                  CMT215

Module Title:                                   Automated Reasoning

Lecturer:                                          Hiroyuki Kido

Assessment Title:                           Implementation and evaluation of case study

Date Set:                                          5th March 2021

Submission date and Time:         29th April at 9:30AM

Return Date:                                   27th May 2021

        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

Description		Type	Name
Cover sheet	Compulsory	One pdf file	[Student number].pdf
Code for Part 1	Compulsory	One Z3/Python file	P1_[Student number].txt/py)
Code for Part 2	Compulsory	One Z3/Python file	P2_[Student number].txt/py)
Code for Part 3	Compulsory	One Z3/Python file	P3_[Student number].txt/py)

        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 Z3 or Z3Py. It consists of three parts: (1) scheduling, (2) program correctness and (3) novel problem.

Part 1: Scheduling [8 marks]

Provide Z3 or Z3Py code to solve the scheduling problem given as follows. There are six jobs #1, #2, #3, #4, #5 and #6. All jobs are executed by three persons A, B and C. Any solutions of the scheduling problem must satisfy all of the following constraints.

(1) Each job should be executed by one of three persons A, B and C without interruption.

(2) Each person can handle at most one job each time.

(3) Each job #i has running time 3 + i if person A or B executes it, and 4 + i otherwise.

(4) Job #3 should be executed by B after jobs #5 and #6 have been completed.

(5) Each job should be done in time 0 to 15.

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

1. Function S maps each job to its start time.

2. Function E maps each job to its end time.

3. Function P maps each job to the person who executes it.

        Explain a solution to the scheduling 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 the information about who executes which job, and when it starts and ends, for each job. The following is an example explanation for job #1.

Job #1 is executed by person A from time 0 to time 4.

Insert the comment symbol (“;” in Z3 and “#” in 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, 15 do

 4:      if ? then

 5:          a ← a + i

 6:          b ← a + b

 7:      else

 8:          b ← b + 2i

 9:          a ← a + b

10:      end if

11:      if b = 1010 then

12:          crash

13:      end if

14:  end for

Here, “←” is an assignment operator and “?” is an unknown test 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,5,20,24,73,134,141,359,368,378,1364,2374,2387,5812]

b = [1,1,4,9,15,39,49,61,202,218,586,964,986,1010,3397,3425]

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 ex-isting 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 Code available in Learning Materi-als in COMSC-SCHOOL in Learning Central. The explanation should be commented on at the very beginning of the source code file.

        Provide Z3 or Z3Py code and a solution to the problem devised. Explain the constraints implemented in the code and the output of the code from 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)

• What are the key components of your approach to the problem? (2 marks/part)

• What are the strengths and limitations of your approach to the problem? (2 marks/part)

	Criterion 1	Criterion 2	Criterion 3	Criterion 4	Criterion 5
Part 1	3 marks	5 marks	N/A	N/A	N/A
Part 2	3 marks	5 marks	6 marks	N/A	N/A
Part 3	3 marks	5 marks	6 marks	6 marks	6 marks
	18%	30%	24%	12%	16%

The full marks for each item will only be awarded if the requested content is fully presented. The examiner will have the discretion to award partial marks for an item if it is partially present. The following indicates the level of attainment against the appropriate award.

• Distinction (70-100%)

• Merit (60-69%)

• Pass (50-59%)

• Fail (0-50%)

Feedback

Feedback on your coursework will address the above criteria. Feedback and marks will be returned by 27th May 2021 via Learning Central. Feedback from this assignment will be useful for Dissertation CMT400 and the second assessment in this module.