我是命题逻辑和布尔表达式的新手.所以这就是我需要帮助的原因.这是我的问题:
在汽车行业,您可以在购买汽车时选择数千种不同的组件.并非每个组件都是可组合的,因此对于每辆车而言,存在许多以命题逻辑表达的规则.在我的情况下,每辆车都有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