如何在SAT4J中随机地(不确定地)找到解？

Question

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

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

我知道有可能(确定地)使用iterate over solutions，而只取一个随机的解决方案，但在我的情况下，这不是一个可行的解决方案，因为首先有太多的解决方案，而计算它们需要花费太多的时间。

Answer 1

是的，在默认情况下，Sat4j是确定性的:如果您在同一个问题上从命令行中多次运行它，它总是会找到相同的解决方案。

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

但是，请注意，如果您在命令行中多次这样做：

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