Н. Ф. (далее ДНФ);

n блок упрощения ДНФ;

n блок работы собственно обратного метода.

Продемонстрируем работу каждого блока подробнее.

Обратный метод С.Ю. Маслова работает с формулой, представленной в виде дизъюнктивной нормальной формы (ДНФ), поэтому необходимо преобразование введенной формулы. Блок перевода в ДНФ строит по древесному представлению формулы ее ДНФ по оригинальному алгоритму, более подробно изложенному в [19, 20]. Главное отличие данного метода от других алгоритмов в том, что он не строит полноценную ДНФ, а строит свернутую форму ДНФ — свертку ДНФ. Результат работы этого алгоритма (первого блока программы) можно продемонстрировать на простом примере (пример 1).

Пусть нам дана следующая формула (aЪb) & (~aЪbЪ~c). Здесь знак ~ обозначает отрицание, & — конъюнкцию, Ъ — дизъюнкцию. При применении стандартного алгоритма, использующего правила де Моргана получим следующую ДНФ D1: (a&~a) Ъ (a&b) Ъ (a&~c) Ъ (b&~a) Ъ (b&b) Ъ (b&~c).

При применении нашего оригинального алгоритма мы получим следующую свертку ДНФ:

~c (с 1 (с шагом 3) до 6)

b (с 2 (с шагом 3) до 6)

~a (с 3 (с шагом 3) до 6)

b (с 1 до 3)

a (с 4 до 6)

Первая запись свертки ДНФ означает следующее. Литера ~c (литера с отрицанием) встречается в первом дизъюнкте, и далее она встречается в каждом последующем третьем дизъюнкте (в каждом последующем дизъюнкте с шагом 3) до дизъюнкта не превышающего номера 6 (можно отметить, что представленная выше свертка ДНФ показывает, что число дизъюнктов данной ДНФ не более 6), т.е. литера ~c встречается в дизъюнктах 1 и 4, а следующий третий дизъюнкт имеет номер 4+3=7, который больше 6, что свидетельствует о том, что литера ~c не встречается более в данной ДНФ (соответственно вторая (третья) строка свертки означает, что литера b (~a) встречается во втором (третьем) дизъюнкте, и далее она встречается в каждом последующем третьем дизъюнкте, т.е. в дизъюнкте 5 (6). Четвертая (пятая) запись свертки a(4 до 6) [b (с 1 до 3)] означает, что литера a [b] встречается в дизъюнктах с 4 по 6 [c 1 по 3] включительно. Тем самым, представленную выше свертку ДНФ можно развернуть в полноценную ДНФ следующего вида: (b&~c) Ъ (b&b) Ъ (b&~a) Ъ (a&~c) Ъ (a&b) Ъ (a&~a), что с точностью до перестановки дизъюнктов совпадает с D1, построенной с помощью стандартного преобразования формул в ДНФ .

Для наглядности описания двух последующих блоков программы (блока упрощения ДНФ и блока работы собственно обратного метода) рассмотрим еще один пример (пример 2), с помощью которого попробуем рассказать о наиболее существенных моментах работы алгоритма.

Пример 2. Пусть необходимо проверить формулу D2 :
~c Ъ (b&a) Ъ (~a&c&d) Ъ (~b&~d) Ъ (~b&d) Ъ (~a&c&~d ) Ъ (~c&x&y)
Отметим, что эта формула представляет собой ДНФ и поэтому в данном случае можно опустить работу первого блока (см. пример 1).
Блок упрощения опирается на [20] и производит следующие действия:

1. Если в ДНФ имеются однолитерные дизъюнкты (ОД) p и ~p, то ДНФ общезначима;

2. Если некоторая переменная входит в ДНФ с одним знаком, то удаляем все дизъюнкты, содержащие эту переменную;

3. Если в ДНФ имеется какой-то однолитерный дизъюнкт p то выполняем следующие действия:

· удаляем все дизъюнкты вида p & … (правило поглощения);

· все дизъюнкты вида ~p & s & … заменяем на дизъюнкты вида s & …, а после этого удаляем сам однолитерный дизъюнкт p (правило удаления однолитерных дизъюнктов).

В нашем случае, поскольку в D2 переменные x и y входят только положительно, то по правилу 2 исключаем из рассмотрения дизъюнкт 7; а поскольку в D2 имеется однолитерный дизъюнкт ~c, то по правилу 3 из третьего и шестого дизъюнктов удаляется литера c, а потом первый дизъюнкт удаляется из формулы. В итоге имеем формулу D 2.1:
(~a&d) Ъ (b&a) Ъ (~a&~d ) Ъ (~b&~d) Ъ (~b&d)

После этого начинает работу блок обратного метода. Прежде чем описать его работу, изложим вкратце суть метода.

Обратный метод оперирует с наборами. Набор имеет вид [i/k, j/l, …] (m, n, …), где i, j, … — номера дизъюнктов в ДНФ, а k, l — номера литер в i и j дизъюнктах соответственно. Числа m, n образуют зависимость набора и представляют собой номера дизъюнктов. В программе есть база данных, в которой хранятся все наборы. Эту базу в дальнейшем мы будем называть базой наборов.

Собственно обратный метод состоит в следующем. Мы выбираем из базы наборов ряд наборов вида [i/1, …] (…), [i/2 ,…] (…), …, [i/n, …] (…), где n — длина i-го дизъюнкта. Затем мы строим новый набор, в котором присутствуют все члены всех выделенных наборов, кроме членов вида i/k, а зависимость представляет собой объединение всех зависимостей плюс элемент i. Это и есть основное правило работы алгоритма — правило склейки, соответствующее правилу Б обратного метода. При этом должен выполняться ряд требований на наборы. Если в процессе многократного применения данного правила удается вывести пустой набор (т.