1

在 SAT4J 文档中的代码示例中，对同一个 SAT 问题多次调用求解器总是产生相同的解决方案，即使存在多个可能的解决方案 - 也就是说，结果是确定性的。

我正在寻找一种在多次运行中获得不同解决方案的方法，即非确定性/随机结果。对于每个可能的解决方案，选择该解决方案的概率应该是非零的。理想情况下，应该以相同的概率选择每个解决方案，但这不是严格的要求。

我知道（确定性地）迭代所有解决方案并随机选择一个解决方案的可能性，但在我的情况下这不是一个可行的解决方案，因为有太多的解决方案要开始，并且计算它们都需要很长时间。

4

1 回答 1

1

是的，Sat4j 默认是确定性的：如果您从命令行对同一个问题多次运行它，它总能找到相同的解决方案。

在启发式中添加一些非确定性的方法是使用 RandomWalkDecorator，例如在 org.sat4j.minisat.SolverFactory 中的 GreedySolver 中。

但是请注意，如果您从命令行多次使用此类求解器：

java -jar org.sat4j.core.jar GreedySolver file.cnf

你仍然是确定性的，因为伪随机数生成器是由一个常数播种的。

因此，您需要在 Java 代码中询问多个模型。

正如你的问题中提到的，你可以使用一个 ModelIterator 装饰器，它有一个界限：

ISolver solver = SolverFactory.newGreedySolver();
ModelIterator mi = new ModelIterator(solver,10); // look for 10 models
于 2020-07-16T05:32:00.327 回答