在Python中求解符号布尔变量

2021-05-13 15:18:54 发布

您现在位置:Python中文网/ 问答频道 /正文

我需要解一组符号布尔表达式,例如:

>>> 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)得到了SyntaxErrorsolve(x * y, True, x),而{}给出了AttributeError。我不知道还能做什么!在

编辑(2):我还发现this,可能有用!在

2条回答
网友
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为假的解决方案(可以将&视为在解决方案上添加额外的条件)。以这种方式迭代,您可以生成所有的解决方案。在

网友
2楼 ·

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

相关问题