Округление LinearExpr с помощью SAT-решателя google or-tools

Я создаю ограничение (на Java), используя or-tools SAT solver:

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 < 180, то есть false.

Итак, для q = 180 и expression = 176 я хотел бы, чтобы условие возвращало false.

Случай 2

q = 210 и expression = 218.

Хотя условие 218 < 210 равно false, после округления 218 до 200 проверяемое условие должно быть 200 < 210, то есть true.

Итак, для q = 210 и expression = 218 я хотел бы, чтобы условие возвращало true.

Как я могу этого добиться?


java or-tools nonlinear-optimization sat
person forhas    schedule 29.06.2020    source источник
comment
Я думаю, вы могли бы создать логическое значение для каждого случая, создать еще одну intvar и установить это значение на основе этого, хотя должен быть лучший способ   -  person Stradivari    schedule 30.06.2020
comment
@Stradivari Я только что обновил вопрос двумя примерами. Я не уверен, что понимаю тебя   -  person forhas    schedule 30.06.2020

Ответы (1)


arrow_upward
1
arrow_downward

Чтобы уточнить мой комментарий (код на 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])
person Stradivari    schedule 30.06.2020
comment
Спасибо за это, мне удалось это реализовать. Вы случайно не знаете, как я могу реализовать такое решение, если выражение нелинейное? Я задал его отдельным вопросом: stackoverflow.com/questions/62804600/ - person forhas; 09.07.2020