在SAT4J文档中的代码示例中，对同一SAT问题多次调用求解器总是会产生相同的解决方案，即使存在多个可能的解决方案-也就是说，结果是确定的。
我正在寻找一种在多次运行中获得不同解决方案的方法，也就是说，一个不确定/随机的结果。对于每个可能的解决方案，应该有一个非零概率的解决方案被挑选。理想情况下，每个解决方案都应该以相同的概率进行选择，但这不是一个严格的要求。
我知道(确定性地(迭代所有解决方案并只取一个随机的解决方案的可能性，但在我的情况下，这不是一个可行的解决方案，因为一开始有太多解决方案，计算它们都需要太长时间。
是的，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