1

我有一个布尔方程系统（下面给出的示例）

p = x & ~y
q = x & y

现在，我想获取x系统中其他变量（如果可能是LHS变量）的表达式，或者发现无法获取。这在sympy（或z3？）中可能吗？

import sympy as s
p,q = s.symbols('p,q')
x,y = s.symbols('x,y')
v = s.And(s.Eq(p,x & y), s.Eq(q,x & ~y))

我看过，solve()但solveset()他们似乎正在处理线性方程。

>>> s.solveset(v, x)
    raise ValueError("%s is not a valid SymPy expression" % f)
ValueError: Eq(p, x & y) & Eq(q, x & ~y) is not a valid SymPy expression

还有其他选择吗？

我真的不明白文档。根据它，以下应该有效，因为它清楚地表明在 中sympy.solvers.solvers.solve(f, *symbols, **flags)，f 可以是关系表达式或布尔值。

>>> s.And(s.Equivalent(p, x &y), s.Equivalent(q, x&~y)).simplify()
(x | ~p) & (x | ~q) & (y | ~p) & (~p | ~q) & (~q | ~y) & (p | q | ~x) & (q | y | ~x) & (p | ~x | ~y)

>>> s.solve(s.And(s.Equivalent(p, x &y), s.Equivalent(q, x&~y)),x)
TypeError: unsupported operand type(s) for -: 'And' and 'int'

>>> s.solveset(s.And(s.Equivalent(p, x &y), s.Equivalent(q, x&~y)),x)
ValueError: (Equivalent(p, x & y)) & (Equivalent(q, x & ~y)) is not a valid SymPy expression
4

0 回答 0