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

Условие

Петя изучает теорию сложности вычислений и узнал, что задача "Сапёр" является 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 ≤ n, m ≤ 10

Гарантируется, что входные данные корректны

В SAT формулу включаются только те закрытые клетки, которые граничат с открытыми клетками, содержащими числа. Остальные закрытые клетки игнорируются при построении формулы.

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

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