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

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

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

它们看起来像这样:

> A→B∨C∨D
> C→¬F
>F∧G→D
> ……

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

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

例:

> Component_1,Component_2:(A)∧(B)
> Component_1,Component_3:(A)∧(C∨F)
> Component_3,Component_5:(B∨G)
> ……

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

>哪种工具,软件和算法可以解决这些类型的问题?
>有说明性的例子吗?
>我如何自动化它,所以我可以检查列表中的每个组合?
>一般来说,我应该在Google中搜索哪些内容以加深我对此主题的了解?

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

最佳答案 您可能想尝试使用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
点赞