CS208 Coursework 1

Logical Modelling

This is the first coursework for semester one of CS208 Logic and Algorithms 2024/25.

It is worth 7.5% towards your final mark for all of CS208 (both semesters). The rest will be a second Logic coursework (worth 7.5%), Algorithms coursework in semester two (worth 15% in total), and a final exam in April/May 2025 worth 70%.

This coursework is comprised of several questions for you to do with the logical modelling tool introduced in the lectures and course notes. The questions will make use of the concepts of Logical Modelling described in part 1 of the course. The whole coursework is marked out of 20.

This page will remember the answers you type in, even if you leave the page and come back. Your browser's local storage API is used to store the data. If you delete saved data in your browser, or visit this page in private browsing mode and then close the window, you will lose your answers.

Once you have completed the questions, please click on the “Download” button to download your answers as a file called cs208-2024-coursework1.answers. When you are ready to submit your answers, please upload the file to the MyPlace submission page.

The deadline is 18:00 Wednesday 23rd October 2024. All extension requests should be submitted via MyPlace.

Question 0 (no marks)

Please enter your name and registration number:

• Name:

  <name>

• Registration number:

  <registration-number>

Question 1 (4 marks)

This question is on encoding constraints using the patterns we have seen.

For each of the questions, please read it carefully and then fill in the part that says you_fill_this_in with your answer. You can use any defined definitions you like to make your code easier to read.

Q1a (1 mark)

Replace you_fill_this_in with the necessary constraints to express that at least one of w, x, y, or z is true.

Q1b (1 mark)

Replace you_fill_this_in with the necessary constraints to express that exactly one of w, x, y, or z is true.

Q1c (2 marks)

Replace you_fill_this_in with the necessary constraints to express that exactly two of x, y, and z are true.

Hint: think about the problem in terms of individual constraints: (1) some of the atoms must be true; (2) for each of the atoms, if it is true, then so must one of the others; and (3) at least one atom is false.

Question 2: Register Allocation (5 marks)

Compilers have to translate from high level code that uses any amount of variables to low-level machine code that only has as many registers as the CPU has. This is a kind of resource allocation problem. One way to solve this problem is to use logical modelling.

As an example, we will look at the following program (though the solution you will write should work for any program by changing the constraints). The program uses six variables, and is written in Static Single Assignment (SSA) form. This means that every variable is only written to once, which makes things easier (most modern compilers use SSA internally).

1. X = 5
2. Y = 6
3. Z = X + Y
4. W = X + Z
5. U = W + Z
6. V = U + X
7. return V

Let's say we are compiling to a machine with only three registers R1, R2, R3. To systematically work out how to assign registers to variables, we need to work out the "live ranges" of each variable: the range of instructions for which a variable is required to have a place to call its own. If two variables have overlapping live ranges then they must be stored in separate registers. If not they can "share" a register.

For this program, the live ranges for each variable are as follows, where the starting instruction is when it gets assigned and the finish instruction is the last time it is used.

X : 1 to 6
Y : 2 to 3
Z : 3 to 5
W : 4 to 5
U : 5 to 6
V : 6 to 7

If two variables have ranges (s1,e1) and (s2,e2), then they can only share a register if either e1 <= s2 or e2 <= s1 (it is ok for the start of one to be the same as the end of another if we assume that the add instruction can write to the same register as one of its arguments).

Complete the solver program below to solve the register allocation in this case. You should write the constraints so that they generate all possible solutions, not just one of them. Use the examples on the resource allocation page as a guide.

Question 3: Robot World (5 marks)

The setup

The world consists of three places: the store, the factory, and the loading bay. We will represent this with a domain definition:

domain location { Store, Factory, LoadingBay }

In the world, there are two objects that may be in places or be carried by the robot: some putty and a widget:

domain object { Putty, Widget }

The possible states of the world are described by the following parameterised atoms, which can be either true or false:

atom robotIn(l : location)
atom objectIn(l : location, o : object)
atom robotHolding(o : object)

The first, robotIn(l) is true when the robot is in location l, and false otherwise. The second, objectIn(l,o) is true when the object o is in location l and false otherwise. The third, robotHolding(o) is true when the robot is holding the object o and false otherwise.

Writing our own Physical Laws

Not all possible valuations of the atoms listed above describing possible worlds make sense. We want to impose some physical laws on our worlds stating things like the robot can only be in one place. The laws we want to state are:

1. The robot is in some place.

2. The robot is in at most one place.

3. Every object is either being held by the robot or is in some location.

4. Every object is in at most one location.

5. Every object is never being held and in a location.

Physics as Logic

Fill in the definitions below to express these constraints. When 'Run' is clicked, all the worlds that are generated are ones that are physically possible given our laws of physics above.

Hint: there are many worlds that satisfy all the constraints (48 in total (why?)). To debug your solutions you can add other constraints to whittle down the number of potential solutions. For example, add robotIn(Store) to restrict to the robot being in the Store (and nowhere else, if you have implemented Law 2 correctly).

Question 4: Finding Paths (6 marks)

We now look at a simplified version of the Robot World, where we only worry about where the robot is, and where it can move to. We will look at how to use logical modelling for simplified route finding and planning problems.

The setup

We have more locations:

domain location {
  Store, Factory, LoadingBay,
  Road, Yard, WasteHeap
}

And now we add the march of time to our problems. In the end, we have to make logical formulas that only have a finite number of constraints, so we fix the number of timesteps available up front:

domain timestep { T1, T2, T3, T4, T5, Tend }

We can now express the movement of the robot throughout time using an atom parameterised by the timestep and the location:

atom robotIn(t : timestep, l : location)

The map

In order to describe the ways that the robot can move, we need to get the possible links between locations into the solver. We will use a special feature that makes a definition from a table of values that make it true:

define linked(l1 : location, l2 : location)
  table {
    (Store, Factory)
    (Factory, Store)
    (Factory, LoadingBay)
    (Store, Yard)
    (Yard, Factory)
    (Yard, Store)
    (LoadingBay, Factory)
    (LoadingBay, Road)
  }

Time is a sequence

For our purposes, time is a sequence T1, T2, ..., Tend. We could write out the passage of time as a table as we did for linked, but there is a special feature of the solver tool that does this for us automatically. If we write next(tNow, Next) then this is true exactly when tNow and tNext are in sequence.

Route planning

Your task is to write a solver program that computes timelines of robot positions that satisfy the following constraints:

1. The robot is always somewhere.

2. The robot is never in two places.

3. For each pair of timesteps in sequence (i.e. for which next(t1,t2) is true), the two locations the robot is in are linked by the map (i.e. the linked definition).

4. The robot is in the Store at timestep T1.

5. The robot is in the Road at timestep Tend.

There are seven routes from the Store to the Road.

Finally, there is an additional task: to compute only those routes that do not visit the same place more than once.

Remember to download your answers and submit them to MyPlace.