解决Sympy中的约束满足问题

Question

我试图在Sympy解决一些简单的Boolean satisfiability problems。在这里，我试图解决包含Or逻辑运算符的约束：

from sympy import *
a,b = symbols("a b")

print(solve(Or(Eq(3, b*2), Eq(3, b*3))))
# In other words: (3 equals b*2) or (3 equals b*3)
# [1,3/2] was the answer that I expected

令人惊讶的是，这会导致错误：

TypeError: unsupported operand type(s) for -: 'Or' and 'int'

我可以使用Piecewise解决这个问题，但这更详细：

from sympy import *
a,b = symbols("a b")
print(solve(Piecewise((Eq(3, b*2),Eq(3, b*2)), (Eq(3, b*3),Eq(3, b*3)))))
#prints [1,3/2], as expected

不幸的是，当我尝试解决两个变量而不是一个变量时，这种解决方法失败了：

from sympy import *
a,b = symbols("a b")

print(solve([Eq(a,3+b),Piecewise((Eq(b,3),Eq(b,3)), (Eq(b,4),Eq(b,4)))]))
#AttributeError: 'BooleanTrue' object has no attribute 'n'

是否有更可靠的方法来解决像Sympy这样的约束？

Answer 1

每个等式可以表示为等于0的等式。例如，3-2 * b = 0而不是3 = 2 * b。 （在Sympy中，你甚至不必编写=0部分，它是假定的。）然后你可以简单地乘方程来表达OR逻辑：

>>> from sympy import *
>>> a,b = symbols("a b")
>>> solve((3-b*2)*(3-b*3))
[1, 3/2]
>>> solve([a-3-b, (3-b*2)*(3-b*3)])
[{b: 1, a: 4}, {b: 3/2, a: 9/2}]

Answer 2

为了扩展zaq的答案，SymPy无法识别solve中的逻辑运算符，但您可以使用以下事实：

a*b = 0

相当于

a = 0 OR b = 0

也就是说，将两个方程相乘

solve((3 - 2*b)*(3 - 3*b), b)

另外请注意，如果您想使用AND而不是OR，则可以求解系统。那是，

solve([eq1, eq2])

相当于解决

eq1 = 0 AND eq2 = 0

Answer 3

我找到了解决Sympy中约束满足问题的另一种方法。它只是将布尔表达式转换为连接法线形式，以生成多个方程组：

import sympy
a,b,c = sympy.symbols("a,b,c")

def clauses(Arg,expr):    # for DNFs only
    if not isinstance(expr, Arg):
        return expr,
    return expr.args

def backtrack_solutions_(the_list,total_list,solutions):
    if(the_list == []):
        solution = sympy.solve(total_list)
        if solution != [] and solution not in solutions:
            solutions += [solution]
        return
    head, *tail = the_list
    for j in head:
        if(sympy.solve(total_list+[j]) != []):
            backtrack_solutions_(tail,total_list+[j],solutions)
    return solutions

def backtrack_solutions(formula_to_solve):
    return backtrack_solutions_([list(clauses(sympy.boolalg.Or,a)) for a in clauses(sympy.boolalg.And,sympy.boolalg.to_cnf(formula_to_solve))],[],[])

# (3 = b*2) or (3 = b*3)
to_solve = sympy.Or(sympy.Eq(3, b*2), sympy.Eq(3, b*3))

print(["All solutions:",backtrack_solutions(to_solve)])

这个例子打印['All solutions:', [{b: 3/2}, {b: 1}]]。