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

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

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

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

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

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

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

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

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

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

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

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

${\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 \фи}$

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

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

${\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})\\&\equiv (\neg x_{2}\lor p\lor q)\land (\neg p\lor x_{2})\land (\neg q\lor x_{2})\end{align}}}$

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

Тип	Операция	CNF-субвыражение
И	${\displaystyle C=A\cdot B}$	${\displaystyle ({\overline {A}}\vee {\overline {B}}\vee C)\wedge (A\vee {\overline {C}})\wedge (B\vee {\overline {C}})}$
НЕ-И	${\displaystyle C={\overline {A\cdot B}}}$	${\displaystyle ({\overline {A}}\vee {\overline {B}}\vee {\overline {C}})\wedge (A\vee C)\wedge (B\vee C)}$
ИЛИ	${\displaystyle С=А+В}$	${\displaystyle (A\vee B\vee {\overline {C}})\wedge ({\overline {A}}\vee C)\wedge ({\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}})\wedge (A\vee C)}$
XOR	${\displaystyle C=A\oplus B}$	${\displaystyle ({\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)}$
X-NOR-не	${\displaystyle C={\overline {A\oplus B}}}$	${\displaystyle ({\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, когда хотя бы некоторые из ее входов являются true, но не более двух за раз. Она реализует уравнение y = x1 · x2 + x1 · x2 + x2 · x3 . Для каждого выхода вентиля вводится переменная; здесь каждый отмечен красным:

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

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

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

Значения введенных переменных обычно отбрасываются, но их можно использовать для отслеживания логического пути в исходной схеме. Здесь, действительно, соответствует критериям исходной схемы, чтобы вывести true. Чтобы найти другой ответ, можно добавить предложение (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))\wedge ({\overline {C}}\rightarrow ({\overline {A}}\wedge {\overline {B}}))}$

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

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

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

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

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

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

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

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

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

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

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

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

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

${\displaystyle (C\rightarrow {\overline {(A\vee B)}})\wedge ({\overline {C}}\rightarrow (A\vee B))}$, , , ,${\displaystyle {\overline {\overline {({\overline {C}}\vee ({\overline {A}}\wedge {\overline {B}}))}}}\wedge (C\vee A\vee B))}$${\displaystyle {\overline {(C\wedge (A\vee B))}}\wedge (C\vee A\vee B))}$${\displaystyle {\overline {(A\wedge C)\vee (B\wedge C)}}\wedge (C\vee A\vee B))}$${\displaystyle ({\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 г.