在Python中解决符号布尔变量 [英] Solving Symbolic Boolean variables in Python

问题描述

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

I need to solve a set of symbolic Boolean expressions like:

>>> 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 和

Number of such variables is large (~200) so that Brute Force strategy is not possible. I searched the web and found that Sympy and Sage have symbolic manipulation capabilities (particularly this and this may be useful). How can I do that?

我主要是试图操纵这些东西:

I mainly tried to manipulate such things:

>>> 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)和solve(x & y, True, x)给出了AttributeError.我不知道还能尝试什么！

which results in NotImplementedError. Then I tried solve(x * y, x) which gave [0] (I don't know what does it mean), solve(x * y = True, x) resulted in a SyntaxError, solve(x * y, True, x) and solve(x & y, True, x) gave an AttributeError. I don't know what else to try!

编辑(2):我还发现这，可能会有用！

EDIT (2): I also found this, may be useful!

推荐答案

首先，更正您的问题中某些明显错误的事情:

First, to correct a few things that are just blatently wrong in your question:

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

• solve solves for algebraic expressions. solve(expr, x) solves the equation expr = 0 for x.

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

solve(x | y = False) and so on are invalid syntax. You cannot use = to mean equality in Python. See http://docs.sympy.org/latest/tutorial/gotchas.html#equals-signs (and I recommend reading the rest of that tutorial as well).

正如我在另一个问题的答案中提到的那样， Symbol('y', bool=True)不执行任何操作. Symbol('x', something=True)在x上设置is_something假设，但bool不是SymPy的任何部分都认可的假设.只需对布尔表达式使用常规的Symbol('x').

As I mentioned in the answer to another question, Symbol('y', bool=True) does nothing. Symbol('x', something=True) sets the is_something assumption on x, but bool is not a recognized assumption by any part of SymPy. Just use regular Symbol('x') for boolean expressions.

正如一些评论者所述，您想要的是satisfiable，它实现了SAT解算器. satisfiable(expr)告诉您expr是否可满足，即expr中是否存在使它成立的变量值.如果可以满足，则返回这些值的映射(称为模型").如果不存在这样的映射，即expr是矛盾的，它将返回False.

As some commenters noted, what you want is satisfiable, which implements a SAT solver. satisfiable(expr) tells you if expr is satisfiable, that is, if there are values for the variables in expr that make it true. If it is satisfiable, it returns a mapping of such values (called a "model"). If no such mapping exists, i.e., expr is a contradiction, it returns False.

因此，satisfiable(expr)与解决expr = True相同.如果要求解expr = False，则应使用satisfiable(~expr)(SymPy中的~表示不).

Therefore, satisfiable(expr) is the same as solving for expr = True. If you want to solve for expr = False, you should use satisfiable(~expr) (~ in SymPy means not).

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是表达式中变量的数量.

Finally, note that satisfiable only returns one solution, because in general this is all you want, whereas finding all the solutions in general is extremely expensive, as there could be as many as 2**n of them, where n is the number of variables in your expression.

但是，如果要查找所有这些表达式，通常的技巧是在原始表达式后附加~E，其中E是先前解决方案的结合.例如，

If however, you want to find all of them, the usual trick is to append your original expression with ~E, where E is the conjunction of the previous solution. So for example,

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为true而y为false的解决方案(将&视为在解决方案上添加了额外条件).以这种方式进行迭代，您可以生成所有解决方案.

The & ~(x & ~y) means that you don't want a solution where x is true and y is false (think of & as adding extra conditions on your solution). Iterating this way, you can generate all solutions.

这篇关于在Python中解决符号布尔变量的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！