解决命题逻辑/布尔表达式的工具(SAT Solver?)

Question

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

在汽车行业，当你买车时，你有成千上万种不同的部件可供选择。并不是每一个组件都是可组合的，所以对于每一辆车，都存在许多用命题逻辑表示的规则。就我而言，每辆车都有2000到4000条规则。

它们看起来像这样：

1. A→B∧C∧D
2. C→-F
3. F∧G→D

其中"∧"="and"/"∆"="或"/"-"="not"/"→"="含义".

变量A、B、C。。。链接到BOM表中的零部件。我拥有的数据由成对的组件及其链接的变量组成。

示例：

1. 组件_1，组件_2：(A)∧(B)
2. 组件_1，组件_3:(A)∧(C∧F)
3. 组件_3，组件_5：(B∧G)

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

1. 哪种工具、软件和算法可以解决这些类型的问题
2. 有说明性的例子吗
3. 我如何将其自动化，以便检查列表中的每个组合
4. 一般来说，我应该在谷歌上搜索什么来加深我对这个主题的了解

非常感谢您的帮助！Olaf

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

然后，您可以使用顶级搜索布尔公式的解决方案，就像这里的示例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