使用 google 或工具 SAT 求解器舍入 LinearExpr

Question

创建约束（在 Java 中）

IntVar x, y, z;
IntVar[] variables = new IntVar{x, y, z};
int[] multiplier = new int{2, 3, 3};
LinearExpr expression = LinearExpr.scalProd(variables, multiplier); //2x + 3y + 3z
model.addLessThan(expression, q);

其中 q 是某个给定的整数。

问题是我需要对表达式结果进行舍入。类似于：

if(expression < 25) {
    expression = 0;
} else 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;
}

因此 expression 的值（应在 addLessThan 约束中使用）是以下之一：

0, 50, 100, 150, 200, 250, 300

让我们回顾2个案例：

案例一

q = 180 和 expression = 176.

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

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

案例二

q = 210 和 expression = 218.

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

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

我怎样才能做到这一点？

Answer 1

详细说明我的评论（Python 中的代码）：

roundedExpr = model.NewIntVarFromDomain(cp_model.Domain.FromValues([0, 50, 100, 150, 200, 250, 300]), "roundedExpr")

b1 = model.NewBoolVar("< 25")
model.Add(expression < 25).OnlyEnforceIf(b1)
model.Add(roundedExpr == 0).OnlyEnforceIf(b1)
...
b7 = model.NewBoolVar(">= 275")
model.Add(expression >= 275).OnlyEnforceIf(b7)
model.Add(roundedExpr == 300).OnlyEnforceIf(b7)

model.AddBoolOr([b1, b2, b3, ..., b7])

使用 google 或工具 SAT 求解器舍入 LinearExpr

Rounding LinearExpr with google or-tools SAT solver

java

nonlinear-optimization

sat

or-tools