一种减少摩天大楼（带有高度线索的拉丁方）到SAT的方法

Question

我正在尝试将 skyscrapper 拉丁方问题减少到 SAT。

摩天大楼问题与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)

相同

因此，为了使用 SAT 求解器解决这个问题，我尝试了一种使用 SAT 求解数独的类似方法（我已经这样做了）。所以首先我定义了 n^3 个二元变量 X_i,j,k 表示在 i,j 单元格中值 k 为真（所以在 i,j 单元格中我们有一个高度为 skyscrapper k)

我以 CNF 的形式添加了以下约束：

每个单元格仅包含 1 个真实变量
每行恰好包含每个值中的 1 个
每列恰好包含每个值中的 1 个

现在我很难弄清楚应该为线索和高度添加哪些约束。首先，我考虑了为每个给定的线索添加每个可能顺序的选项，例如，如果从左边我可以看到 3 个摩天大楼（n = 4），那么可能性是： [[2 ,3 ,4, 1],[1,3,4,2]] 但我认为总共是 O(n!)...

我使用 ILP 实现了数独求解器，所以我阅读了有关使用 ILP（整数线性规划）解决此问题的信息。我发现 this link 描述了如何做到这一点。但是我仍然找不到他们在 ILP 情况下添加的适合 SAT 求解器的高度约束的等价物。

非常感谢！

Answer 1

可能有很多方法，但我想到的可能如下所示。

对于每条线索C_i，你引入新的辅助变量：

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

NV_i_1, NV_i_2, ... NV_i_n

一条线索在于发布正确的基数（不同的方法；您选择如何）

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

现在的问题是如何约束NV:

NV_i_1 = true 始终有效
NV_i_j = true <-> there exists a HIGHER value EARLIER

它增长很快，但我推荐以下方法（对于我在您的链接页面中看到的那些尺寸应该没有问题；虽然 SAT 在这里比 CP 更不自然）：

对于 N=5，受限于你的全差约束，有 C(N, 2) = 10 个无对称唯一对：

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

您现在将在以下方面使用这些对：

成对位置 (1 - N)
成对值 (1 - N)

假设您的决策变量是维度为 (N, N, N) 的 3 阶张量（行位置、列位置、一元编码中的值）的决策变量：

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 可以表示为（我们假设一条线索在某些列此处处于活动状态）：

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)

现在只剩下一件事了（我不会展示它）：

将这些组件转换为 cnf
- 您已经为 all-diff 分解做了一些基数编码
  - 可以重复使用线索所需的基数
- 对于 NV 约束：
  - 我建议使用外部工具（sympy、mathematica 等）而不是手动操作
  - 我还建议将其外包到某个函数中，该函数由张量的子矩阵之类的东西提供（张量中的行或列，线索处于活动状态，被削掉）+ clue_n

一种减少摩天大楼（带有高度线索的拉丁方）到SAT的方法

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

algorithm

reduction

sat

latin-square