SAT求解器设置默认结果（cryptominisat）答案

【问题标题】：SAT solver set default result(cryptominisat)SAT求解器设置默认结果（cryptominisat）
【发布时间】：2017-01-17 02:43:30
【问题描述】：

我正在用 SAT 建模一个问题，并尝试用 cryptominisat 解决它。如果没有约束，我想给我的变量一个默认值。

我浏览了手册，set_default_polarity 似乎是答案。我试过了，但它没有像我预期的那样工作。我在这里并没有真正理解 polarity 这个词。一些谷歌搜索并没有帮助我，因为我不熟悉逻辑。

所以，我的问题是：

您能否解释一下polarity 是什么，或者指出一些入门级的资源？
cryptominisat（或通常在 SAT 求解器中）是否有接口来设置逻辑变量的默认值？这种功能的术语是什么？

谢谢。

【问题讨论】：

标签： logic solver sat

【解决方案1】：

cryptominisat --hhelp（注意额外的h！）提供以下扩展帮助：

.....
  --polar arg (=auto)                   {true,false,rnd,auto} Selects polarity
                                        mode. 'true' -> selects only positive
                                        polarity when branching. 'false' ->
                                        selects only negative polarity when
                                        brancing. 'auto' -> selects last
                                        polarity used (also called 'caching')
.....

我使用--polar=false 让cryptominisat 首先搜索带有false/0 变量的解决方案，因为我的示例具有大多数解决方案变量。

在源码中，这对应于solverconf.h：

enum class PolarityMode {
    polarmode_pos
    , polarmode_neg
    , polarmode_rnd
    , polarmode_automatic
};

各自的SolverConf变量是PolarityMode polarity_mode

在main.cpp 中显示了如何在程序中设置此配置属性：

if (vm.count("polar")) {
        string mode = vm["polar"].as<string>();

        if (mode == "true") conf.polarity_mode = polarmode_pos;
        else if (mode == "false") conf.polarity_mode = polarmode_neg;
        else if (mode == "rnd") conf.polarity_mode = polarmode_rnd;
        else if (mode == "auto") conf.polarity_mode = polarmode_automatic;
        else throw WrongParam(mode, "unknown polarity-mode");
    }

其他 SAT 求解器正在使用 phase 或 sign 等术语。

Microsoft Z3 可以通过命令行参数化sat.phase=always_false 以首先尝试false phase。请参阅related question。实际上，我在 2012 年就 StackOverflow 提出的第一个问题。

Clasp 正在使用命令行语法--sign-def=neg 优先使用false polarity。

【讨论】：