mathematical-optimization - SCIP 代码如何处理 SAT 问题？

Question

我试图找出 SCIP 如何处理 SAT 问题。

在 SCIP 网站中，建议在读取 cnf 文件后在命令行中键入 'set强调 cpsolver' 来解决 SAT 问题。SCIP 求解器会在输入“优化”后做自己的事情。我在代码跟踪方面不是特别熟练，我想知道 SCIP 求解器在键入“设置强调 cpsolver”命令后所采用的路径。

此命令是否处理 SAT 问题并简单地从其他地方调用 SAT 求解器？还是将SAT问题当作离散优化问题，使用切割平面、分支定界等经典方法求解？

到目前为止，我已经在 8 小时的时间限制内对 50 个 SAT 问题实例运行了 SCIP，但没有结果。在相同的 8 小时时间限制下使用带有后门的 SAT 求解器可以成功求解大约一半的实例。

标签： mathematical-optimizationscipsat

Answer 1

当您运行set emphasis cpsolverSCIP 时，会显示更改的设置。主要是禁用 lp-solving 并增加冲突分析的工作限制。因此 SCIP 使用更多的冲突分析运行分支定界，并且不使用 lp-relaxation，而是使用伪解进行定界。它不会从其他地方调用 SAT 求解器。

SCIP 可能会被专门的 SAT 求解器超越，这对我来说并不奇怪。另请注意，没有必要将强调设置设置为 cpsolver 以解决 SCIP 的 SAT 问题，您也可以尝试使用默认参数运行（或者如果您认为 lp-relaxation 不适合，则仅禁用 lp-solving对您的问题有用）。

我希望这些信息对你有用。