5

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

>>> 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）：我也发现了这个，可能有用！

4

2 回答 2

4

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

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

  • solve(x | y = False)等等都是无效的语法。在 Python 中，您不能使用=to 来表示相等。请参阅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为假的解决方案（认为&在您的解决方案上添加额外的条件）。以这种方式迭代，您可以生成所有解决方案。

于 2013-11-05T01:29:49.020 回答
0

我想我明白了（尽管它的用途还不清楚）。

于 2013-11-01T06:24:54.310 回答