2SAT

2-SAT Выполнимость

Рассмотрим функцию, записанную в виде 2-КНФ (КНФ Крома).
2-SAT выполнимость данной функции - эта задача распределения аргументов таким образом, чтобы результат данной функции был равен 1.

Алгоритм Решения

Рассмотрим любой дизъюнкт функции: (a || b)
Несложно заметить, что это равнозначно записи !a => b и !b => a

Построим ориентированный граф, где вершинами будут аргументы и их отрицание, а ребрами будут ребра вида: !a => b и !b => a для каждого дизъюнкта функции (a || b)

Для того, чтобы данная задача 2-SAT имела решение, необходимо и достаточно, чтобы для любой переменной x из вершины x нельзя достичь !x и из вершины !x нельзя достичь x одновременно. (!x => x && x => !x)

Доказательство

Пусть 2-SAT имеет решение.
Докажем, что не может быть такого, чтобы для любой переменной x из вершины x можно достичь !x и из вершины !x можно достичь x одновременно. (!x => x && x => !x)
Тогда чтобы из !x достичь x (!x => x) x было верным, x должен быть равен 1. С другой стороны для того, чтобы из x достичь !x (!x => x) было верным, x должен быть равен 0. Отсюда следует противоречие.

Пусть для любой переменной x из вершины x нельзя достичь !x и из вершины !x нельзя достичь x одновременно.
Докажем, что этого достаточно, чтобы 2-SAT имело решение.
Пусть из !x можно достичь x, но из вершины x нельзя достичь !x. Докажем, что из x не достижимо такой y, что из y достижимо !y. (т.е. x => y => !y. (x = 1, y = 0)).
Если из x => y, то (!x || y), отсюда следует (!y => !x). Тогда x => y => !y => !x. Следовательно x => !x. Противоречие.

Ссылки

• MAXimal :: algo :: Задача 2-SAT (2-CNF)