## Description

Problem 1 (30 points)

In this problem, you will experiment with giving two different encodings to the same problem, and comparing

their performance. The learning objective is to gain an understanding that there are many ways to encode

a problem as a constraint solving problem, and some are better than others.

The At-most-k constraint on n (n > k) variables (X1, . . . , Xn) is noted ≤k (X1, . . . , Xn) and satisfied iff

at most k of the X1, . . . , Xn variables are true.

1

Naive encoding Devise a simple encoding for the At-most-k constraint, and implement it in the naive(literals, k)

function.

• The function should return all the clauses of the encoding that ensures at most k literals in the list

literals can be true.

• You are not allowed to create any new variables for the encoding in this function.

Encoding using a sequential counter Sinz [?] introduced an encoding for the At-most-k constraint by

encoding a sequential counter that counts the number of Xi that are true. For more details on why this

encoding works, you can read the original paper, but this is not required for the assignment.

To encode ≤k (X1, . . . , Xn), this encoding introduces (n−1)∗k new variables {Ri,j |1 ≤ i < n, 1 ≤ j ≤ k}.

Below is the conjunctive normal form of the encoding:

¬X1 ∨ R11

Vk

j=2 ¬R1,j

Vn−1

i=2 ((¬Xi ∨ Ri,1) ∧ (¬Ri−1,1 ∨ Ri,1))

Vn−1

i=2

Vk

j=2(¬Xi ∨ ¬Ri−1,j−1 ∨ Ri,j ) ∧ (¬Ri−1,j ∨ Ri,j )

Vn−1

i=2 (¬Xi ∨ ¬Ri−1,k)

∧(¬Xn ∨ ¬Rn−1,k)

1. Implement this encoding in the sequential_counter(literals,k) function in q1.py. The function

should return all the clauses of the encoding that ensure at most k literals in the list literals are

true.

2. Compare the performance of the two encodings and write a short paragraph in the comments in q1.py

to explain which encoding performs better depending on n and k, if there is one.

To help you, a small test function has been implemented in q1.py. You can execute the script q1.py

with three arguments: E is 0 to use your encoding, 1 to use the sequential encoding. N is the number

of variables and K is the number of variables that have to be set to true (0 < K < N).

python q1.py E N K

If your encoding is correct, the response should be PASSED in (-)s, where the “- ” will be replaced

with the running time (in seconds) of the solver to solve the encoded constraints.

Note that the test function encodes the constraint ensuring exactly k variables are true, not the

weaker constraint at-most-k. To do so, it calls your implementation of at-most-k twice, with different

arguments.

Note that the goal of the test function is to encode the constraint that exactly k variables are true. It

achieves this by reducing the goal to a combination of results from two calls to your implementation

of at-most-k.

Problem 2 (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:

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

2

Input format The partially completed grid is provided to you with – standing for each blank cell to be

filled with a number, and * for blocked cells (that are not to be filled with a number). Each symbol two

symbols is 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 – – * *

Has the following solution, represented in the same format:

* * 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 * *

The function parsing the input grid is provided in q2.py.

Task

The goal of this problem is to use the SMT solver to produce a solution for any given instance of the puzzle.

You may use the theory of your choice to formulate a Hidato puzzle solver using Z3’s Python interface. You

will complete the function solve(grid) in q2.py such that the function answers:

Given a partially completed grid, is it possible to complete the grid obeying the rules of Hidato?

If the answer is no, then simply output None. If the answer is yes, then you need to output the completed

grid.

You are not allowed to use more variables for z3 (using Int() or Bool()) than there are cells on the grid.

Problem 3 (40 points)

The goal of this problem is to solve Hidato again, but this time without the power of SMT. For this instance,

we want to limit ourselves to a SAT solver only. The encoding will naturally be less high level and less

intuitive in this case.

The specification of the output is precisely the same as stated in Problem 2, but you will complete the

function solve(grid) in q3.py this time which only permits you to use Boolean variables.

Problem 2 vs Problem 3

You are asked to redo the same problem in two different encodings, precisely so that you get a sense how

different the solutions (encodings) can be. The constraints put in place in each case are there to make sure

that you do not recycle an idea from one solution to the other, but rather rethink and resolve the problem

given the context.

In class, we discussed how a computation model can be built around a SAT/SMT oracle. In both instances

of Hidato, your wrapper code should have polynomial time complexity on the input size to produce the

encoding (which itself should also be polynomial on the input size). Considering that Hidato is known to be

NP-Complete, this effectively forces you to use the solver properly since any algorithmic solution to Hidato

without the SAT/SMT oracle must have super-polynomial complexity.

3