在 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)which give [0]（我不知道这是什么意思），solve(x * y = True, x)结果是 a SyntaxError，solve(x * y, True, x)然后solve(x & y, True, x)给了AttributeError. 我不知道还能尝试什么！

编辑（2）：我也发现了这个，可能有用！

Answer 1

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

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

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

• 正如我在另一个问题的回答中提到的，Symbol('y', bool=True)什么也不做。Symbol('x', something=True)将is_something假设设置为x，但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，其中n是表达式中变量的数量。

但是，如果您想找到所有这些，通常的技巧是将原始表达式附加~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错误的解决方案（可以认为&是在您的解决方案上添加额外的条件）。以这种方式迭代，您可以生成所有解决方案。