我正在尝试了解 SCIP 如何处理 SAT 问题。
在 SCIP 网站中，建议在读取 cnf 文件后在命令行中输入“setemergency cpsolver”来解决 SAT 问题。 SCIP 求解器会在输入“optimize”后执行自己的操作。我在代码跟踪方面并不是特别熟练，并且想知道 SCIP 求解器在输入“set focus cpsolver”命令后所采取的路径。
此命令是否会处理 SAT 问题并简单地从其他地方调用 SAT 求解器？还是将SAT问题视为离散优化问题并使用割平面、分支定界等经典方法来求解？
到目前为止，我已经在 8 小时的时间限制内对 50 个 SAT 问题实例运行了 SCIP，但没有结果。在同样的 8 小时时间限制下使用带有后门的 SAT 求解器可以成功解决大约一半的实例。
当你跑步时set emphasis cpsolverSCIP 显示更改的设置。主要是禁用了 lp 求解，并增加了冲突分析的工作限制。
因此 SCIP 运行分支定界并进行更多冲突分析，并且不使用 lp 松弛，而是使用伪解进行定界。它不会从其他地方调用 SAT 求解器。
SCIP 的性能可能优于专用 SAT 求解器，这对我来说并不奇怪。另请注意，没有必要将重点设置设置为 cpsolver 来解决 SCIP 的 SAT 问题，您也可以尝试使用默认参数运行（或者如果您认为 lp 松弛不存在，则仅禁用 lp 求解）对你的问题有用）。
我希望这些信息对你有用。
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
