체이틴 변환

Tseytin 변환은 Tseitin 변환으로, 임의의 조합 논리회로를 입력으로 하여 CNF-SAT 솔버에 의해 해결할 수 있는 결합정규형(CNF)의 부울식을 생성합니다.공식의 길이는 회로 크기에 따라 선형입니다.회로 출력을 "참"으로 만드는 입력 벡터는 공식을 만족시키는 할당과 1 대 1로 대응합니다.이것에 의해, 모든 회로(모든 공식 포함)에서의 회로 만족도의 문제가 3-CNF 공식에서의 만족도의 문제로 경감됩니다.

동기

단순한 접근방식은 회로를 부울식으로 쓰고 De Morgan의 법칙과 분배 속성을 사용하여 CNF로 변환하는 것입니다.그러나 이로 인해 방정식 크기가 기하급수적으로 증가할 수 있습니다.Tseytin 변환은 입력 회로에 비해 크기가 선형으로 증가하는 공식을 출력합니다.

접근

출력 방정식은 식과 동일한 상수 1 집합입니다.이 식은 서브 표현의 조합으로, 각 서브 표현의 만족도에 따라 입력 회로 내의 단일 게이트가 올바르게 동작합니다.따라서 출력식 전체가 만족스러우면 입력 회로 전체가 올바르게 동작합니다.

각 게이트에 대해 게이트의 출력을 나타내는 새로운 변수가 도입됩니다.입력과 출력을 관련짓는 미리 계산된 CNF 식이 출력식에 ("and" 연산을 통해) 추가됩니다.이러한 게이트에 대한 입력은 원본 리터럴 또는 하위 게이트의 출력을 나타내는 도입된 변수일 수 있습니다.

출력식이 입력식보다 더 많은 변수를 포함하지만, 이는 원래 입력 방정식이 만족스러운 경우에만 만족할 수 있음을 의미합니다.만족스러운 변수 할당이 발견되면 도입된 변수에 대한 이러한 할당은 간단히 폐기될 수 있습니다.

final 절에는 단일 리터럴(final gate의 출력 변수)이 추가됩니다.이 리터럴이 보완되면 이 절이 충족되면 출력식이 false가 됩니다.그렇지 않으면 식이 true가 됩니다.

예

다음 수식 "\$displaystyle\phi"$를 고려합니다$.$

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

모든 보조 공식(단순 변수 제외)을 고려합니다.

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

각 보조 공식에 대해 새 변수 도입:

${\displaystyle {displaystyle {s}x_{1}&\left rightarrow p\lor q\x_{3}&\left rightarrow x_{2}&\left rightarrow x_{3}&\left rightarrow x_{3}&\led} 정렬$

$모든{\displaystyle }$ 치환과 $§(\displaystyle\phi$

$(\displaystyle T(\phi):=x_{4}\land (x_{4}\왼쪽 화살표 x_{3}\to x_{1})\land (x_{3}\왼쪽 화살표 x_{2}\land r)\land (x_{2}\왼쪽 화살표 p\lor q)\land (x_{1}\왼쪽 화살표 \neg s})$

모든 치환은 예를 들어 CNF로 변환할 수 있습니다.

${\displaystyle{\begin{정렬}x_{2}\leftrightarrow p\lor q&,\equiv(x_{2}\to(p\lor q))\land((p\lor q)\to x_{2})\\&, \equiv(\neg x_{2}\lorp\lor q)\land(\neg(p\lor q)\lor x_{2})\\&, \equiv(\neg x_{2}\lorp\lor q)\land((\neg p\land \neg q)\lor x_{2})\\&, \equiv(\neg x_{2}\lorp\lor q)\land(\neg p\lor x_{2})\land(\neg q\lor x_{2})\.end{정렬}}}$

게이트 하위 표현식

다양한 로직 게이트에 대해 작성할 수 있는 서브 표현식의 일부를 나타냅니다.연산식에서는 C가 출력으로 동작합니다.CNF 서브식에서는 C가 새로운 부울 변수로 동작합니다.각 연산에 대해 CNF 하위 표현식은 C가 가능한 모든 입력 값에 대해 부울 연산의 계약을 준수하는 경우에만 True입니다.

유형	작동	CNF 서브 표현식
그리고.	${\displaystyle C=A\cdot B}$	$\displaystyle({\overline {A}}\vee C}\wedge(A\vee {C})\wedge(B\vee {C})\veee$
낸드	${\displaystyle C=오버라인 {A\cdot B}}$	$\displaystyle({\overline {A}}\veee {B}}\veee\wedge(A\vee C)\wedge(B\vee C)}$
또는	${\displaystyle C=A+B}$	${\displaystyle(A\vey B\veee {C})\wedge(\overline {A}\vee C)\wedge(\overline {B}\vee C)}$
도 아니다	${\displaystyle C=오버라인 {A+B}}$	${\displaystyle(A\vee C)\wedge(\overline {A}\vee {C})\wedge(\overline {B}\vee {C})}$
것은 아니다.	${\displaystyle C=오버라인 {A}}$	$\displaystyle({\overline {A}}\veee {C})\wedge(A\vee C)}$
XOR	${\displaystyle C=A\oplus B}$	${\displaystyle({\overline {A}}\vee {C}})\wedge(A\vee B\vee {C})\wedge(\overline {A}\vee C})\wedge(\verline {A}\vee C})$
XNOR	${\displaystyle C=오버라인 {A\oplus B}}$	$\displaystyle({\overline {A})\wedge(A\vee B\vee C)\wedge(A\vee {B})\wedge(\overline {A}\vee {C})\wedge(\overline {A})$

단순 조합 논리

다음 회로는 입력 중 적어도 일부가 참일 때 동시에 두 개 이하일 때 참을 반환합니다.이것은 y = x1 · x2 + x1 · x2 + x2 · x3의 방정식을 구현한다.각 게이트의 출력에 대해 변수가 도입됩니다. 여기서 각 변수는 빨간색으로 표시됩니다.

x를 입력으로 하는₂ 인버터 출력에는 2개의 변수가 도입되어 있습니다.이것은 장황하지만 결과 방정식의 등가성에는 영향을 주지 않습니다.이제 각 게이트를 적절한 CNF 하위 표현식으로 대체합니다.

게이트	CNF 서브 표현식
게이트 1	(gate1 'x1) (gate1 'x1)
게이트 2	(gate2 'gate1) ' (gate2 'x2) ' (x2 ' gate2 ' gate1)
게이트 3	(gate3 'x2) (gate3 'x2)
게이트 4	(gate4 'x1) ' (gate4 ' gate3) ' (gate3 ' gate4 'x1)
게이트 5	(gate5 xx2) (gate5 xx2)
게이트 6	(gate6 'gate5) ' (gate6 'x3) ' (x3 ' gate6 ' gate5)
게이트7	(gate7 2 gate2) ( ( gate7 ) gate4) 2 ( gate2 4 gate7 gate gate4)
게이트 8	(gate8 gate gate6) ( ( gate8 gate gate7) ( ( gate6 gate gate8 gate gate7)

최종 출력 변수는 gate8이므로 이 회선의 출력이 True가 되도록 하기 위해 (gate8)이라는 마지막 간단한 구가 추가됩니다.이러한 방정식을 조합하면 SAT의 최종 인스턴스가 됩니다.

(gate1 'x1) " (gate1 'x1) " (gate2 ' gate1) " (gate2 'x2) " " " "

(x2 'gate2 ' gate1) ' (gate3 'x2) ' (gate3 'x2) ' (gate4 'x1) '

(gate4 "gate3) " (gate3 "gate4 "x1) " (gate5 "x2) " " "

(gate5 "x2) " (gate6 "gate5) " (gate6 "x3) " "

(x3 6 gate6 gate gate5) ( ( gate7 gate gate2) ∨ ( gate7 gate gate4) )

(gate2 'gate7 ' gate4) ' (gate8 ' gate6) ' (gate8 ' gate7) '

(게이트6 ∨게이트8 ∨게이트7) ∧ (게이트8) = 1

이러한 변수의 할당에 만족할 수 있는 한 가지 방법은 다음과 같습니다.

변수	가치
게이트 2	0
게이트 3	1
게이트 1	1
게이트 6	1
게이트7	0
게이트 4	0
게이트 5	1
게이트 8	1
x2	0
x3	1
x1	0

도입된 변수의 값은 일반적으로 폐기되지만 원래 회선 내의 논리 경로를 추적하기 위해 사용할 수 있습니다.여기서${\displaystyle }$( ${\displaystyle \mathrm{x}1}$, x${\displaystyle 2}$, ${\displaystyle \mathrm{x}}$3 )${\displaystyle =}$( ${\displaystyle 0}$, ${\displaystyle 0}$ , 1$$) { $displaystyle ( x$1$,$ x 2, x 3) = ($0$ , $0 , 1$ ) } 은$$, 원래의 회로가 true 로 출력하는 기준을 실제로 만족시킵니다.다른 답을 찾으려면 절(x1 xx2 xx3)을 추가하고 SAT 솔버를 다시 실행합니다.

파생

선택된 일부 게이트에 대해 CNF 하위 표현식의 가능한 한 가지 파생 결과를 제시합니다.

OR 게이트

2개의 입력 A 및 B와 1개의 출력 C를 가진 OR 게이트는 다음 조건을 충족합니다.

1. 출력 C가 참이면 입력 A 또는 B 중 적어도 하나는 참입니다.
2. 출력 C가 false일 경우 입력 A와 B는 모두 false입니다.

이 두 가지 조건을 다음 두 가지 함축의 조합으로 나타낼 수 있습니다.

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

연결, 분절 및 부정 수율만 포함하는 등가 표현으로 함의 대체

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

이미 거의 결합 정상 형태에 가깝습니다.맨 오른쪽 절을 두 번 분배하면 산출량이 늘어납니다.

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

결합의 연관성을 적용하면 CNF 공식을 얻을 수 있습니다.

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

NOT 게이트

NOT 게이트는 입력과 출력이 서로 마주보고 있을 때 올바르게 작동하고 있습니다.즉, 다음과 같습니다.

1. 출력 C가 true이면 입력 A는 false입니다.
2. 출력 C가 false일 경우 입력 A는 true입니다.

는 다음 조건을 만족해야 하는 표현으로 표현합니다.

${\displaystyle (}$ ${\displaystyle C}$ ${\displaystyle \to }$ ${\displaystyle A}$) ${\displaystyle （}$ ${\displaystyle C\stackrel{}{}}$ ${\displaystyle \stackrel{}{）}}$ ${\displaystyle \to }$ $）$ { $displaystyle ( C$ \ $rightarrow${$A$} \ $wedge$( C \ $overline { A$${\displaystyle \}}$ )$$、 ( ${\displaystyle C\mathrm{over}A\stackrel{}{}}$)$$、 {$overline${$$C } ） 。

NOR 게이트

NOR 게이트는 다음 조건이 충족될 때 올바르게 작동합니다.

1. 출력 C가 true이면 A도 B도 true가 아닙니다.
2. 출력 C가 false일 경우 A와 B 중 적어도1개는 true입니다

는 다음 조건을 만족해야 하는 표현으로 표현합니다.

${\displaystyle (}$ ${\displaystyle C}$ ${\displaystyle \to }$ ( A${\displaystyle \stackrel{}{b}}$B )${\displaystyle \wedge \stackrel{}{}、}$ ( ${\displaystyle A}$ ${\displaystyle b}$B )$$、 ( A ) ${\displaystyle 、}$ $displaystyle$ ($C$ \ $rightarrow {$ ( A \ vee B ) } 、 $wedge$( \ $overline${$C$} \ $rightarrow ( A$ \ $vee$ B$$)$$） 、${\displaystyle \stackrel{}{\stackrel{}{}}}$、 C ${\displaystyle \stackrel{}{\stackrel{}{、}}}$ C （ ${\displaystyle \stackrel{}{\stackrel{}{A\stackrel{}{}\stackrel{}{）}}}}$ ${\displaystyle \stackrel{}{\stackrel{}{\stackrel{}{）}}}}$ 。$}}\wedge$ ($C\vee$ A$\veee$B$)\}\},$ (${\displaystyle \stackrel{}{Cb}}$ B${\displaystyle \stackrel{}{}),}$(${\displaystyle Ca}$ A${\displaystyle b}$ B $),$ $(\displaystyle$ {($C\wedge$ ($A\veee$B))}, (\displaystyle {(C\wedge ($A$\vee B)})$}}\wedge$ ($C\veee$ A$\veee$B$)\}\},$ (${\displaystyle \stackrel{}{A}}$C${\displaystyle \stackrel{}{),}}$ (C${\displaystyle c}$ ${\displaystyle C}$ ${\displaystyle ),}$(C ∨ A$$ B ), (C$∨$ C $),$ (C ${\displaystyle \backslash }$ $wedge C$), (B \ $wedge$ C ), (B \$wedge$ A ), ($B,$B, $B,$ B, B, C, C${\displaystyle \stackrel{}{,}}$ C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C, C,$VEE B)},$

레퍼런스

• G.S. Tseytin:명제 미적분의 파생 복잡성에 대해서.인: Slizenko, A.O. (ed.) 건설수학과 수리논리학의 연구, 파트 2 수학 세미나, 115-125페이지.Steklov 수학 연구소(1970).러시아어 번역: Zapiski Nauchnykh Seminarov LOMI 8(1968), 234~259페이지.
• G.S. Tseytin:명제 미적분의 파생 복잡성에 대해서.1966년 9월에 개최된 레닌그라드 수학논리 세미나에서 발표.