8 皇后拼图与降序二元决策图

Question

我不知道如何用归约二元决策图 (ROBDD) 解决 8 皇后难题。我用谷歌搜索了它，但找不到问题的良好解释。 所以，这里的问题—— 到目前为止，我已经发现 ROBDD 会有 n*n 个输入变量或状态。现在，我如何才能真正创建一个能够解决 8 皇后谜题的 ROBDD？

1. ROBDD 是如何解决这个问题的？
2. 我无法弄清楚上述问题的图形表示
3. 它实际上是如何产生最小节点数的？
4. 输入变量的顺序如何？
5. 如何减少？

解释将帮助我更好地理解问题。

Answer 1

你的问题有点误导。 ROBDD 只是表示和操作布尔函数的一种手段。因此，首先，您必须处理代表问题的布尔函数。关于n-queen问题的材料很多，所以我不会在这个答案中解释。

一旦你有了你的函数，你就可以在 ROBDD 上表示它。每个节点可能会回答“这个方格中有女王？是的，没有”。关于reduce和reordering，与问题本身没有直接关系。 Reduce 是一种标准算法，有很多不同的算法和启发式算法用于重新排序（例如 CUDD 包提供了十几种）。同样，详细解释这些事情不是这个答案的范围，而且互联网上有大量的材料可供研究。但是，我可以说 reduce 算法将保留所有变量，因为您几乎不会遇到在正方形上有或没有皇后是相同的情况。

现在是时候寻找解决方案了。如果问题确实有解决方案，您会发现至少有一条通往 1 的路径。沿着那条路径（或那些路径，可能不止一条），您可以分辨出哪些变量设置为 1 或 0（也就是说，皇后在哪里，哪里不在）。

Answer 2

命题逻辑中8皇后问题的表述可以在安徒生的优秀“An introduction to binary decision diagrams”, Lecture notes, TU Denmark, 1997中找到。

我建议自己先编写这样一个布尔公式，然后检查该文本以纠正任何错误，然后从中学习。

至于问题列表：阅读安徒生的介绍将回答Q2-5。这些是关于 BDD 如何工作的问题，而不是关于具体问题的问题。

Q1：如果问题是要决定可满足性（也许还要列举解决方案），那么解决问题的是简化 BDD 的构造。通过变量排序引起的表示的规范性，得到的 BDD 表示一组令人满意的分配。该集合为空，当且仅当 BDD 是终端节点“False”。