如何使用SymPy结合约束条件简化关系不等式表达式？

我正在用SymPy处理不等式，示例表达式如下：

expression = (x > 852 | y <= 7) & (x > 704 | y >= 6)

已知约束条件constraint = x <= 759为真，因此x > 852这一项必然为假，期望将表达式简化为：

(y <= 7) & (x > 704 | y >= 6)

尝试过用subs直接替换约束条件，但只能做直接替换，无法达到简化效果，代码如下：

import sympy

x = sympy.Symbol('x')
y = sympy.Symbol('y')

# (x > 852 | y <= 7) & (x > 704 | y >= 6)
expression = (sympy.Gt(x, 852) | sympy.Le(y, 7)) & (sympy.Gt(x, 704) | sympy.Ge(y, 6))

# x <= 759
condition = sympy.Le(x, 759)

# 仅做直接替换，无法简化表达式
expression = expression.subs(condition, True)

解决方案 #

可以用SymPy的refine函数结合约束条件来实现简化，refine能根据给定的假设条件对表达式进行逻辑简化。修改后的代码如下：

import sympy

x = sympy.Symbol('x')
y = sympy.Symbol('y')

expression = (sympy.Gt(x, 852) | sympy.Le(y, 7)) & (sympy.Gt(x, 704) | sympy.Ge(y, 6))
condition = sympy.Le(x, 759)

# 使用refine结合约束条件简化表达式
simplified_expr = sympy.refine(expression, condition)
print(simplified_expr)

运行后会输出：(y <= 7) & ((x > 704) | (y >= 6))，符合预期的简化结果。

原理说明 #

• refine函数会分析表达式中的各个子项，结合给定的约束条件判断子项的真假：因为x <=759，所以x>852恒为假，在逻辑或运算(假 | y<=7)中，结果等价于y<=7，从而完成简化。
• 相比subs只是直接替换符号，refine能基于逻辑规则对表达式进行智能简化。

内容的提问来源于stack exchange，提问作者Germán Castro