Что означает агрегация для проблем SAT в SCIP? - PullRequest
Новая
       52

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

0 голосов
/ 25 марта 2020

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

Однако для проблем 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>

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

1 Ответ

0 голосов
/ 25 марта 2020

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

Пример 

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

эквивалентен (логическое значение alg): 

~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

ведущим to: 

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, это имеет некоторый смысл для меня.

Последний термин агрегации также соответствует истине- table: 

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

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

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

...