SCIP代码如何处理SAT问题? [英] How does the SCIP code treat SAT problems?

问题描述

我正在尝试找出SCIP如何处理SAT问题.

I am trying to find out how SCIP treats SAT problems.

在SCIP网站上，建议在读取cnf文件后在SAT问题中的命令行中键入"set强调cpsolver".然后，在键入"optimize"之后，SCIP求解器将做自己的事情.我对代码跟踪不是特别熟练，并且想知道SCIP求解器在键入设置强调cpsolver"命令后采用的途径.

In the SCIP website, it is recommended to type 'set emphasis cpsolver' in the command line for SAT problems after reading the cnf file. The SCIP solver would then do its own thing after typing 'optimize'. I am not particularly skilled in code tracing and would like to know the pathway the SCIP solver takes after typing the 'set emphasis cpsolver' command.

此命令是否处理SAT问题并从其他地方简单地调用SAT解算器?还是将SAT问题视为离散优化问题，并使用诸如切割平面，分支和边界之类的经典方法来解决?

Does this command take the SAT problem and simply call a SAT solver from elsewhere? Or does it treat the SAT problem as a discrete optimisation problem and use the classical methods such as cutting planes, branch and bound to solve it?

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

So far, I have ran SCIP on 50 instances of SAT problems on 8h time limit each, with no result. Using SAT solvers with backdoors under the same 8h time limit leads to successful solving of about half the instances.

推荐答案

当您运行set emphasis cpsolver时，SCIP将显示已更改的设置.主要是禁用lp解决，并且增加了冲突分析的工作范围. 因此，SCIP使用更多的冲突分析进行分支定界，而无需使用lp-relaxation，而是使用伪解决方案进行绑定.它不会从其他地方调用SAT求解器.

when you run set emphasis cpsolver SCIP displays the settings that are changed. Mainly, lp-solving is disabled and the working limits for conflict analysis are increased. So SCIP runs branch-and-bound with more conflict analysis and without using an lp-relaxation, instead, it uses the pseudo-solution for bounding. It does not call a SAT solver from somewhere else.

让我感到惊讶的是，专用的SAT求解器可能会胜过SCIP.另请注意，为了解决SCIP的SAT问题，不必将强调设置设置为cpsolver，也可以尝试使用默认参数运行(或者如果您认为lp-relaxation不是，则仅禁用lp-solving.对您的问题有用).

It is not surprising to me that SCIP might be outperformed by dedicated SAT solvers. Please also note that it is not necessary to set the emphasis setting to cpsolver in order to solve a SAT problem with SCIP, you can also try running with default parameters (or merely disabling lp-solving if you do not think the lp-relaxation is useful for your problem).

我希望这些信息对您有所帮助.

I hope this information is helpful.

这篇关于SCIP代码如何处理SAT问题?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！