Превращение Цейтина

Преобразование Цейтина , альтернативно называемое преобразование Цейтина , принимает на вход произвольную комбинаторную логическую схему и создает эквивалентную булеву формулу в конъюнктивной нормальной форме (КНФ). Длина формулы линейно зависит от размера схемы. Входные векторы, которые делают выход схемы «истинным», находятся в однозначном соответствии с присваиваниями, удовлетворяющими формуле. Это сводит проблему выполнимости схем на любой схеме (включая любую формулу) к проблеме выполнимости формул 3-КНФ. Его открыл российский учёный Григорий Цейтин .

Мотивация

Наивный подход состоит в том, чтобы записать схему в виде логического выражения и использовать закон Де Моргана и распределительное свойство для преобразования ее в КНФ. Однако это может привести к экспоненциальному увеличению размера уравнения. Преобразование Цейтина выводит формулу, размер которой растет линейно относительно размера входной схемы.

Подход

Выходное уравнение — это константа 1, равная выражению. Это выражение представляет собой объединение подвыражений, где выполнение каждого подвыражения обеспечивает правильную работу одного вентиля во входной схеме. Таким образом, удовлетворение всего выходного выражения гарантирует, что вся входная схема работает правильно.

Для каждого вентиля вводится новая переменная, представляющая его выход. Небольшое предварительно рассчитанное выражение CNF, связывающее входные и выходные данные, добавляется (через операцию «и») к выходному выражению. Обратите внимание, что входными данными для этих элементов могут быть либо исходные литералы, либо введенные переменные, представляющие выходные данные подэлементов.

Хотя выходное выражение содержит больше переменных, чем входные, оно остается равновыполнимым , что означает, что оно выполнимо тогда и только тогда, когда исходное входное уравнение выполнимо. Когда найдено удовлетворительное присвоение переменных, эти присвоения введенным переменным можно просто отбросить.

К последнему предложению добавляется один литерал: выходная переменная последнего вентиля. Если этот литерал дополняется, то выполнение этого предложения приводит к тому, что выходное выражение становится ложным; в противном случае выражение становится истинным.

Примеры

Рассмотрим следующую формулу $\phi$ .

$\phi :=((p\lor q)\land r)\to (\neg s)$

Рассмотрим все подформулы (исключая простые переменные):

${\begin{aligned}&\neg s\\&p\lor q\\&(p\lor q)\land r\\&((p\lor q)\land r)\to (\neg s)\end{aligned}}$

Введите новую переменную для каждой подформулы:

${\begin{aligned}x_{1}&\leftrightarrow \neg s\\x_{2}&\leftrightarrow p\lor q\\x_{3}&\leftrightarrow x_{2}\land r\\x_{4}&\leftrightarrow x_{3}\to x_{1}\end{aligned}}$

Соедините все замены и замену на $\phi$:

$T(\phi ):=x_{4}\land (x_{4}\leftrightarrow x_{3}\to x_{1})\land (x_{3}\leftrightarrow x_{2}\land r)\land (x_{2}\leftrightarrow p\lor q)\land (x_{1}\leftrightarrow \neg s)$

Все замены могут быть преобразованы в CNF, например

${\begin{aligned}x_{2}\leftrightarrow p\lor q&\equiv (x_{2}\to (p\lor q))\land ((p\lor q)\to x_{2})\\&\equiv (\neg x_{2}\lor p\lor q)\land (\neg (p\lor q)\lor x_{2})\\&\equiv (\neg x_{2}\lor p\lor q)\land ((\neg p\land \neg q)\lor x_{2})\\&\equiv (\neg x_{2}\lor p\lor q)\land (\neg p\lor x_{2})\land (\neg q\lor x_{2})\end{aligned}}$

Подвыражения шлюза

Перечислены некоторые возможные подвыражения, которые можно создать для различных логических элементов. В выражении операции C действует как выход; в подвыражении CNF C действует как новая логическая переменная. Для каждой операции подвыражение CNF истинно тогда и только тогда, когда C придерживается контракта логической операции для всех возможных входных значений.

Тип	Операция	Подвыражение CNF
И	$C=A\cdot B$	$({\overline {A}}\vee {\overline {B}}\vee C)\wedge (A\vee {\overline {C}})\wedge (B\vee {\overline {C}})$
NAND	$C={\overline {A\cdot B}}$	$({\overline {A}}\vee {\overline {B}}\vee {\overline {C}})\wedge (A\vee C)\wedge (B\vee C)$
ИЛИ	$C=A+B$	$(A\vee B\vee {\overline {C}})\wedge ({\overline {A}}\vee C)\wedge ({\overline {B}}\vee C)$
НИ	$C={\overline {A+B}}$	$(A\vee B\vee C)\wedge ({\overline {A}}\vee {\overline {C}})\wedge ({\overline {B}}\vee {\overline {C}})$
НЕТ	$C={\overline {A}}$	$({\overline {A}}\vee {\overline {C}})\wedge (A\vee C)$
БЕСПЛАТНО	$C=A\oplus B$	$({\overline {A}}\vee {\overline {B}}\vee {\overline {C}})\wedge (A\vee B\vee {\overline {C}})\wedge (A\vee {\overline {B}}\vee C)\wedge ({\overline {A}}\vee B\vee C)$
ИСНО-ИЛИ	$C={\overline {A\oplus B}}$	$({\overline {A}}\vee {\overline {B}}\vee C)\wedge (A\vee B\vee C)\wedge (A\vee {\overline {B}}\vee {\overline {C}})\wedge ({\overline {A}}\vee B\vee {\overline {C}})$

Простая комбинаторная логика

Следующая схема возвращает true, если хотя бы некоторые из ее входных данных верны, но не более двух одновременно. Он реализует уравнение y = x1 · x2 + x1 · x2 + x2 · x3 . Для выхода каждого вентиля вводится переменная; здесь каждый отмечен красным:

Обратите внимание, что на выходе инвертора с _{x 2} входом представлены две переменные. Хотя это и избыточно, но не влияет на эквивыполнимость полученного уравнения. Теперь замените каждый элемент соответствующим подвыражением CNF:

ворота	Подвыражение CNF
ворота1	(ворота1 ∨ x1) ∧ ( ворота1 ∨ x1 )
ворота2	( ворота2 ∨ ворота1) ∧ ( ворота2 ∨ x2) ∧ ( x2 ∨ ворота2 ∨ ворота1 )
ворота3	(ворота3 ∨ x2) ∧ ( ворота3 ∨ x2 )
ворота4	( ворота4 ∨ x1) ∧ ( ворота4 ∨ ворота3) ∧ ( ворота3 ∨ ворота4 ∨ x1 )
ворота5	(ворота5 ∨ x2) ∧ ( ворота5 ∨ x2 )
ворота6	( ворота6 ∨ ворота5) ∧ ( ворота6 ∨ x3) ∧ ( x3 ∨ ворота6 ∨ ворота5 )
ворота7	(ворота7 ∨ ворота2 ) ∧ (ворота7 ∨ ворота4 ) ∧ (ворота2 ∨ ворота7 ∨ ворота4)
ворота8	(ворота8 ∨ ворота6 ) ∧ (ворота8 ∨ ворота7 ) ∧ (ворота6 ∨ ворота8 ∨ ворота7)

Последней выходной переменной является Gate8, поэтому для обеспечения того, чтобы вывод этой схемы был истинным, добавляется еще одно последнее простое предложение: (ворота8). Объединение этих уравнений приводит к окончательному варианту SAT:

(ворота1 ∨ x1) ∧ ( ворота1 ∨ x1 ) ∧ ( ворота2 ∨ ворота1) ∧ ( ворота2 ∨ x2) ∧

( x2 ∨ ворота2 ∨ ворота1 ) ∧ (ворота3 ∨ x2) ∧ ( ворота3 ∨ x2 ) ∧ ( ворота4 ∨ x1) ∧

( ворота4 ∨ ворота3) ∧ ( ворота3 ∨ ворота4 ∨ x1 ) ∧ (ворота5 ∨ x2) ∧

( ворота 5 ∨ x2 ) ∧ ( ворота 6 ∨ ворота 5) ∧ ( ворота 6 ∨ x3) ∧

( x3 ∨ ворота6 ∨ ворота5 ) ∧ (ворота7 ∨ ворота2 ) ∧ (ворота7 ∨ ворота4 ) ∧

(ворота2 ∨ ворота7 ∨ ворота4) ∧ (ворота8 ∨ ворота6 ) ∧ (ворота8 ∨ ворота7 ) ∧

(ворота6 ∨ ворота8 ∨ ворота7) ∧ (ворота8) = 1

Одним из возможных удовлетворительных назначений этих переменных является:

переменная	ценить
ворота2	0
ворота3	1
ворота1	1
ворота6	1
ворота7	0
ворота4	0
ворота5	1
ворота8	1
х2	0
х3	1
х1	0

Значения введенных переменных обычно отбрасываются, но по ним можно проследить логический путь в исходной схеме. Здесь, $(x1,x2,x3)=(0,0,1)$ действительно соответствует критериям исходной схемы для вывода истины. Чтобы найти другой ответ, предложение (x1 ∨ x2 ∨ x3 можно добавить ) и снова запустить решатель SAT.

Вывод

Представлен один из возможных вариантов получения подвыражения CNF для некоторых выбранных вентилей:

ИЛИ Ворота

Логический элемент ИЛИ с двумя входами A и B и одним выходом C удовлетворяет следующим условиям:

1. если выход C истинен, то хотя бы один из его входов A или B истинен,
2. если выход C ложен, то оба его входа A и B ложны.

Мы можем выразить эти два условия как сочетание двух импликаций:

$(C\rightarrow (A\vee B))\wedge ({\overline {C}}\rightarrow ({\overline {A}}\wedge {\overline {B}}))$

Замена импликаций эквивалентными выражениями, включающими только союзы, дизъюнкции и отрицания, дает

$({\overline {C}}\vee (A\vee B))\wedge (C\vee ({\overline {A}}\wedge {\overline {B}})),$

что уже почти находится в конъюнктивной нормальной форме . Распределение крайнего правого предложения дважды дает

$({\overline {C}}\vee A\vee B)\wedge ((C\vee {\overline {A}})\wedge (C\vee {\overline {B}})),$

и применение ассоциативности соединения дает формулу КНФ

$({\overline {C}}\vee A\vee B)\wedge (C\vee {\overline {A}})\wedge (C\vee {\overline {B}})$

НЕ ворота

Вентиль НЕ работает правильно, когда его вход и выход противоположны друг другу. То есть:

1. если выход C истинен, вход A ложен
2. если выход C ложен, вход A истинен

выразить эти условия в виде выражения, которое должно быть удовлетворено:

$(C\rightarrow {\overline {A}})\wedge ({\overline {C}}\rightarrow A)$, $({\overline {C}}\vee {\overline {A}})\wedge (C\vee A)$

НО-ворота

Вентиль NOR работает правильно, если выполняются следующие условия:

1. если вывод C истинен, то ни A, ни B не являются истинными
2. если выход C ложный, то хотя бы один из A и B был истинным

выразить эти условия в виде выражения, которое должно быть удовлетворено:

$(C\rightarrow {\overline {(A\vee B)}})\wedge ({\overline {C}}\rightarrow (A\vee B))$, ${\overline {\overline {({\overline {C}}\vee ({\overline {A}}\wedge {\overline {B}}))}}}\wedge (C\vee A\vee B))$, ${\overline {(C\wedge (A\vee B))}}\wedge (C\vee A\vee B))$, ${\overline {(A\wedge C)\vee (B\wedge C)}}\wedge (C\vee A\vee B))$, $({\overline {A}}\vee {\overline {C}})\wedge ({\overline {B}}\vee {\overline {C}})\wedge (C\vee A\vee B))$

Ссылки

• Г. С. Цейтин : О сложности вывода в исчислении высказываний. В: Слисенко А.О. (ред.) Исследования по конструктивной математике и математической логике, Часть II, Семинары по математике, стр. 115–125. Математический институт им. Стеклова (1970). Перевод с русского: Записки научных семинаров ЛОМИ 8 (1968), стр. 234–259.
• Г. С. Цейтин: О сложности вывода в исчислении высказываний. Доложено на Ленинградском семинаре по математической логике, состоявшемся в сентябре 1966 года.