在 Python 中求解符号布尔变量

Question

我需要解决一组符号布尔表达式，例如：

>>> solve(x | y = False)
(False, False)

>>> solve(x & y = True)
(True, True)

>>> solve (x & y & z = True)
(True, True, True)

>>> solve(x ^ y = False)
((False, False), (True, True))

此类变量的数量很大（~200），因此暴力策略是不可能的。我在网上搜索，发现Sympy 和Sage 具有符号操作能力（特别是this 和this 可能有用）。我该怎么做？

编辑：我主要试图操纵这样的事情：

>>> from sympy import *

>>> x=Symbol('x', bool=True)

>>> y=Symbol('y', bool=True)

>>> solve(x & y, x)

导致NotImplementedError。 然后我尝试了solve(x * y, x)，它给出了[0]（我不知道这是什么意思），solve(x * y = True, x) 导致了SyntaxError，solve(x * y, True, x) 和solve(x & y, True, x) 给出了AttributeError。我不知道还能尝试什么！

编辑（2）：我还找到了this，可能有用！

Answer 1

首先，纠正您的问题中明显错误的一些事情：

• solve 求解代数表达式。 solve(expr, x) 求解 x 的方程 expr = 0。

• solve(x | y = False) 等是无效的语法。在 Python 中，您不能使用 = 来表示相等。请参阅http://docs.sympy.org/latest/tutorial/gotchas.html#equals-signs（我建议您也阅读该教程的其余部分）。

• 正如我在回答another 问题时提到的，Symbol('y', bool=True) 什么都不做。 Symbol('x', something=True) 在x 上设置is_something 假设，但bool 不是SymPy 的任何部分认可的假设。只需将常规 Symbol('x') 用于布尔表达式即可。

正如一些评论者所说，你想要的是 satisfiable，它实现了一个 SAT 求解器。 satisfiable(expr) 告诉您 expr 是否可满足，也就是说，expr 中的变量是否存在使其正确的值。如果它是可满足的，它会返回这些值的映射（称为“模型”）。如果不存在这样的映射，即expr 是矛盾的，则返回False。

因此，satisfiable(expr) 与求解 expr = True 相同。如果要解决expr = False，则应使用satisfiable(~expr)（SymPy 中的~ 表示不是）。

In [5]: satisfiable(x & y)
Out[5]: {x: True, y: True}

In [6]: satisfiable(~(x | y))
Out[6]: {x: False, y: False}

In [7]: satisfiable(x & y & z)
Out[7]: {x: True, y: True, z: True}

最后，请注意satisfiable 只返回一个解决方案，因为通常这就是您想要的全部，而找到所有解决方案通常非常昂贵，因为它们可能多达2**n，其中@ 987654348@ 是表达式中的变量数。

但是，如果您想找到所有这些，通常的技巧是在您的原始表达式后面加上~E，其中E 是前一个解决方案的合取。例如，

In [8]: satisfiable(x ^ y)
Out[8]: {x: True, y: False}

In [9]: satisfiable((x ^ y) & ~(x & ~y))
Out[9]: {x: False, y: True}

& ~(x & ~y) 表示您不想要x 为真而y 为假的解决方案（将& 视为在您的解决方案中添加额外条件）。以这种方式迭代，您可以生成所有解决方案。

Answer 2

我想我得到了it（尽管它的用途还不清楚）。