自动简化冗余算术关系

Question

我正在寻找一种自动确定的方法，例如，

(a < 12) & (a < 3) & (c >= 4)

与

(a < 3) & (c >= 4)

相同。我研究了 Matlab 的符号工具箱和 Python 中的 SymPy，但这些显然只能简化纯布尔逻辑（例如，

simplify(a & b | b & a) -> ans=(a & b)

）

有没有办法像上面描述的那样使用这些符号数学工具？

编辑

正如对 @user12750353 的答案的评论中所指出的，我还想简化与布尔 OR 连接的关系系统，例如

((a < 12) & (a < 3) & (c >= 4)) | (a < 1)

。

Answer 1

SymPy 集可用于进行单变量简化，例如

((x < 3) & (x < 5)).as_set() -> Interval.open(-oo, 3)

和集合可以转换回关系。下面将复杂表达式转换为 cnf 形式，将参数与自由符号分开，并简化单变量参数，同时保持多变量参数不变。

def f(eq):
    from collections import defaultdict
    from sympy import to_cnf, ordered
    cnf = to_cnf(eq)
    args = defaultdict(list)
    for a in cnf.args:
        args[tuple(ordered(a.free_symbols))].append(a)
    _args = []
    for k in args:
        if len(k) == 1:
            _args.append(cnf.func(*args[k]).as_set().as_relational(k[0]))
        else:
            _args.append(cnf.func(*args[k]))
    return cnf.func(*_args)

例如：

>>> from sympy.abc import a, c
>>> f((a < 1) | ((c >= 4) & (a < 3) & (a < 12)))
(a < 3) & ((c >= 4) | (a < 1))

如果结果中出现

oo

或

-oo

并且您希望此类关系为 True，则可以将所有此类关系替换为 True，否则使变量为实值：

>>> from sympy import Dummy
>>> from sympy.abc import x

>>> (x < 3).as_set().as_relational(x)
(-oo < x) & (x < 3)
>>> _.replace(
...  lambda x: x.is_Relational and x.has(
...     S.Infinity, S.NegativeInfinity), 
...  lambda x: True)
...
x < 3

>>> r = Dummy(real=True)
>>> (x < 3).as_set().as_relational(r).subs(r, x)
x < 3

Answer 2

您可以查看 sympy 不等式求解器 中的一些选项。

我可以将

reduce_inequalities

应用于您的问题

from sympy.abc import a, c
import sympy.solvers.inequalities as neq
t = neq.reduce_inequalities([a < 12, a < 3, c >= 4])

结果

(4 <= c) & (-oo < a) & (a < 3) & (c < oo)

它也适用于一些更复杂的示例

只要每个不等式都有一个变量。