如何为 SAT 问题生成切割平面？答案

【问题标题】：How to generate cutting planes for a SAT problem?如何为 SAT 问题生成切割平面？
【发布时间】：2021-12-23 08:29:18
【问题描述】：

我正在研究需要我为 SAT 问题生成切割平面的想法。我正在使用来自https://www.cs.ubc.ca/~hoos/SATLIB/benchm.html 的问题，来自 SAT 编码的准群（或拉丁方）实例的 qg5-10.cnf。

我正在使用最新版本的 SCIP，SCIP8.0.0。我想知道是否有任何方法可以为 SAT 问题生成切割平面并打印出生成的切割平面。我只需要在预求解后的第一次迭代中执行此操作。

我尝试了以下方法：

set separating gomory freq 65534, set separating (other cutting plane methods) freq -1

但是，这并不能告诉我在使用 optimize 命令时是否正在生成 gomory 切割。

但是什么都没有打印出来，让我认为 SCIP 的默认分支规则根本没有使用切割平面。

有关如何进行此操作的一些建议将帮助我检验我的切割平面假设。谢谢！

【问题讨论】：

【解决方案1】：

切割平面的生成/分离不受分支规则的约束。您只需运行display statistics 即可查看是否已生成和分离了哪些剪辑。

【讨论】：