0

我正在尝试将摩天大楼拉丁方问题减少到 SAT。

摩天大楼问题与拉丁广场相同，但此外，摩天大楼难题要求玩家将不同高度的建筑物放置在网格上，以满足网格边缘给出的线索。这些“边缘线索”告诉玩家从给定线索沿棋盘边缘的位置可以看到多少建筑物。（完整解释）

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

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

  1. 每个单元格仅包含 1 个真正的 var
  2. 每行恰好包含每个值的 1
  3. 每列包含每个值的恰好 1

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

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

非常感谢！

4

1 回答 1

0

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

对于每条线索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，受您的 all-diff 约束的约束，存在无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
    • 你已经为你的全差异分解 做了一些基数编码
      • 可重复用于线索所需的基数
    • 对于NV约束：
      • 我建议使用外部工具（sympy、mathematica、...）而不是手动操作
      • 我还建议将其外包给某个函数，该函数由诸如张量的子矩阵之类的东西提供（线索处于活动状态的行或列被切掉的张量）+clue_n
于 2020-04-10T12:27:16.140 回答