时间戳

首页 > 解决方案 > 使用 google or-tools SAT 求解器舍入 LinearExpr

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

问题描述

我正在使用or-tools SAT solver创建一个约束（在 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个案例：

情况1

q = 180和expression = 176。

虽然条件176 < 180是true，但是在四舍五入到 176 到 200 之后，测试的条件应该是200 < 180which is false。

所以 forq = 180和expression = 176我想返回的条件false。

案例2

q = 210和expression = 218。

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

所以 forq = 210和expression = 218我想返回的条件true。

我怎样才能做到这一点？

标签： javanonlinear-optimizationor-toolssat

解决方案

详细说明我的评论（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])

推荐阅读