Преобразование Цейтина - Tseytin transformation

Преобразование Цейтина , иначе называемое преобразованием Цейтина , принимает в качестве входных данных произвольную комбинаторную логическую схему и производит логическую формулу в конъюнктивной нормальной форме (CNF) , которую можно решить с помощью решателя CNF-SAT . Длина формулы линейна по размеру цепи. Входные векторы, которые делают выход схемы "истинным", находятся в соответствии 1 к 1 с присвоениями, которые удовлетворяют формуле. Это сводит проблему выполнимости любой схемы (включая любую формулу) к проблеме выполнимости формул 3-CNF.

Мотивация

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

Подход

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

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

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

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

Примеры

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

${\ Displaystyle \ фи: = ((п \ лор д) \ земля р) \ к (\ нег s)}$

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

${\ Displaystyle {\ begin {align} & \ neg s \\ & p \ lor q \\ & (p \ lor q) \ land r \\ & ((p \ lor q) \ land r) \ to (\ neg s) \ end {выровнен}}}$

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

${\ displaystyle {\ begin {align} 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 {align}}}$

Соедините все замены и замену для : ${\ displaystyle \ phi}$

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

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

${\ Displaystyle {\ begin {align} 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}) \\ & \ Equ (\ neg x_ {2} \ lor p \ lor q) \ land (\ нег р \ лор х_ {2}) \ земля (\ нег д \ лор х_ {2}) \ конец {выровнено}}}$

Подвыражения ворот

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

Тип	Операция	CNF подвыражении
А ТАКЖЕ	${\ Displaystyle C = A \ cdot B}$	${\ Displaystyle ({\ overline {A}} \ vee {\ overline {B}} \ vee C) \ клин (A \ vee {\ overline {C}}) \ клин (B \ vee {\ overline {C} })}$
NAND	${\ displaystyle C = {\ overline {A \ cdot B}}}$	${\ Displaystyle ({\ overline {A}} \ vee {\ overline {B}} \ vee {\ overline {C}}) \ клин (A \ vee C) \ клин (B \ vee C)}$
ИЛИ	${\ displaystyle C = A + B}$	${\ displaystyle (A \ vee B \ vee {\ overline {C}}) \ клин ({\ overline {A}} \ vee C) \ клин ({\ overline {B}} \ vee C)}$
НИ	${\ displaystyle C = {\ overline {A + B}}}$	${\ displaystyle (A \ vee B \ vee C) \ wedge ({\ overline {A}} \ vee {\ overline {C}}) \ wedge ({\ overline {B}} \ vee {\ overline {C}) })}$
НЕТ	${\ displaystyle C = {\ overline {A}}}$	${\ Displaystyle ({\ overline {A}} \ vee {\ overline {C}}) \ клин (A \ vee C)}$
XOR	${\ displaystyle C = A \ oplus B}$	${\ displaystyle ({\ overline {A}} \ vee {\ overline {B}} \ vee {\ overline {C}}) \ клин (A \ vee B \ vee {\ overline {C}}) \ клин ( A \ vee {\ overline {B}} \ vee C) \ wedge ({\ overline {A}} \ vee B \ vee C)}$
XNOR	${\ displaystyle C = {\ overline {A \ oplus B}}}$	${\ displaystyle ({\ overline {A}} \ vee {\ overline {B}} \ vee C) \ клин (A \ vee B \ vee C) \ клин (A \ vee {\ overline {B}} \ vee {\ overline {C}}) \ wedge ({\ overline {A}} \ vee B \ vee {\ overline {C}})}$

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

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

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

ворота	CNF Подвыражение
gate1	(ворота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, поэтому для обеспечения того, чтобы выход этой схемы был истинным, добавляется одно последнее простое предложение: (gate8). Объединение этих уравнений приводит к последнему экземпляру SAT:

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

( x2 ∨ gate2 ∨ gate1 ) ∧ (gate3 ∨ x2) ∧ ( gate3 ∨ x2 ) ∧ ( gate4 ∨ 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
gate1	1
ворота6	1
ворота7	0
ворота4	0
ворота5	1
ворота8	1
x2	0
x3	1
x1	0

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

Вывод

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

ИЛИ Ворота

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

1. если выход C истинен, то по крайней мере один из его входов A или B истинен,
2. если выход C ложен, то оба его входа A и B ложны.

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

${\ displaystyle (C \ rightarrow (A \ vee B)) \ клин ({\ overline {C}} \ rightarrow ({\ overline {A}} \ wedge {\ overline {B}}))}$

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

${\ displaystyle ({\ overline {C}} \ vee (A \ vee B)) \ клин (C \ vee ({\ overline {A}} \ клин {\ overline {B}})),}$

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

${\ displaystyle ({\ overline {C}} \ vee A \ vee B) \ клин ((C \ vee {\ overline {A}}) \ клин (C \ vee {\ overline {B}})),}$

и применение ассоциативности конъюнкции дает формулу CNF

${\ displaystyle ({\ overline {C}} \ vee A \ vee B) \ клин (C \ vee {\ overline {A}}) \ клин (C \ vee {\ overline {B}})}$

НЕ ворота

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

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

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

${\ Displaystyle (C \ rightarrow {\ overline {A}}) \ клин ({\ overline {C}} \ rightarrow A)}$, ${\ Displaystyle ({\ overline {C}} \ vee {\ overline {A}}) \ клин (C \ vee A)}$

NOR Gate

Вентиль ИЛИ-НЕ работает должным образом при соблюдении следующих условий:

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

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

${\ displaystyle (C \ rightarrow {\ overline {(A \ vee B)}}) \ клин ({\ overline {C}} \ rightarrow (A \ vee B))}$, , , ,${\ Displaystyle {\ overline {\ overline {({\ overline {C}} \ vee ({\ overline {A}} \ wedge {\ overline {B}}))}}} \ клин (C \ vee A \ vee B))}$${\ Displaystyle {\ overline {(С \ клин (А \ Ви В))}} \ клин (С \ Ви А \ Ви В))}$${\ Displaystyle {\ overline {(А \ клин С) \ Ви (В \ клин С)}} \ клин (С \ Ви А \ Ви В))}$${\ displaystyle ({\ overline {A}} \ vee {\ overline {C}}) \ клин ({\ overline {B}} \ vee {\ overline {C}}) \ клин (C \ vee A \ vee Б))}$

использованная литература

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