solves for algebraic expressions.
>>> 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))
solves the equation expr = 0 for . and so on are invalid syntax. You cannot use to mean equality in Python. See http: 我需要解决一组符号布尔表达式，如。这样的变量数量很大(约200个)，所以不可能采用蛮力策略。我在网上搜索了一下，发现 Sympy
和
>>> 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)EDIT：我主要是尝试着去操作这样的事情。solve(x & y, True, x)结果是... AttributeError. 然后我试了一下
这给 我不知道这是什么意思）。 导致
,. 我不知道还可以尝试什么!
solveEDIT（2）: 我还发现 solve(expr, x)这个x，可能会有用!
solve(x | y = False) = 我需要解决一组符号布尔表达式，如：>>>solve(x /docs.sympy.orglatesttutorialgotchas.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 是假的 & 作为对你的解决方案添加额外的条件）。) 通过这种方式迭代，你可以生成所有的解决方案。
我想我得到了 它 (虽然用途还不清楚)。