Изменения
→КНФ в форме Крома
*Существует алгоритм, который за полиномиальное время проверяет, что функцию, заданную в форме Крома можно удовлетворить(т.е КНФ в форме Крома не является тождественным <tex>0</tex>).
Для начала приведем данное выражение к импликативной форме следующим образом: заметим, что выражение вида <tex> a \vee b </tex> эквивалентно <tex> \neg a \Rightarrow b \vee \neg b \Rightarrow a </tex>. Это можно воспринимать следующим образом: если есть выражение <tex> a \vee b </tex>, и нам необходимо добиться обращения его в <tex> true </tex> то, если <tex> a = true </tex>, <tex> b </tex> должно быть равно <tex> false </tex> и наоборот. Построим граф импликаций, для каждой переменной в паре будет по две вершины (обозначим их <tex> x </tex> и <tex> \neg x </tex>). Рёбра в графе будут соответствовать импликативным связям. Например, для формулы вида: <tex> (a \vee b) \wedge (a \vee \neg b) </tex> граф импликаций будет содержать следующие ориентированные ребра: <tex> \neg a \rightarrow b, \neg b \rightarrow a, \neg b \rightarrow \neg c, c \rightarrow b </tex>. Заметим, что если для какой-то вершины <tex> x </tex> выполняется, что из <tex> x </tex> достижима <tex> \neg x </tex>, а из <tex> \neg x </tex> достижима <tex> x </tex>, то задача не имеет решения.Это следует из того, что какое бы значение для переменной <tex> x </tex> мы бы ни выбрали, мы всегда придём к противоречию, что должно быть выбрано и обратное ему значение. Условие не существования таких вершин является необходимым и достаточным для решения данной задачи. Переформулируем утверждение в терминах теории графов: для решения данной задачи необходимо и достаточно, чтобы <tex> \forall x </tex> вершины <tex> x </tex> и <tex> \neg x </tex> находились в разных компонентах сильной связности графа импликаций.
*Функцию <tex>F</tex> можно задать в форме Крома <tex> \iff </tex> выполнено следующее следствие:
