使用 google or-tools SAT 求解器舍入 Non-LinearExpr [英] Rounding Non-LinearExpr with google or-tools SAT solver

问题描述

使用谷歌或工具的CP-SAT我'我正在尝试编写此约束:

Using CP-SAT of google or-tools I'm trying to write this constraint:

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

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

Where q is a simple integer.

问题是我需要将等式的右侧四舍五入(我们称之为 expression)如下:

The thing is I need to round the right side of the equation (let's call it expression) as follows:

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;
}

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

So I need to round the expression

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

以便它获得以下值之一:

So that it gets one of the following values:

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

---

让我们回顾两个案例:

---

Let's review 2 cases:

案例 1

q = 180 和 expression = 176.

虽然条件180 >= 176是true，但是在将176四舍五入到200之后，测试条件应该是180 >= 200> 这是 false.

Although the condition 180 >= 176 is true, after rounding up 176 to 200 the tested condition should be 180 >= 200 which is false.

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

So for q = 180 and expression = 176 I would like the condition to return false.

案例 2

q = 210 和 expression = 218.

虽然条件210 >= 218是false，但是在将218四舍五入到200之后，测试条件应该是210 >= 200 这是 true.

Although the condition 210 >= 218 is false, after rounding down 218 to 200 the tested condition should be 210 >= 200 which is true.

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

So for q = 210 and expression = 218 I would like the condition to return true.

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

I got a great answer here for resolving this challenge over a linear expression but now I need to resolve it for a non-linear expression.

有什么建议吗?

推荐答案

让我们改写

您有一个整数变量 e，其值在 0 到 300 之间.你想把它四舍五入到最接近的 50 的倍数

you have an integer variable e with a value between 0 and 300. You want to round it to the nearest multiple of 50

如果你这样做:

(e div 50) * 50

您将得到小于或等于 e

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

要获得最接近的舍入，您需要在除法之前将 25 添加到 e

To get a round to nearest, you need to add 25 to e before the division

((e + 25) div 50) * 50

哪个将进行正确的舍入

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

使用正确的 or-tools CP-SAT python 代码:

with the correct or-tools CP-SAT python code:

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的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！