3

我对命题逻辑和布尔表达式这个话题很陌生。所以这就是我需要帮助的原因。这是我的问题：

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

它们看起来像这样：

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

其中“∧”=“和”/“∨”=“或”/“¬”=“非”/“→”=“蕴涵”。

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

例子：

  1. 组件_1，组件_2：（A）∧（B）
  2. 组件_1，组件_3：（A）∧（C∨F）
  3. 组件_3，组件_5：（B∨G）
  4. ...

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

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

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

4

1 回答 1

0

您可能想尝试使用 SAT Solver 的 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 代码演示的好处是，可以通过 Prolog 代码本身来完成对 SAT 公式的问题编码。运行上述代码时，我按预期得到以下结果：

?- L=[_,_,_,_,_,_], kitchen(L), labeling(L).
L = [0,1,0,0,1,0] ;
L = [1,0,0,0,0,1] ;
No
于 2018-03-19T00:45:06.303 回答