S4 (x5 — 0) = 0.

На основе унарной операции конкретизации, примененной несколько раз к различным переменным, естественным образом вводится многоместная операция. Пример обозначения конкретизации трех переменных: S (x1 , x2 , x5 — 0, 1, 0). Далее будем считать, что процедура очищения СКТ автоматически выполняется после операций пересечения и конкретизации; эти операции приводят к образованию подструктур (ПС).

Подструктура S СКТ S представляет собой СКТ, составленную из подмножества согласованных по ярусам строк S (обозначение операции: S <z S). Подчеркнем, что в подструктуре, как и в любой непустой СКТ, должны присутствовать n - 2 яруса. Элементарной назовем СКТ, содержащей по одной строке на каждом из ярусов. Элементарной СКТ соответствует единственная конкатенация строк и, соответственно, один набор значений переменных.

Из сказанного следует, что по заданному множеству наборов значений переменных может быть синтезирована СКТ, содержащая эти наборы: для этого достаточно объединить соответствующие элементарные СКТ. Нетрудно видеть, что при объединении СКТ (не только элементарных) в результирующей структуре, помимо СКТ-операндов, появляются, в общем случае, новые (побочные) подструктуры, которые будут играть важную роль в последующем анализе.

Введем на множестве СКТ S1, S2 , ... , Sq , построенных на основе различных перестановок переменных, многоместную операцию унификации, которая включает несколько правил совместного преобразования структур:

1.Если некоторая переменная xj = 0 или xj = 1 хотя бы в одной СКТ Sp (1 < j < n , 1 < p < q), то все строки, содержащие инверсное значение указанной переменной, удаляются из всех унифицируемых СКТ.

2.Если две переменные xj и xr присутствуют (в любом порядке) в компактных тройках двух или более унифицируемых СКТ, то сочетания значений этих переменных должны быть общими во всех таких СКТ. Все строки, не отвечающие этому требованию, удаляются из СКТ.

3.Если три переменные xj , xr и xt составляют (в любом порядке) компактные тройки в двух или более унифицируемых СКТ, то сочетания значений этих переменных должны быть общими во всех таких СКТ. Все строки, не отвечающие этому требованию, удаляются из СКТ.

4.Удаление строк из СКТ согласно правилам 1 - 3 всегда сопровождается очищением соответствующих структур.

При унификации возникают варианты получения пустого множества структур в следующих случаях: (*) некоторый ярус хотя бы в одной СКТ оказывается пустым; (**) существует "конфликт" константных значений для переменной xj хотя бы в двух различных СКТ, т. е. xj = 0 в одной из них и xj = 1 - в другой; (***) хотя бы одна СКТ пуста изначально (тривиальный случай). Таким образом, унифицированные СКТ могут быть пустыми либо непустыми только одновременно.

3. Декомпозиция формулы

Для решения задачи 3-ВЫП в общем случае используем декомпозицию формулы: F = F1&F2& ... &Fk , при которой каждая формула Fr (r = 1, ... , k ; k < m) сопряжена с собственной перестановкой переменных Pr = <xr1, ... , xrn) и представлена в виде ФКТ.

Декомпозиция может быть реализована различными алгоритмами полиномиальной сложности, сводящимися к перебору строк табличной формулы F и формированию подходящих перестановок таким образом, что группы строк, относящиеся к каждой перестановке, образуют компактные тройки. Нетрудно заключить, что значение k (число ФКТ) находится в пределах Tw/(n - 2)1 < k < m , где w - число групп термов в F, содержащих одинаковые переменные. При "идеальных" исходных данных задачи k = 1; предельный случай k = m связан с формированием отдельной перестановки переменных для каждого терма исходной формулы. Заметим, что минимизация числа ФКТ при декомпозиции не является принципиальной.

ФКТ преобразуются в k структур компактных троек: S1 , ... , Sk , после чего решение задачи 3-ВЫП в общем случае сводится к вопросу: существует ли непустое пересечение множеств наборов, закодированных в СКТ, которые построены на основе несовпадающих перестановок переменных? Цель состоит в ответе на этот вопрос, т. е. установлении факта существования или отсутствия совместных выполняющих наборов (СВН) для k формул компактных троек, без генерирования самих наборов, имеющего следствием в общем случае экспоненциальную сложность вычислений.

В качестве примера для иллюстрации теоретических построений (не ограничивающего общность рассуждений) рассмотрим формулу F , представленную таблицей 1.

Таблица 1. Исходная формула F

СКТ1 (S1)

Таблица 2. Структуры компактных троек

СКТ2 (S2)

СКТ3 (S3)

Оптимальная декомпозиция формулы, приведенной в таблице 1, базируется на трех перестановках переменных и является основой для формирования трех структур компактных троек S1, S2 и S3 (таблица 2).

4. Решение задачи о существовании совместных выполняющих наборов для двух СКТ

Ключевым является метод решения задачи о существовании СВН для двух СКТ (назовем их S1 и S2), основанных на несовпадающих перестановках переменных. Предварительный этап решения заключается в унификации S1 и S2 , так как унификация по принципу действия сохраняет в структурах-операндах все существующие СВН и одновременно минимизирует упомянутые структуры по числу элементов (строк). Для унифицированных СКТ сохраним первоначальные обозначения, подчеркнув тем самым, что унификация заключается в замещении исходных СКТ эквивалентными по критерию включения СВН структурами. В нашем примере унифицированные структуры для СКТ S1 и S2 , взятых из таблицы 2, представлены таблицей 3.