在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和{a2}具有符号操作功能（尤其是this和{a4}可能有用）。我怎么能做到呢？在

编辑：我主要是想操纵这些东西：

^{pr2}$

结果是NotImplementedError。 然后我尝试了solve(x * y, x)，它给出了[0]（我不知道这是什么意思），solve(x * y = True, x)得到了SyntaxError，solve(x * y, True, x)，而{}给出了AttributeError。我不知道还能做什么！在

编辑（2）：我还发现this，可能有用！在

Answer 1

首先，纠正你问题中一些明显错误的地方：

• solve求解代数表达式。^{{cdr>

• 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假设，但是{}不是SymPy任何部分都认可的假设。只需对布尔表达式使用正则Symbol('x')。

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

因此，satisfiable(expr)与求解{}是相同的。如果你想求解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，其中{}是表达式中的变量数。在

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

^{pr2}$

& ~(x & ~y)表示您不希望得到一个x为真且y为假的解决方案（可以将&视为在解决方案上添加额外的条件）。以这种方式迭代，您可以生成所有的解决方案。在

Answer 2

我想我得到了it（虽然它的用法还不清楚）。在