求解命题逻辑/布尔表达式的工具（SAT求解器？-解网

问：

我是命题逻辑和布尔表达式的新手。所以这就是我需要帮助的原因。这是我的问题：

在汽车行业，当您购买汽车时，有数千种不同的组件可供选择。不是每个组件都是可组合的，所以对于每辆车来说，都存在许多用命题逻辑表达的规则。就我而言，每辆车都有 2000 到 4000 条规则。

它们看起来像这样：

A → B ∨ C ∨ D
C → ¬F
F ∧ G → D
...

其中 “∧” = “and” / “∨” = “or” / “¬” = “not” / “→” = “implication”。

变量 A、B、C、...链接到物料清单中的组件。我拥有的数据由成对的组件及其链接变量组成。

例：

Component_1、Component_2：（A）∧（B）
Component_1， Component_3：（A） ∧ （C ∨ F）
Component_3，Component_5：（B∨G）
...

现在，我的问题是如何解决这个问题。具体来说，我想知道根据上述规则，组件的每种组合是否可行。

哪种工具、软件和算法可以解决这些类型的问题？
有没有一个说明性的例子？
我怎样才能自动化它，以便我可以检查列表中的每个组合？
一般来说，我应该在谷歌中搜索什么来加深我对这个主题的了解？

非常感谢您的帮助！奥拉夫

-逻辑布尔表达式 SAT 满足性

您可以查看过去的 SAT 竞赛列表，选择一种工具来解决自己的问题。恕我直言，《满意手册》是您可以开始的关于该主题的最全面的介绍。对所有规则进行编码后，您可以使用所谓的全卫星搜索来列出公式的所有可能模型，每个模型对应于特定的组件组合。要实现自动化，请使用一些脚本来生成 SAT 公式。如果可能，请尝试在用例中以增量方式使用求解器，以获得更好的性能。

2赞 Olaf_SQL 12/6/2017

好的，非常感谢。尤其是“全坐”搜索可能会对我有所帮助。

0赞 CaptainTrunky 12/13/2017

至于 AllSAT，我会推荐 sharpCDCL，我对它有很好的积极体验，解决了一些现实世界的 poblems。如果想要更多的“表现力”，可以考虑使用搭扣

答：

0赞 user502187 3/19/2018 #1

您可能想尝试带有 SAT 求解器的 Prolog 系统，例如 SWI-Prolog、Jekejeke Minlog 等......您可以在 Prolog 系统的 REPL 中轻松使用它。要加载 SAT 求解器，只需键入（您不需要键入？- 本身）：

/* in SWI-Prolog */
?- use_module(library(clpb)).

/* in Jekejeke Minlog */
?- use_module(library(finite/clpb)).

然后，您可以使用顶层来搜索布尔公式的解决方案，例如此处的 xor 示例：

?- sat(X#Y), labeling([X,Y]).
X = 0,
Y = 1 ;
X = 1,
Y = 0.

下面是厨房规划器代码的示例。厨房有3个地方，我们分配了一个冰柜和一个炉子。冰箱不允许靠近炉子。

冰箱的代码为 0,1，炉子的代码为 1,0。我们利用卡约束来放置冰柜和炉子。

:- use_module(library(finite/clpb)).

freezer([X,Y|L],[(~X)*Y|R]) :-
   freezer(L, R).
freezer([], []).

stove([X,Y|L],[X*(~Y)|R]) :-
   stove(L, R).
stove([], []).

free([X,Y|L],[(~X)*(~Y)|R]) :-
    free(L, R).
free([], []).

allowed([X,Y,Z,T|L]) :-
   sat(~((~X)*Y*Z*(~T))),
   sat(~(X*(~Y)*(~Z)*T)),
   allowed([Z,T|L]).
allowed([_,_]).
allowed([]).

kitchen(L) :-
   freezer(L, F), card(1, F),
   stove(L, G), card(1, G),
   free(L, H), card(1, H),
   allowed(L).

我想用 Prolog 代码展示的好处是，SAT 公式的问题编码可以通过 Prolog 代码本身来完成。当上面的代码运行时，我得到以下结果，如预期的那样：

?- L=[_,_,_,_,_,_], kitchen(L), labeling(L).
L = [0,1,0,0,1,0] ;
L = [1,0,0,0,0,1] ;
No

上一个：简化大条件语句

下一个：用于避免 NP 完备性的受限布尔公式

求解命题逻辑/布尔表达式的工具（SAT求解器？

Tool to solve propositional logic / boolean expressions (SAT Solver?)

评论