解决命题逻辑/布尔表达式的工具(SAT解算器?) [英] Tool to solve propositional logic / boolean expressions (SAT Solver?)

问题描述

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

I am new to the topic of propositional logic and boolean expressions. So this is why I need help. Here is my problem:

在汽车工业中，购买汽车时可以选择成千上万种不同的组件.并非每个组件都是可组合的，因此对于每辆汽车，都有很多以命题逻辑表示的规则.就我而言，每辆车都有2000到4000条规则.

In the car industry you have thousand of different variants of components available to choose from when you buy a car. Not every component is combinable, so for each car there exist a lot of rules that are expressed in propositional logic. In my case each car has between 2000 and 4000 rules.

它们看起来像这样:

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

其中∧" =和"/∨" =或"/¬" =非"/→" =蕴涵".

where "∧" = "and" / "∨" = "or" / "¬" = "not" / "→" = "implication".

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

The variables A, B, C, ... are linked to the components in the bill of material. The data I have consists of pairs of components with their linked variables.

示例:

1. Component_1，Component_2:(A)∧(B)
2. Component_1，Component_3:(A)∧(C∨F)
3. Component_3，Component_5:(B∨G)
4. ...

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

Now, my question is how to solve this problem. Specifically, I would like to know if each combination of the components is possible according to rules above.

1. 哪种工具，软件和算法可以解决这类问题?
2. 有没有说明性的例子?
3. 如何使其自动化，以便可以检查列表中的每个组合?
4. 通常，我应该在Google中搜索什么以加深我对该主题的了解?

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

Thank you very much for your help! Olaf

推荐答案

您可能想尝试使用SAT解算器的Prolog系统，例如SWI-Prolog，Jejejeke Minlog等，您可以轻松地在其中使用它Prolog系统的REPL.要加载SAT解算器，只需键入(您无需键入?-本身):

You might want to try a Prolog system with a SAT Solver, such as SWI-Prolog, Jekejeke Minlog, etc... you can readily play with it in the REPL of the Prolog system. To load the SAT solver just type (you don't need to type the ?- itself):

/* in SWI-Prolog */
?- use_module(library(clpb)).

/* in Jekejeke Minlog */
?- use_module(library(finite/clpb)).

然后，您可以使用顶级搜索布尔公式的解，例如本例中的xor:

You can then use the top-level to search for solutions of a boolean formula, like this example here an xor:

?- sat(X#Y), labeling([X,Y]).
X = 0,
Y = 1 ;
X = 1,
Y = 0.

这是厨房计划员代码的示例.厨房有3个地方， 我们分配了一个冰柜和一个火炉.冰箱不能靠近火炉.

Here is an example of a kitchen planner code. The kitchen has 3 places, and we assign a freezer and a stove. The freezer is not allowed to be near to the stove.

冷冻室的代码为0,1，火炉的代码为1,0.我们利用卡约束来放置冰柜和火炉.

The freezer has code 0,1 and the stove has code 1,0. We make use of the card constraint to place the freezer and the stove.

:- 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公式编码的问题.运行上面的代码后，按预期方式得到以下结果:

What I want to demonstrate with the Prolog code is the benefit, that problem encoding towards a SAT formulation can be done via Prolog code itself. When the above code is run I get the following result as expected:

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

这篇关于解决命题逻辑/布尔表达式的工具(SAT解算器?)的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！