假设符号是整数，简化不等式表达式答案

【问题标题】：Simplify an expression with inequalities assuming a symbol is an integer假设符号是整数，简化不等式表达式
【发布时间】：2018-01-04 18:12:11
【问题描述】：

我正在使用 SymPy 创建 Kakuro 求解器，但我无法强制要求符号必须是整数。到目前为止，我得到了一个不等式表达式，如下所示：

((1 <= x) & (x < 3/2)) | ((3/2 < x) & (x < 2))

符号x 应该等于1，因此表达式是正确的，因为1 是唯一可能的整数。

如何强制x 为整数？

我知道 SymPy 中有可用的丢番图求解器，但它们似乎只处理方程，而不是不等式。我尝试使用以下方法创建符号：

x = Symbol('x', integer=True)

但没有运气。

【问题讨论】：

标签： sympy

【解决方案1】：

似乎没有内置方法，但我编写了一个函数来简化您提到的那种关系，假设我们使用整数。

重写规则有八种：例如x <= number替换为x <= floor(number)，x < number替换为x <= ceiling(number) - 1等。

应用这些规则后，表达式的任何剩余And 部分都将服从reduce_inequalities。示例：

expr = ((1 <= x) & (x < 3 / 2)) | ((3 / 2 < x) & (x < 2))
simplify_integer_relation(expr)   # returns Eq(x, 1)

警告：重写规则假设我们不会在表达式中执行类似x/2 的操作，从而创建一个未知的小数。假设是所有涉及未知数的都是整数。

代码：

def simplify_integer_relation(expr):
    rewrite_rules = {
        GreaterThan: {
            "lhs": lambda z: floor(z),
            "rhs": lambda z: ceiling(z),
            "rel": GreaterThan,
        },
        LessThan: {
            "lhs": lambda z: ceiling(z),
            "rhs": lambda z: floor(z),
            "rel": LessThan,
        },
        StrictGreaterThan: {
            "lhs": lambda z: ceiling(z) - 1,
            "rhs": lambda z: floor(z) + 1,
            "rel": GreaterThan,
        },
        StrictLessThan: {
            "lhs": lambda z: floor(z) + 1,
            "rhs": lambda z: ceiling(z) - 1,
            "rel": LessThan,
        },
    }

    for rel in rewrite_rules:
        rule = rewrite_rules[rel]
        for atom in expr.atoms(rel):
            if atom.lhs.is_number:
                new_atom = rule["rel"](rule["lhs"](atom.lhs), atom.rhs)
                expr = expr.subs(atom, new_atom)
            elif atom.rhs.is_number:
                new_atom = rule["rel"](atom.lhs, rule["rhs"](atom.rhs))
                expr = expr.subs(atom, new_atom)

    for system in expr.atoms(And):
        expr = expr.subs(system, reduce_inequalities(system.args))

    return expr

【讨论】：