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

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

0 голосов
/ 09 июля 2020

Используя CP-SAT из 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 случая:

Случай 1

q = 180 и expression = 176.

Хотя условие 180 >= 176 равно true, после округления от 176 до 200 проверяемое условие должно быть 180 >= 200, что равно false.

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

Случай 2

q = 210 и expression = 218.

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

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

У меня есть отличный ответ здесь для решения этой проблемы над линейным выражением, но теперь мне нужно решить эту проблему для нелинейного выражения.

Есть предложения?

Ответы [ 2 ]

2 голосов
/ 09 июля 2020

Давайте перефразируем

у вас есть целочисленная переменная e со значением от 0 до 300. Вы хотите округлить ее до ближайшего кратного 50

, если вы это сделаете: 

(e div 50) * 50

вы получите максимальное кратное 50 меньше или равно e

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

Чтобы округлить до ближайшего, вам нужно добавить 25 к e перед делением 

((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 код: 

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)
1 голос
/ 09 июля 2020

, если 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

Остальная часть преобразования такая же.

...