1

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

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

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

4

2 回答 2

2

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

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

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

于 2014-10-22T08:19:34.077 回答
1

命题逻辑中 8 个皇后问题的表述可以在安徒生出色的“二元决策图简介”（Lecture notes，TU Denmark，1997 ）中找到。

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

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

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

于 2015-06-08T01:22:42.263 回答