Что означает агрегирование для проблем с SAT в SCIP?

В документе SCIP Optimization Suite 6.0 есть раздел, посвященный предварительному вычислению агрегации. Приведенный пример представляет собой линейное ограничение с двумя переменными a1x1 + a2x2 = b, где либо x1, либо x2 делается субъектом, а затем заменяется на другие ограничения. Я понимаю логику, когда это линейная программа.

Однако для проблем с SAT мой problem файл и transproblem файлы показывают следующее:

[logicor] <c301>: logicor(<x591>[B],<~x666>[B]); (This comes from problem file)
[logicor] <c302>: logicor(<~x591>[B],<x666>[B]);

преобразован в

[binary] <t_x666>: obj=-0, global bounds=[-0,1], local bounds=[-0,1], aggregated: +1<t_x591>

а также

[logicor] <c1402>: logicor(<x538>[B],<x138>[B]); (This comes from problem file)
[logicor] <c1403>: logicor(<~x538>[B],<~x138>[B]);

преобразован в

  [binary] <t_x138>: obj=-0, global bounds=[-0,1], local bounds=[-0,1], aggregated: 1 -1<t_x538>

Я не понимаю, как агрегация работает в этих двух случаях из-за ограничений логики или. Кто-нибудь, пожалуйста, объясните мне это? Спасибо!


mathematical-optimization scip sat
person Chia Teck Yan    schedule 25.03.2020    source источник

Ответы (1)


arrow_upward
0
arrow_downward

(Много догадок, так как я мало что знаю о внутренностях scip)

Пример

[logicor] <c301>: logicor(<x591>[B],<~x666>[B]); (This comes from problem file)
[logicor] <c302>: logicor(<~x591>[B],<x666>[B]);

эквивалентно (логический алгоритм):

~591 -> ~x666
x591 -> x666

Это действительно похоже на случай 2 из 4 (из presol_implics.h):

x=0 ⇒ y=lb and x=1 ⇒ y=ub : aggregate y == lb + (ub − lb)x

с участием:

lb = 0 
ub = 1

ведущие к:

aggregate y == lb + (ub − lb)x
<-> x666 == 0 + (1-0) x591 
<-> x666 == +1 x591

for comparison:
[binary] <t_x666>: obj=-0, global bounds=[-0,1], local bounds=[-0,1], aggregated: +1<t_x591>

Поэтому, если вывод scip означает, что t_x666 является замененной версией x666, это имеет для меня некоторый смысл.

Последний член агрегации также соответствует таблице истинности:

a    b    (a | ~b) & (~a | b)
0    0        1
0    1        0
1    0        0
1    1        1

-> в основном отрицательный XOR -> равенство -> истина, если оба равны

Поскольку импликационный граф - это естественная вещь для рассуждений о предложениях с двумя вариантами, я склонен сказать, что это действительно часть внутренних элементов scips, действующих здесь.

person sascha    schedule 25.03.2020