Метод линейной резолюции

Линейным выводом из множества дизъюнктов M назовем конечную последовательность дизъюнктов D ₁, D ₂, … D_i, в которой D ₁ принадлежит M, а каждый последующий дизъюнкт D_i (i =2,…, m) является резольвентой дизъюнкта D_{i -1} и одного из дизъюнктов совокупности S_{i -1}= M { D ₂} { D ₃} … { D_{i -2}}. При этом в процессе вывода каждый очередной дизъюнкт D_i именуется центральным дизъюнктом, а дизъюнкт, выбираемый из совокупности S_{i -1}, боковым дизъюнктом.

Пример 6. Методом линейной резолюции требуется доказать противоречивость следующей совокупности дизъюнктов (см. пример 5):

1) A А'; 2) В В'; 3) A B; 4) A В';

5) В А'; 6) А' В'; 7) В' А'.

Реализуемый методом линейной резолюции вывод пустого дизъюнкта представим следующей схемой:

В А' A B

А' В' A А'

A В' А' В'

В^' В В'

A B В

А' A A

А' B А'

В B

ÿ

Теорема о полноте принципа линейной резолюции. Если конечная совокупность дизъюнктов противоречива, то данный факт может быть доказан методом линейной резолюции.

Отметим, что если в методе линейной резолюции боковой дизъюнкт брать только из исходного множества M, то, существенно упрощаясь, он теряет свойство полноты. Перебором вариантов можно показать, что таким образом нельзя доказать противоречивость совокупности дизъюнктов { Р Q, Р Q, Р Q, Р Q } (см. пример 3).

Верхняя оценка временной вычислительной сложности алгоритма проверки непротиворечивости КНФ, основанного на принципе линейной резолюции, остается экспоненциальной, что связано с полнотой данного принципа и NP - полнотой задачи выполнимости КНФ.

Дата добавления: 2015-06-27