$2$ Use Z$3$ to find a solution

We are going to reduce your puzzle to a satisfiability problem and solve it using Z$3.$ Basically,

our existential claim will be $$This puzzle is solvable$,$ and then the $$model$$ that Z$3$ produces

to prove the claim will be the solution to the puzzle. To do this, we need to represent the

puzzle as a set of variables and constraints.

The specific steps below are just one suggested way of accomplishing this task; feel free to

do it differently $($especially if you aren$$t creating a Ciphered Skyscrapers$)$ as long as you end

up with an appropriate artifact to turn in $($see end of the section$).$ I recommend frequently

checking your work in progress by using the check$-$sat and get$-$model commands. For

example, after the first step below, Z$3$ can already tell you that your puzzle is solvable

$($sat$)$ and give you a model $$solution$,$ though since you haven$$t added any constraints yet

that solution will be something silly like putting a $0$ into every square.

$1.$ Create variables representing all the things that the solver must determine: one variable for each square in the grid $($it$$s probably best to also include squares that already have a clue written in them, even though there$$s nothing further for the solver to determine$),$ and one variable for each letter used by your cipher. $($You can use whatever variable scheme you want, but if you are using row$/$column indices anyway and your representation makes the following convenient, please follow standard puzzle convention where row index comes before col index and $(1,1)$ is the upper$-$left corner of the grid. So e$.$g$.$ the variable for the lower$-$left corner might be something like x$31.)$

$2.$ Add constraints representing the rules that must be followed even if the grid has no clues given in it $($for example, in each row all squares must have distinct values$).$

$3.$ Write a function named clue which takes in three numbers $($representing the contents of a row or column$),$ and returns the appropriate Skyscrapers clue for that row$/$column$.$For example, $($clue $213)$ should return $2.$

$4.$ Using your clue function when needed, add constraints for each clue given in your puzzle. If you haven$$t actually constructed a puzzle yet, this is one place you can get Z$3$ to help you do so: experiment with adding clues and their corresponding constraints one at a time, and for each one, run Z$3$ to make sure that your new version of the puzzle still has a solution.

$3$ Use Z$3$ to confirm your solution is unique

Your goal now is to add one additional assert statement representing $$the solution is not the

same as the solution found in part $2.($This will be a very large constraint $-$ tedious to write

by hand, but fast if you use take the model output by part $2$ and edit it using find$/$replace$.)$

Assuming your puzzle actually has only one solution, Z$3$ should now respond with $$unsat$$

since there does not exist a solution which meets all your part$-2$ constraints while also being

distinct from your part$-2$ solution. If your puzzle does have multiple solutions, you need to

go back to earlier stages and add more clues $($constraints$)$ to your puzzle until all but one of

the solutions becomes invalid $($and Z$3$s output will help you do this, since it will provide you

with concrete alternate solutions you may not have thought of$).$ Hint: make sure that your

new constraint disallows only the one solution from part $2,$ rather than encoding a stricter

criterion like $$the solution doesn$$t have even one square in common with the solution found

in part $2.$ There may not be an easy way to check if you did this right, since disallowing a

larger set of solutions would also result in an $$unsat$$ output.