使用 google or-tools SAT 求解器舍入 Non-LinearExpr

Question

使用 CP-SAT of google or-tools 我正在尝试编写此约束：

q >= (50x + 100y + 150z + 200k + 250p + 300v) / (x + y + z + k + p + v)

其中 q 是一个简单的整数。

问题是我需要将等式的右边四舍五入（我们称之为 expression），如下所示：

if(expression < 75) {
    expression = 50;
} else if(expression < 125) {
    expression = 100;
} else if(expression < 175) {
    expression = 150;
} else if(expression < 225) {
    expression = 200;
} else if(expression < 275) {
    expression = 250;
} else {
    expression = 300;
}

所以我需要对表达式进行舍入

(50x + 100y + 150z + 200k + 250p + 300v) / (x + y + z + k + p + v)

使其获得以下值之一：

{50, 100, 150, 200, 250, 300}

让我们回顾2个案例：

案例一

q = 180 和 expression = 176.

虽然条件 180 >= 176 是 true，但在将 176 向上舍入到 200 后测试的条件应该是 180 >= 200 即 false.

所以对于 q = 180 和 expression = 176 我希望条件为 return false.

案例二

q = 210 和 expression = 218.

虽然条件 210 >= 218 是 false，但在将 218 向下舍入到 200 后测试的条件应该是 210 >= 200 即 true.

所以对于 q = 210 和 expression = 218 我希望条件为 return true.

我得到了一个很好的答案来解决线性表达式的这个挑战，但现在我需要解决一个非线性表达式的问题。

有什么建议吗？

Answer 1

如果 a 和 b 为正则

a div b >= q

相当于

a >= q * b

现在，您的示例没有指定如何舍入（最近或向下）

如果要向下取整

q * (x + y + z + k + p + v) <= (50x + 100y + 150z + 200k + 250p + 300v)

如果要四舍五入，需要在合适的地方加上q/2

 q * (x + y + z + k + p + v) <= (50x + 100y + 150z + 200k + 250p + 300v + q / 2)

现在，如果你想要另一个方向

a div b <= q

相当于

a <= q * b + q - 1

其余变换同上

Answer 2

让我们换个说法

你有一个整型变量 e，其值介于 0 到 300 之间。你想将它四舍五入到最接近的 50

的倍数

如果你这样做：

(e div 50) * 50

你将得到小于或等于50的最大倍数e

(70 / 50) * 50 -> 50
(99 / 50) * 50 -> 50
(102 / 50) * 50 -> 100

要得到最接近的一轮，需要在除法前e加上25

((e + 25) div 50) * 50

哪个会进行正确的舍入

((70 + 25) / 50) * 50 -> 50
((99 + 25) / 50) * 50 -> 100
((102 + 25) / 50) * 50 -> 100

使用正确的或工具 CP-SAT python 代码：

numerator = model.NewIntVar(...)
model.Add(numerator == 50x + 100y + 150z + 200k + 250p + 300v)
denom = model.NewIntVar(...)
model.Add(denom == 50x + 100y + 150z + 200k + 250p + 300v)
e = model.NewIntVar(0, 300, 'e')
model.AddDivisionEquality(e, numerator, denom)

shifted_e = model.NewIntVar(25, 325, 'shifted_e')
model.Add(shifted_e == e + 25)
multiple_of_fifty = model.NewIntVar(0, 6, 'multiple_of_fifty')
model.AddDivisionEquality(multiple_of_fifty, shifted_e, 50)
result = model.NewIntVar(0, 300, 'result')
model.Add(result = multiple_of_fifty * 50)

使用 google or-tools SAT 求解器舍入 Non-LinearExpr

Rounding Non-LinearExpr with google or-tools SAT solver

optimization

nonlinear-optimization

or-tools

sat