首先，最好注意等价性和等可满足性之间的区别。一般来说，将任意布尔公式（例如 DNF 中的某些公式）转换为 CNF 可能会导致大小呈指数级增长。
这次爆炸是你的问题from_dnf方法：每当你处理另一个产品术语时，each该产品中的文字需要当前 cnf 子句集的新副本（它将在每个子句中添加自己）。如果您有 n 个大小为 k 的乘积项，则增长为O(k^n).
在你的情况下n实际上是一个函数k!。保留为乘积项的内容将被过滤为满足视图约束的内容，但总体而言，程序的运行时间大致在O(k^f(k!))。即使 f 按对数增长，这仍然是O(k^(k lg k))而且不太理想！
因为你问“这是可以满足的吗？”，所以你不需要相等的公式但仅仅是一个可同等满足的一。这是一些新公式，当且仅当原始公式是可满足的时，它是可满足的，但相同的分配可能无法满足该公式。
例如，(a ∨ b) and (a ∨ c) ∧ (¬b)显然每个都是可满足的，因此它们是可等满足的。但设置btrue 满足第一个，而 false 满足第二个，因此它们不等价。此外，第一个甚至没有c作为一个变量，再次使其不等于第二个。
这种放松足以用linear大小的翻译代替。
关键的想法是使用扩展变量。这些是新变量（即，公式中尚未存在），允许我们缩写表达式，因此我们最终不会在翻译中制作它们的多个副本。由于新变量不存在于原始变量中，因此我们将不再有等效的公式；但因为当且仅当表达式为真时变量才为真，所以它是可等满足的。
如果我们想使用x作为缩写y，我们会说x ≡ y。这与x → y and y → x，这与(¬x ∨ y) ∧ (¬y ∨ x)，它已经存在于 CNF 中。
考虑产品术语的缩写：x ≡ (a ∧ b)。这是x → (a ∧ b) and (a ∧ b) → x，它由三个子句组成：(¬x ∨ a) ∧ (¬x ∨ b) ∧ (¬a ∨ ¬b ∨ x)。一般来说，将 k 个文字的乘积项缩写为x将产生 k 个二元子句，表示x意味着它们中的每一个，并且一个(k+1)- 子句表示它们一起意味着x。这是线性的k.
要真正了解为什么这有帮助，请尝试转换(a ∧ b ∧ c) ∨ (d ∧ e ∧ f) ∨ (g ∧ h ∧ i)到第一个乘积项具有或不具有扩展变量的等效 CNF。当然，我们不会仅仅停留在一个术语上：如果我们缩写每个术语，那么结果恰好是一个 CNF 子句：(x ∨ y ∨ z)其中每个都缩写单个产品术语。这个小了很多！
这种方法可用于转动任何circuit转化为可等满足的公式，大小和 CNF 呈线性。这被称为切丁转化 https://en.wikipedia.org/wiki/Tseytin_transformation。您的 DNF 公式只是一个由一堆任意扇入与门组成的电路，所有输入都馈入单个任意扇入或门。
最重要的是，尽管由于附加变量，该公式并不等效，但我们可以通过简单地删除扩展变量来恢复原始公式的赋值。它是一种“最佳情况”可等满足公式，是原始公式的严格超集。
为了将其修补到您的代码中，我添加了：
# Uses pseudo-namespacing to avoid collisions.
_EXT_SUFFIX = "___"
_NEXT_EXT_INDEX = 0
def is_ext_var(element) -> bool:
return element.endswith(_EXT_SUFFIX)
def ext_var() -> str:
global _NEXT_EXT_INDEX
ext_index = _NEXT_EXT_INDEX
_NEXT_EXT_INDEX += 1
return intern(f"{ext_index}{_EXT_SUFFIX}")
这让我们可以凭空提取一个新的命名变量。由于这些扩展变量名称对您的解决方案显示函数没有有意义的语义，因此我更改了：
point_to_value = {
point: value for point, value in [fact.split() for fact in self.solution]
}
into:
point_to_value = {
point: value
for point, value in [
fact.split() for fact in self.solution if not is_ext_var(fact)
]
}
当然有更好的方法可以做到这一点，这只是一个补丁。 :)
重新实现你的from_dnf有了上面的想法，我们得到：
def from_dnf(groups) -> "cnf":
"Convert from or-of-ands to and-of-ors, equisatisfiably"
cnf = []
extension_vars = []
for group in groups:
extension_var = ext_var()
neg_extension_var = neg(extension_var)
imply_ext_clause = []
for literal in group:
imply_ext_clause.append(neg(literal))
cnf.append((neg_extension_var, literal))
imply_ext_clause.append(extension_var)
cnf.append(tuple(imply_ext_clause))
extension_vars.append(extension_var)
cnf.append(tuple(extension_vars))
return cnf
每个组都有一个扩展变量。组中的每个文字都将其否定添加到(k+1)- 大小的蕴含子句，并由扩展隐含。处理文字后，扩展变量完成剩余的含义并将其自身添加到新扩展变量的列表中。最后，这些扩展变量中至少有一个必须为 true。
仅此一项更改就让我立即解决了这个 5x5 难题：
self.visible_from_top = [3, 2, 1, 4, 2]
self.visible_from_bottom = [2, 2, 4, 1, 2]
self.visible_from_left = [3, 2, 3, 1, 3]
self.visible_from_right = [2, 2, 1, 3, 2]
self.given_numbers = {}
我还添加了一些计时输出：
@property
def solution(self):
if self._solution is None:
start_time = time.perf_counter()
cnf = self.cnf
cnf_time = time.perf_counter()
print(f"CNF: {cnf_time - start_time}s")
self._solution = solve_one(cnf)
end_time = time.perf_counter()
print(f"Solve: {end_time - cnf_time}s")
return self._solution
5x5 拼图给了我：
CNF: 0.00565183162689209s
Solve: 0.005589433014392853s
然而，我们仍然有那个讨厌的k!枚举可行的塔高度排列时的增长。
我生成了9x9 拼图 https://www.chiark.greenend.org.uk/%7Esgtatham/puzzles/js/towers.html#9:3/3/3/3/1/4/2/4/2/3/1/4/2/5/3/3/2/3/3/3/1/2/4/5/2/3/2/3/1/7/4/3/3/2/2/4,a5a4h3_2g7a5_1c1e7a4g2_2c8j7a6_3d2a1g6b（站点允许的最大），对应于：
self.visible_from_top = [3, 3, 3, 3, 1, 4, 2, 4, 2]
self.visible_from_bottom = [3, 1, 4, 2, 5, 3, 3, 2, 3]
self.visible_from_left = [3, 3, 1, 2, 4, 5, 2, 3, 2]
self.visible_from_right = [3, 1, 7, 4, 3, 3, 2, 2, 4]
self.given_numbers = {
"AB": 5,
"AD": 4,
"BD": 3,
"BE": 2,
"CD": 7,
"CF": 5,
"CG": 1,
"DB": 1,
"DH": 7,
"EA": 4,
"EI": 2,
"FA": 2,
"FE": 8,
"GG": 7,
"GI": 6,
"HA": 3,
"HF": 2,
"HH": 1,
"IG": 6,
}
这给了我：
CNF: 28.505195066332817s
Solve: 40.48229135945439s
我们应该花更多的时间解决问题，减少生成的时间，但接近一半的时间都在生成。
在我看来，在 CNF-SAT 翻译中使用 DNF 通常是错误方法的标志。求解器比我们更善于探索和了解解空间——花费阶乘时间进行预探索实际上比求解器的指数最坏情况更糟糕。
“回退”到 DNF 是可以理解的，因为程序员自然会考虑“编写一个能够给出解决方案的算法”。但当您将其编码到问题中。让求解器推理解决方案变得不可行的条件。为此，我们需要从电路的角度进行思考。幸运的是，我们还知道如何快速将电路转变为 CNF。
†I said "often"; if your DNF is small and quick to produce (like a single circuit gate), or if encoding it to a circuit is prohibitively complicated, then it can be helpful to pre-compute some of the solution space.
实际上你已经做了一些这样的事情！例如，我们需要一个电路来计算某个数字在一个范围（行或列）中出现的次数，并断言该数字恰好是一。然后对于每个跨度和每个数字，我们将发出这个电路。这样，如果一座塔的尺寸例如3 连续出现两次，该行 3 的计数器将发出“2”，并且我们关于其为“1”的断言将不会得到支持。
Your one_of约束是一种可能 https://www.semanticscholar.org/paper/SAT-Encodings-of-the-At-Most-k-Constraint-Some-Old-Frisch-Giannaros/69836f0bc61620368e76c7f0bd19f6ad7315a00a的实施。您使用“明显”的成对编码：对于跨度中的每个位置，如果 N 出现在该位置，那么它不会出现在任何其他位置。这实际上是一个非常好的编码，因为它几乎完全由二进制子句组成，并且 SAT 求解器喜欢二进制子句（它们使用的内存显着减少并且经常传播）。但对于真正需要计算的大量事物来说，这O(n^2)缩放可能会成为一个问题。
您可以想象一种替代方法，您可以从字面上编码加法器电路 https://en.wikipedia.org/wiki/Adder_(electronics)：每个位置都是电路的一个输入位，电路产生 n 位输出，告诉您最终的总和（上面的论文值得一读！）。然后，您可以使用强制特定输出位的单位子句断言该总和恰好为一。
仅对电路进行编码以强制其某些输出为恒定值似乎是多余的。然而，这更容易推理，并且现代求解器意识到编码可以做到这一点并对其进行优化。它们执行的处理过程比初始编码过程合理得多。使用求解器的“艺术”在于了解和测试这些替代编码何时比其他编码更有效。
注意exactly_k_of is at_least_k_of随着at_most_k_of。您已经在您的Q class ==执行。实施at_least_1_of是微不足道的，是一个子句；at_most_1_of很常见，通常被称为AMO。我鼓励你尝试实施< and >在本文中讨论的其他一些方法（甚至可能根据输入大小选择使用哪种方法）来感受它。
将我们的注意力转回到k!可见性约束，我们需要的是一个电路，告诉我们从某个方向可以看到多少座塔，然后我们可以断言它是一个特定值。
停下来想一想如何做到这一点，这并不容易！
类似于各种one_of方法，我们可以使用“纯”电路进行计数，或者使用更简单但缩放比例更差的成对方法。我在这个答案的最底部（‡）附上了纯电路方法的草图。现在我们将使用成对方法。
主要观察是，在不可见的塔中，我们不关心它们的排列。考虑：
3 -> 1 5 _ _ _ 9 _ _ _
A B C D E F G H I
只要 CDE 组包含，我们就会从左边看到 3 座塔2, 3, and 4，同样如果 GHI 组包含6, 7, and 8。但它们在组中出现的顺序对可见的塔没有任何影响。
我们不会计算哪些塔是可见的，而是声明哪些塔是可见的并遵循它们的含义。我们将填写这个函数：
def visible_in_span(points: Collection[str], desired: int) -> "cnf":
"""Assert desired visible towers in span. Wlog, visibility is from index 0."""
points = list(points)
n = len(points)
assert desired <= n
cnf = []
# ...
return cnf
假设固定的跨度和观察方向：每个位置将有 k 个关联变量，Av1通过Avk说明“这是第 k 个可见的塔”。我们还将有Av ≡ (Av1 ∨ Av2 ∨ ⋯ ∨ Avk)意思是“A 有一座可见的塔”。
在上面的例子中，Av1, Bv2, and Fv3都是真的。排放有一些明显的含义。在某个位置，最多其中一个是正确的（你不能同时是第一个和第二个可见的塔）——但不是exactly一，因为拥有一座不可见的塔是完全可以的。另一个是，如果一个位置是第 k 个可见塔，则没有其他位置也是第 k 个可见塔。
到目前为止我们可以添加这个：
is_kth_visible_tower_at = {}
is_kth_visible_tower_vars = collections.defaultdict(list)
is_visible_tower_at = {}
for point in points:
is_visible_tower_vars = []
for k in range(1, n + 1):
# Xvk
is_kth_visible_tower_var = ext_var()
is_kth_visible_tower_at[(point, k)] = is_kth_visible_tower_var
is_kth_visible_tower_vars[k].append(is_kth_visible_tower_var)
is_visible_tower_vars.append(is_kth_visible_tower_var)
# Xv
is_visible_tower_at_var = ext_var()
# Xv → (Xv1 ∨ Xv2 ∨ ⋯)
cnf.append(tuple([neg(is_visible_tower_at_var)] + is_visible_tower_vars))
# (Xv1 ∨ Xv2 ∨ ⋯) → Xv
for is_visible_tower_var in is_visible_tower_vars:
cnf.append((neg(is_visible_tower_var), is_visible_tower_at_var))
is_visible_tower_at[point] = is_visible_tower_at_var
# At most one visible tower here.
cnf += Q(is_visible_tower_vars) <= 1
# At most one kth visible tower anywhere.
for k in range(1, n + 1):
cnf += Q(is_kth_visible_tower_vars[k]) <= 1
接下来，我们需要对可见塔进行排序，以便第 k + 1 个可见塔位于第 k 个可见塔之后。这是通过第 k + 1 个可见塔迫使至少一个先前位置成为第 k 个可见塔来实现的。例如。，Dv3 → (Av2 ∨ Bv2 ∨ Cv2) and Cv2 → (Av1 ∨ Bv1)。我们知道Av1始终为真，这提供了基本情况。 （如果我们进入需要 B 成为第三个可见塔的情况，则需要 A 成为第二个可见塔，这与Av1.)
# Towers are ordered.
for index, point in enumerate(points):
if index == 0:
cnf += basic_fact(is_kth_visible_tower_at[(point, 1)])
continue
for k in range(1, n + 1):
# Xvk → ⋯
implication = [neg(is_kth_visible_tower_at[(point, k)])]
j = k - 1
if j > 0:
for index_j, point_j in enumerate(points):
if index_j == index:
break
# ⋯ ∨ Wxj ∨ ⋯
implication.append(is_kth_visible_tower_at[(point_j, j)])
cnf.append(tuple(implication))
到目前为止一切顺利，但我们还没有将塔的高度与能见度联系起来。上述将允许9 8 7作为解决方案，调用9第一个可见的塔，8第二个，和7第三。为了解决这个问题，我们希望塔的放置能够防止较小的塔也可见。
每个位置将再次收到一组缩写，指示它是否被遮挡在一定高度以下，称为Ao1, Ao2， 等等。这将为我们提供一个“网格”，让事情变得更简单。首先，较高的塔被遮挡意味着同一位置的下一个最高的塔也被遮挡，因此Ao3 → Ao2 and Ao2 → Ao1。第二个是，如果一座塔在一个位置被遮挡，那么它在以后的所有位置也会被遮挡。这是Ao3 → Bo3 and Bo3 → Co3等等。
is_height_obscured_at = {}
is_height_obscured_previous = [None] * n
for point in points:
is_obscured_previous = None
for k in range(1, n + 1):
# Xok
is_height_obscured_var = ext_var()
# Wok → Xok
is_k_obscured_previous = is_height_obscured_previous[k - 1]
if is_k_obscured_previous is not None:
cnf.append((neg(is_k_obscured_previous), is_height_obscured_var))
# Xok → Xo(k-1)
if is_obscured_previous is not None:
cnf.append((neg(is_height_obscured_var), is_obscured_previous))
is_height_obscured_at[(point, k)] = is_height_obscured_var
is_height_obscured_previous[k - 1] = is_height_obscured_var
is_obscured_previous = is_height_obscured_var
由此很容易看出，例如Bo4意味着其余高度等于或小于 4 的塔都被遮挡了。我们现在可以轻松地将塔的放置与默默无闻联系起来：A5 → Bo4.
# A placed tower obscures smaller later towers.
for index, point in enumerate(points):
if index + 1 == len(points):
break
next_point = points[index + 1]
for k in range(2, n + 1):
j = k - 1
# Xk → Yo(k-1)
cnf.append((neg(comb(point, k)), is_height_obscured_at[(next_point, j)]))
最后，我们需要将模糊性与可见性联系起来。我们需要最后一组缩写，说明specific塔的高度在某个位置可见。冒着容易出现拼写错误的风险，我们将其称为Ahv对于一定高度h， 以便Ahv ≡ (Ah ∧ Av)。一个具体的例子是C3v ≡ (C3 ∧ Cv)：当且仅当在 C 处有一座可见的塔时，高度为 3 的塔在 C 处可见，并且该塔是高度为 3 的塔。
is_height_visible_at = {}
for point in points:
for k in range(1, n + 1):
# Xhv
height_visible_at_var = ext_var()
# Xhv ≡ (Xh ∧ Xv)
cnf.append((neg(height_visible_at_var), comb(point, k)))
cnf.append((neg(height_visible_at_var), is_visible_tower_at[point]))
cnf.append(
(
neg(comb(point, k)),
neg(is_visible_tower_at[point]),
height_visible_at_var,
)
)
is_height_visible_at[(point, k)] = height_visible_at_var
这使我们能够得出对塔放置的最终影响。如果高度为 h 的塔被遮挡，则它是不可见的：Bo4 → ¬B4v。这是not等价，我们不能对待Bo4 ≡ ¬B4v; maybe ¬B4v成立，因为B4只是没有放置在那里（但它是可见的！）。
for point in points:
for k in range(1, n + 1):
# Xok → ¬Xkv
cnf.append(
(
neg(is_height_obscured_at[(point, k)]),
neg(is_height_visible_at[(point, k)]),
)
)
为了将其与特定谜题的可见性值联系起来，我们只需要禁止太多可见塔并确保所需的计数至少可见一个（因此恰好一次）：
# At least one of the towers is the desired kth visible.
cnf.append(tuple(is_kth_visible_tower_vars[desired]))
# None of the towers can be visible above the desired kth.
if desired < n:
for is_kth_visible_tower_var in is_kth_visible_tower_vars[desired + 1]:
cnf += basic_fact(neg(is_kth_visible_tower_var))
return cnf
我们只需要阻挡第一层不需要的第k个可见塔。由于第 k + 1 层意味着存在第 k 层可见塔，因此它也被排除。 （等等。）
最后，我们将其挂接到 CNF 构建器中：
# Set visible from left
if self.visible_from_left:
for index, row in enumerate(self.rows):
target_visible = self.visible_from_left[index]
if not target_visible:
continue
cnf += visible_in_span(row, target_visible)
# Set visible from right
if self.visible_from_right:
for index, row in enumerate(self.rows):
target_visible = self.visible_from_right[index]
if not target_visible:
continue
cnf += visible_in_span(reversed(row), target_visible)
# Set visible from top
if self.visible_from_top:
for index, col in enumerate(self.cols):
target_visible = self.visible_from_top[index]
if not target_visible:
continue
cnf += visible_in_span(col, target_visible)
# Set visible from bottom
if self.visible_from_bottom:
for index, col in enumerate(self.cols):
target_visible = self.visible_from_bottom[index]
if not target_visible:
continue
cnf += visible_in_span(reversed(col), target_visible)
以上给了我更快的 9x9 解决方案：
CNF: 0.028973951935768127s
Solve: 0.07169117406010628s
速度提高了约 685 倍，并且求解器承担了更多的整体工作。又快又脏还不错！
有很多方法可以清理这个问题。例如，我们看到的每个地方cnf.append((neg(a), b))可能cnf += implies(a, b)而不是为了可读性。我们可以避免分配无意义的大 kth 可见变量，等等。
这还没有经过充分测试；我可能错过了一些含义或规则。希望此时很容易修复。
我想谈的最后一件事是 SAT 的适用性。也许现在很痛苦地清楚了，SAT 求解器并不擅长计数和算术。你必须降低到一个电路，从求解过程中隐藏更高级别的语义。
其他方法可以让你自然地表达算术、区间、集合等。答案集编程 (ASP) 就是一个例子，SMT 求解器是另一个例子。对于小问题，SAT 没问题，但对于困难问题，这些更高级别的方法可以大大简化问题。
他们中的每一个实际上可能在内部决定通过 SAT 解决（特别是 SMT）进行推理，但他们将在对问题的一些更高层次的理解的背景下这样做。
‡ 这是计数塔的纯电路方法。
它是否比pairwise更好取决于所计算的塔的数量；也许常数因子太高而没有用处，或者即使在小尺寸下它也非常有用。老实说，我不知道——我以前编码过巨大的电路并且让它们工作得很好。需要实验才能知道。
我去打电话Ah位置 A 中塔的整数高度。也就是说，而不是任一的 one-hot 编码A1 or A2或……或A9我们会有Ah0, Ah1， …， 和Ahn作为 n 位整数的低位到高位（统称为Ah）。对于 9x9 的限制，4 位就足够了。我们还会有Bh, Ch， 等等。
您可以使用连接两个表示A1 ≡ (¬Ah3 ∧ ¬Ah2 ∧ ¬Ah1 ∧ Ah0) and A2 ≡ (¬Ah3 ∧ ¬Ah2 ∧ Ah1 ∧ ¬Ah0) and A3 ≡ (¬Ah3 ∧ ¬Ah2 ∧ Ah1 ∧ Ah0)等等。我们有Ah = 3当且仅当A3已设置。 （我们不需要添加只有一个值的约束Ah一次是可能的，因为与每个变量关联的独热变量已经这样做了。）
有了整数在手，可能会更容易了解如何计算可见性。我们可以将每个位置与最大可见塔高度相关联，名为Am, Bm， 等等;显然第一座塔总是可见的并且是最高的，所以Am ≡ Ah。再说一遍，这实际上是一个 n 位值Am0通过Amn.
当且仅当塔的值大于先验的最高值时，塔才可见。我们将跟踪可见性Av, Bv， 等等。这可以通过数字比较器 https://en.wikipedia.org/wiki/Digital_comparator;以便Bv ≡ Bh > Am. (Av是一个基本情况，并且总是正确的。）
这让我们也可以填写其余的最大值。Bm ≡ Bv ? Bh : Am， 等等。条件/if-then-else/ite 是数字多路复用器。对于简单的 2 对 1，这很简单：Bv ? Bh : Am is (Bv ∧ Bh) ∨ (¬Bv ∧ Am)，这确实是(Bv ∧ Bhi) ∨ (¬Bv ∧ Ami)对于每个i ∈ 0..n.
然后，我们将有一堆单一输入Av通过Iv馈入加法器电路，告诉我们其中有多少输入是真实的（即有多少塔是可见的）。这将是另一个 n 位值；然后我们使用单元子句来断言它正是例如3，如果特定谜题需要 3 个可见的塔。
我们为每个方向的每个跨度生成相同的电路。这将是一些多项式大小的规则编码，添加许多扩展变量和许多子句。求解器可以了解到某个塔的放置是不可行的，不是因为我们这么说的，而是因为它意味着一些不可接受的中间可见性。 “应该有 4 个可见，而 2 个已经可见，所以剩下的就是……”。
