如何使用SCIP解决SAT问题？

Question

我正在尝试使用SCIP来解决SAT问题。我的公司使用Mobaxterm的Linux命令行。我已经安装了SCIPoptsuite 6.0.2。我在网上找不到任何关于如何打电话给SCIP来解决SAT问题的信息，包括英文和中文。我有很多cnf文件，我想调用SCIP来解决：enter image description here

有人能指导我怎么做吗？

Answer 1

使用SCIP的交互式shell，您只需阅读问题并解决它。

因此，启动您的SCIP二进制文件(如果它是全局安装的，那么只执行scip就足够了；否则，从安装它的位置调用该二进制文件)。

然后，在交互式shell中，读取问题，例如read 115_3448s.cnf并解决它：optimize。然后，您可以通过display solution打印。有关交互式外壳的简短教程，请参见https://scip.zib.de/doc-6.0.2/html/SHELL.php。

请注意，SCIP是CIP解算器，通常使用LP松弛进行边界处理。如果您想要解算SAT实例(set emphasis cpsolver)，则可以禁用此功能，但与专用的SAT解算器相比，仍有很大的开销。因此，如果您只想求解纯SAT实例，则可能需要尝试专用的SAT解算器。但是，如果您以后考虑添加一些其他常规线性约束，SCIP应该是一个很好的选择。