0

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

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

所以，我的问题是：

  1. 您能否解释一下什么polarity是或向我指出一些入门级的资源？

  2. cryptominisat（或通常在 SAT 求解器中）是否有接口来设置逻辑变量的默认值？这种功能的术语是什么？

谢谢。

4

1 回答 1

0

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。请参阅相关问题。实际上，我StackOverflow在 2012 年提出的第一个问题。

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

于 2017-08-01T19:32:25.757 回答