A way of reduction skyscrapper (latin square with height clues) to SAT

Question

I'm trying to implement a reduction from the skyscrapper latin-square problem to SAT.

The skyscrapper problem is the same of Latin-sqaure but in addition, the skyscraper puzzle asks the player to place buildings of varying & unique heights on a grid so as to satisfy clues given on the grid’s edges. These “edge clues” tell the player how many buildings are visible from the standpoint of a given clue’s placement along the board’s edge. (full explanation)

So in order to solve this problem using SAT solver, I tried a similar approach of solving a suduko using SAT (which I already did). So first off all I defined n^3 binary variables, X_i,j,k which indicates that in the i,j cell the value k is true (so in the i,j cell we have a skyscrapper with a height of k)

I added the following constarints in the form of a CNF:

1. each cell contains only 1 true var
2. each row contains exactly 1 of each value
3. each column contains exacly 1 of each value

Now I'm having troubles figuring out which constraints should I add for the clues and the heights. First I thought about the option of adding every possible order for each clue given, for example If from the left I can see 3 skyscrappers ( n = 4) so the possibilities are: [[2 ,3 ,4, 1],[1,3,4,2]] but I think it would be O(n!) in total...

I implemnted Suduko solver using ILP so I read about solving this problem usin ILP (integer linear programming). I found this link which describes how to do that. But still I can't find the equivalent for the height constarint they added in the ILP situation that will fit in the SAT solver.

Thanks a lot!

Answer 1

There are probably many many approaches, but one that comes to mind can look like the following.

For each clue C_i, you introduce new helper variables:

# NV_?_j = position j is not visible (in regards to clue i)

NV_i_1, NV_i_2, ... NV_i_n  

A clue than consists in posting the correct cardinality (different approaches; you chose how)

sum(NV_1_?) = clue-hint(C_1)

Now the question is how to constrain NV:

• NV_i_1 = true is always valid
• NV_i_j = true <-> there exists a HIGHER value EARLIER

It's growing fast, but i recommend the following approach (which should be no problem for those sizes i saw in your linked pages; although SAT is a less natural approach here than CP for example):

For N=5, constrained by your all-diff constraint, there are C(N, 2) = 10 symmetry-free unique pairs:

1 2    2 3    3 4    4 5
1 3    2 4    3 5
1 4    2 5  
1 5

You will now use these pairs in regards to:

• pairwise positions (1 - N)
• pairwise values (1 - N)

Assuming, your decision-variables are that of some tensor of rank 3 (row position, column position, value in unary encoding) with dimensions (N, N, N):

X111 = row = 1 | column = 1 | value = 1
X112 = row = 1 | column = 1 | value = 2
...
X121 = row = 1 | column = 2 | value = 1
... 

NV_i_j = true <-> there exists a HIGHER value EARLIER can be expressed as (we assume a clue active on some column here):

NV_i_1 <-> true  # fact

# pairs compared: position 1 2
NV_i_2 <-> (X115 ^ X124) | (X115 ^ X123) | ...  | (x112 ^ X121)

# pairs compared: position 1 3 + position 2 3
# 3 compared to 1 and 2 -> existence of HIGHER value EARLIER (2 positions)
NV_i_3 <-> (X115 ^ X134) | (X115 ^ X133) | ...  | (x112 ^ X131) |
           (X125 ^ X134) | (X125 ^ X133) | ...  | (x122 ^ X131) 

...

# pairs compared: position 1 5 + position 2 5 + position 3 5 + position 4 5 
NV_i_5 <-> (X115 ^ X154) | (X115 ^ X153) | ...  | (x112 ^ X151) |
           (X125 ^ X154) | (X125 ^ X153) | ...  | (x122 ^ X151)
           ...
           (X145 ^ X154) | (X145 ^ X153) | ...  | (x142 ^ X151)

Now there is only one thing left (and i won't show it):

• converting these components to cnf
  • you already did some cardinality-encoding for your all-diff decomposition
    • can be reused for the cardinality needed for the clues
  • for the NV constraints:
    • i recommend using external tools (sympy, mathematica, ...) instead of doing it manually
    • i also recommend outsourcing this into some function which is feeded by something like a sub-matrix of your tensor (tensor where the row or column, where clue is active, is chipped away) + clue_n