minisat 随机变量选择不适用于 gcloud答案

【问题标题】：minisat randomize variable selection is not working on gcloudminisat 随机变量选择不适用于 gcloud
【发布时间】：2018-06-08 19:56:21
【问题描述】：

每次我在同一个问题上运行 minisat 时，我都想得到不同的解决方案。我可以通过使用 minisat 的“rnd-seed”参数来做到这一点。它只是随机化变量选择，所以每次我都能得到不同的解决方案。即使此参数在我的机器（Ubuntu16）上完美运行，它也不适用于在 Ubuntu 机器上运行的 gcloud（谷歌云）。

我想我遗漏了一小部分，但我不知道那是什么。

注意：我不想将解决方案的谈判提供给 minisat 以获得不同的解决方案。我实际上需要随机化变量选择。

编辑：让我解释一下为什么我需要随机解决方案。我解决了很多 SAT 问题，通常这些 SAT 问题看起来很像。所以，如果我不能随机变量选择，我大部分时间都会得到非常相似的解决方案，这是我不想要的。因此，我实际上并没有在同样的问题上运行 minisat。

Edit-2：@sascha 想让我解释一下“有效”和“无效”的含义。当我在我的电脑上运行一个 cnf 文件时，每次我得到不同的解决方案。但是，当我在 gcloud 机器上运行相同的 cnf 文件时，我总是得到相同的解决方案。

【问题讨论】：

这种方法可能根本无法保证。你真的确定这也是要走的路吗？
我也愿意接受其他建议。我需要做的就是得到一个不同的解决方案。但是不同的解决方案必须是完全随机的。我总是在我的机器和其他几台服务器上使用这种方法。它总是有效的。
如果完全随机化意味着：均匀采样，你就走错了路（它不会那样工作！）。你会发现一些（可能是可怕的）信息here。
是的，我能理解。完全随机化是可怕的 :) 我用错了词。让我纠正一下自己。我只需要使用基本随机化技术随机化变量选择，而不是加密随机化。
你似乎不明白我在说什么。您对 SAT 求解器、算法、NP 硬度等了解多少？你的工作有多科学？你所做的，好吧，它会在很多问题上失败。但直到现在，甚至还没有一个真正的规范：统一采样，这是人们有时试图实现的一件事，与 PRNG 与 cryptoPRNG 无关。 (CDCL) SAT-solvers 是启发式的并且有很大的偏差。变量选择并没有改变这一切（但有时它看起来像那样；当然很大程度上取决于问题）。阅读我的链接中提到的论文并准确！

标签： gcloud constraint-programming sat sat-solvers

【解决方案1】：

选项 -rnd-seed 不会随机选择分支变量。相反，它允许您为 Minisat 使用的伪随机数生成器设置种子。

除非使用 -rnd-freq 选项，否则分支的变量选择不涉及随机性。传入一个介于 0 和 1 之间的浮点值。0 表示没有随机性，1 表示尝试在每个分支中使用随机变量。该代码仅尝试随机选择一个变量，大概是因为在任意大的优先级队列中搜索未设置的变量会变得非常昂贵。如果该尝试失败，Minisat 将使用正常的优先级队列进行分支。

【讨论】：

由于某种原因，我无法访问我的 gcloud 帐户。一旦我再次连接，我会尝试让你知道结果。