Description
CSC 410 Assignment 2
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
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
