如何使用 sympy 简化基于附加逻辑约束的逻辑表达式

Question

问题

有没有一种方法可以使用

sympy

来简化（在通常定义模糊的意义上）基于一些逻辑约束表达式的逻辑目标表达式？目标表达式和约束都可以在一组符号中具有任意形式

A,B,C...

和操作数

>>,&,|,~

.

例如说我会期待

how_to_do_this( (C & A) | (C & B), [A >> B, ] )
-> (B & C)

请注意，可能存在多个约束。除了一般情况外，仅具有简单含义作为约束的特殊情况也会令人感兴趣。

第一想法

我能想到的一种骇人听闻的方法是简单地添加约束，因为

sp.simplify("A >> B & (C & A) | (C & B)")
-> B & C

但是，对于具有不同目标表达式的相同约束

A >> B

，这会用约束信息“污染”目标表达式，例如

sp.simplify("A >> B & (C & D)")
-> C & D & (B | ~A)

这是不需要的，因为约束属于不同的逻辑上下文。这里的方法失败了，因为我只是期望结果

(C & D)

，因为约束不能用于简化任何事情。

更正式地说，在这种方法中，约束成为目标表达式的一部分，因此它必须确保。

三思

不同的观点，然而这几乎是等同的问题，将用代数表达式重新表述它，例如

how_to_do_this(x+2*y, [x+y==5]) 
-> y+5

但是，请注意，显式方法“为

x+y=5

求解

x=5-y

并将其代入

x+2*y

”在这里不是一个足够通用的解决方案，例如在这个意义上，约束

A>>B

不能“解决”

A

（或

B

），也不能是更复杂的逻辑条件。该算法应该“分组”

x+y

并将其替换为

5

，即

x+2*y=y+(x+y)=y+5

。如果这种机制对于代数表达式是已知的，那么它也应该适用于逻辑表达式：“将

A >> B

分组并用

True

替换它”。

然而，这些只是想法。