logic - 解决命题逻辑/ bool 表达式的工具(SAT Solver？)

Question

我不熟悉命题逻辑和 bool 表达式。所以这就是我需要帮助的原因。这是我的问题:

在汽车行业，当您购买汽车时，有数千种不同的组件可供选择。并非每个组件都是可组合的，因此对于每辆汽车，存在许多以命题逻辑表达的规则。在我的例子中，每辆车都有 2000 到 4000 条规则。

它们看起来像这样:

1. A → B ∨ C ∨ D
2. C → ¬F
3. F∧G→D
4. ...

其中“∧”=“和”/“∨”=“或”/“¬”=“不”/“→”=“暗示”。

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

例子:

1. Component_1, Component_2: (A) ∧ (B)
2. 组件_1、组件_3:(A) ∧ (C ∨ F)
3. 组件_3、组件_5:(B ∨ G)
4. ...

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

1. 哪些工具、软件和算法可以解决这类问题？
2. 是否有说明性示例？
3. 如何实现自动化，以便检查列表中的每个组合？
4. 一般来说，我应该在 Google 中搜索什么来加深我在这个主题上的知识？

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

Answer 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)).

然后您可以使用顶层来搜索 bool 公式的解决方案，例如这里的异或示例:

?- 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 代码展示的好处是，可以通过 Prolog 代码本身完成对 SAT 公式的问题编码。当上面的代码运行时，我得到了预期的结果:

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