Конвертировать Vertex-Total-Magi c -Labeling Задача в SAT

Question

Я и мои друзья получаем проблему из заголовка для разрешения.

Мы нашли красивый и простой в использовании SAT Solver Cryptominisat .

Мы также нашли довольно длинную статью о конвертации VTML в Sat Article . Мы сгенерируем правила / ограничения из python.

Мы действительно нашли препятствия при преобразовании всего Графа в логические правила. Мы также

c 2 na poczatku to jest Y
c 1 na początku to jest X
p cnf 188 5
c i = 1
-111 21 0
111 -21 0
c i = 2
22 -112 0
22 -21 0
-22 112 21 0
c i = 3
23 -113 0
23 -22 0
-23 113 22 0
c i = 4
24 -114 0
24 -23 0
-24 114 23 0
c i = 5
25 -115 0
25 -24 0
-25 115 24 0
c i = 6
26 -116 0
26 -25 0
-26 116 25 0
c jezeli jedno jest true to reszta nie
-21 112 0
-22 113 0
-23 114 0
-24 115 0
-25 116 0
26 0

Согласно статье, которую я написал, cnf клаусулус вручную. 2 в начале - Y,

1 - X X1,1 -> 111

Answer 1

1. Строка p объявляет 188 переменных и 5 предложений, когда имеется только 12 активных переменных и 23 предложения.

2. Решатели SAT обычно ожидайте, что переменные будут пронумерованы от 1 до N, а все переменные от 1 до N включительно появятся хотя бы один раз в предложении, а не будут случайным образом пронумерованы с большими блоками неиспользуемых идентификаторов. Решатель, вероятно, будет работать в любом случае, но использует больше памяти, чем необходимо.

3. Комментарии не должны появляться после строки p .

Кроме тех жалоб, у вас есть экземпляр SAT, который при подаче в SAT-решатель даст результат. Я ничего не знаю о маркировке вершинных полных магий c, поэтому не могу сказать, правильно ли вы закодировали реальную задачу.