sat4j - 如何在 SAT4J 中随机(非确定性地)找到解决方案?
问题描述
在 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
推荐阅读
- arrays - 将mysql记录集中的多列转换为数组
- xcode - 白色背景在 TextFIeld 中显示为透明
- javascript - 当我在 Angular 8 中使用 CTRL + R 重新加载时,页面重定向到主页
- shell - 使用没有文件的 privet SSH 密钥
- spring-boot - 如何将 JobParameters 传递给 Spring Cloud Task 启动的批处理作业?
- scala - 具有连接操作的随机整数的 UDF 的意外行为
- python - 从 tensorflow 打印输出的问题,特定于 C api
- html - caddy webserver - 网站域配置
- c# - ASP.NET Core 中的星级评定
- php - SQLSTATE [42S02]:未找到基表或视图:1146 表“laravel_abonamenty2.currencies”不存在