Задача Z5. Сапёр ≡

Условие

Петя изучает теорию сложности вычислений и узнал, что задача "Сапёр" является NP-полной. Так как эта задача принадлежит классу NP, её можно свести к задаче выполнимости булевых формул (SAT).

Игровое поле состоит из клеток, некоторые из которых содержат мины. Число в клетке (подсказка) показывает, сколько мин находится в соседних 8 клетках. Если в клетке число 0 - все соседние клетки безопасны.

Необходимо реализовать это сведение - преобразовать игровое поле Сапёра в булеву формулу в формате DIMACS CNF.

Формат входных данных

Первая строка содержит два целых числа через пробел: n m, где:

• n - количество строк
• m - количество столбцов

Последующие n строк содержат по m целых чисел через пробел, где:

• -1 обозначает закрытую клетку (неизвестно, есть ли мина)
• 0-8 обозначает открытую клетку с соответствующим числом

Формат выходных данных

Программа должна выводить SAT-формулу в формате DIMACS CNF:

p cnf variables clauses
clause1 0
clause2 0
...

Требования к структуре формулы

Для прохождения тестов формула должна быть детерминированной. Соблюдайте следующие правила:

1. Приоритет подсказок: генерация ограничений происходит в цикле по значению числа в клетке K от 0 до 8. Сначала обрабатываются все клетки с цифрой 0, затем с цифрой 1, и так далее до 8. Внутри группы с одинаковыми цифрами клетки обрабатываются в естественном порядке (построчно: сверху-вниз, слева-направо).
2. Нумерация переменных: переменная для закрытой клетки получает свой ID (1, 2, 3...) в тот момент, когда она впервые упоминается как сосед при формировании ограничений согласно порядку из п.1.
3. Порядок соседей: при перечислении соседей (для формирования клоуза или присвоения ID) используется геометрический порядок: от верхнего левого (-1, -1) к нижнему правому (1, 1).
4. Порядок ограничений для одной клетки:
   • Сначала выводятся условия, запрещающие ситуацию "мин больше K" (комбинации отрицательных литералов).
   • Следом выводятся условия, запрещающие ситуацию "мин меньше K" (комбинации положительных литералов).
5. Уникальность: В итоговом файле не должно быть дублирующихся строк (клоузов). Дубликаты должны быть удалены, при этом сохраняется порядок первого появления клоуза.

Ограничения

1 ≤ n, m ≤ 10

Примеры тестов

3 3
0 1 -1
1 2 -1
-1 -1 -1

p cnf 5 19
-1 -2 0
1 2 0
-3 -4 0
3 4 0
-1 -2 -3 0
-1 -2 -4 0
-1 -2 -5 0
-1 -3 -4 0
-1 -3 -5 0
-1 -4 -5 0
-2 -3 -4 0
-2 -3 -5 0
-2 -4 -5 0
-3 -4 -5 0
1 2 3 4 0
1 2 3 5 0
1 2 4 5 0
1 3 4 5 0
2 3 4 5 0

3 4
0 1 -1 -1
1 3 -1 -1
-1 -1 -1 -1

p cnf 5 19
-1 -2 0
1 2 0
-3 -4 0
3 4 0
-1 -2 -3 -4 0
-1 -2 -3 -5 0
-1 -2 -4 -5 0
-1 -3 -4 -5 0
-2 -3 -4 -5 0
1 2 3 0
1 2 4 0
1 2 5 0
1 3 4 0
1 3 5 0
1 4 5 0
2 3 4 0
2 3 5 0
2 4 5 0
3 4 5 0