## Description

## Problem 1

[30 points] Hidato is a famous puzzle game.

You may have already played this game on your phone. If not,

the time has finally come for you to know about it:

http://en.wikipedia.org/wiki/Hidato

Use your theory of choice to formulate a Hidato puzzle solver: “Given a partially completed grid, is it possible

to complete the grid obeying the rules of Hidato?”

If the answer is no, then a simple “NO SOLUTION” in

the output is sufficient. If the answer is yes, then you need to provide the completed grid as an output.

Input format.

The partially completed grid will be provided to you with “-” standing for each blank cell

(to be filled by a number) and “*” standing for blocked cells (not to be filled by any numbers) each two

symbols separated by a single space. Each line of the puzzle is written in a separate line of the input file.

For example, the input file:

* * 7 6 – * *

* * 5 – – * *

31 – – 4 – – 18

– 33 2 12 15 19 –

29 28 1 14 – – –

* * – 24 22 * *

* * 25 – – * *

represents the game (to be played):

* * 7 6 * *

* * 5 * *

31 4 18

33 2 12 15 19

29 28 1 14

* * 24 22 * *

* * 25 * *

is an input file for which your output should be:

* * 7 6 9 * *

* * 5 8 10 * *

31 32 3 4 11 16 18

30 33 2 12 15 19 17

29 28 1 14 13 21 20

* * 27 24 22 * *

* * 25 26 23 * *

that corresponds to the solved puzzle:

* * 7 6 9 * *

* * 5 8 10 * *

31 32 3 4 11 16 18

29 33 2 12 15 19 17

29 28 1 14 13 21 20

* * 27 24 22 * *

* * 25 26 23 * *

Do not forget: your wrapper code (in your programming language of choice) is meant to only read the

text grid, and output a formula F (in the theory of your choice) where a satisfiable assignment to F is a

solution to puzzle.

You are not allowed to do any other ”solving” in your programming language. All puzzle

solving needs to be deferred to z3. If you do any solving in your wrapper code (even if it is a little bit), you

will get a zero for this problem.

2

## Problem 2

Consider the situation that the students in a class want to team up in groups of (exactly) 2 students for a

course project.

The instructor asks each student to submit a list of partners that they are willing to work

with. These lists are not prioritized, in the sense that it is understood that a student would be equally

happy to work with anyone on her/his list. After all lists are in, the instructor is faced with the challenge of

making as many groups of 2 as possible respecting students’ wishes.

The goal of this problem is to write a

small program to help “her”.

Write a wrapper program that takes the lists of student preferences as an input, and prints in the output

the groups (of two students) formed, with the understanding that as many students as possible have been

grouped together.

You will solve this problem in two ways:

(a) (30 points) You can only use the theory of propositional logic (boolean variables only) for the purposes

of this subproblem. Solutions that use richer theories such as linear arithmetic or equality logic will

get no credit.

(b) (30 points) You can only use a richer theory of your choice. Note that the theory does not have to be

theoretically strictly more expressive; therefore, equality logic with uninterpreted functions (reducible

to propositional logic) is acceptable for this.

Keep in mind that the encoding should be genuinely different in this case compared to (a), in the

sense that you will not add superficial bells and whistles to (a) to get (b). Since this theory subsumes

propositional logic, it is certainly possible to do the superficial thing.

But, that solution will get zero

credit. So, in this case think integer variables instead of booleans, and genuine non-boolean constraints.

The purpose of the exercise is for you to contrast two different encodings of the same problem against

each other, in terms of (i) the ease of encoding, (ii) the size of encoding, and (iii) the performance of

the solver at the end.

You will submit a pdf file (grouping.pdf) containing a short report to let us

know about your conclusions regarding (i–iii). Make clear claims, and back them up by solid evidence.

But, don’t be verbose. There are 10 points dedicated to this report, which will bring the total for the

homework to 100 points.

Do not forget, in each case, like problem 1, you cannot do any solving in the wrapper code. It should

be solely for the purpose of generating and dumping a formula to z3, which will then produce the optimal

solution (including the optimization part) for you. This is in the spirit of the job shop problem you saw

in the tutorial.

For (a), you will be using the assert-soft command (not covered in the tutorial), but

explained in the online Z3 tutorial.

Input format.

For simplicity, we identify students with integer identifiers 1 . . . n (where n is the number

of students in the class). The input will have one line per student in which a (space separated) list of id’s

appear indicating the student’s choice.

For example, in a class with 5 students, the following input:

2 3 4

1 3 5

2 1

1

2

illustrates the partner choices of student “1” as {2, 3, 4}, and the partner choices of student “5” as just a

single student “2”.

The correct (maximal) output for this case then is:

2 groups formed:

1,4

2,5

or

2 groups formed:

1,3

2,5

3

It is understood that there is only one answer for the optimal number of groups that can be formed, but

the arrangement of students into groups that would produce that optimal number may not be unique.

The number should be correct, but any valid arrangement is fine. You do not need to produce all valid

arrangements for the optimal answer.

Note: This is a computationally hard problem. It could be expected, depending on the quality of your

encoding, that your code will not scale to large instances. That said, your code (even if correct) should

not be so bad in quality that it cannot solve small instances like the example given above. So, like any

other code, reasonable performance is part of the specification together with correctness.

If a group’s code

substantially outperforms everyone else’s (in solving large instances), then I will consider a bonus prize (in

the form of extra marks) for that group.

Repeat Warning

The purpose of these exercises is to solve these problems using a reduction to a satisfiability problem. If

you write a program that solves the same problem algorithmically, you will not get any credit for it. The

reason that we ask for the formula file is to verify that you are indeed doing the reduction.

The wrapper

program should only process input, generate formulas, and clean up outputs. All the problem solving should

be deferred (by way of a correct encoding) to Z3.

You have now been warned numerous times in a short

document about this single issue. There will be zero leniency regarding mistakes of this type.

Extra

If you are a genuinely interested student, I encourage you to try to separately program direct solutions

for either of these problems and compare your solution to the wrapper+solver combination. It would be

interesting to see if yours is better or worse, and how long each solution takes. This is just a suggestion for

you and has no bearing on the homework or its mark.

4