تبدیل تسیتین

این مقاله در حال ویرایش و تکمیل است.

تبدیل تسیتین (که گاهی به صورت Tseitin نیز نوشته می‌شود)، یک مدار منطقی ترکیبی دلخواه را به عنوان ورودی می‌گیرد و یک فرمول بولی در شکل فرم نرمال اشتراکی (CNF) تولید می‌کند که از نظر برآوردپذیری معادل مدار است. طول این فرمول، به‌طور خطی با اندازه مدار متناسب است. بردارهای ورودی که باعث می‌شوند خروجی مدار «درست» شود، یک تناظر یک‌به‌یک با انتساب‌های متغیرهایی دارند که فرمول را برآورده می‌کنند. این تبدیل، مسئله برآوردپذیری مدار برای هر مداری (از جمله هر فرمولی) را به مسئله برآوردپذیری روی فرمول‌های CNF با حداکثر ۳ لیترال در هر بند (3-CNF) تقلیل می‌دهد. این روش توسط دانشمند روسی گریگوری تسیتین کشف شد.

## انگیزه

رویکرد ساده‌لوحانه این است که مدار را به صورت یک عبارت بولی نوشته و با به‌کارگیری قوانین دمورگان و خاصیت توزیع‌پذیری، آن را به شکل عطفی نرمال (CNF) تبدیل کنیم. با این حال، این روش می‌تواند به افزایش نمایی در اندازه فرمول بیانجامد. تبدیل تسیتین اما فرمولی تولید می‌کند که اندازه‌اش به‌طور خطی نسبت به اندازه مدار ورودی رشد می‌کند. کاربرد نخستین این روش، ساخت «سوارکارهای آماری» (مجموعه‌های آماری از سفرها) برای یک شرکت حمل‌ونقل نوردیک از روی بلیت‌های سفر تکسیره روزانه بود که به‌طور مؤثر، سفرهای بدون برچسبی را که می‌توانستند متعلق به یک مسافر واحد باشند، به یکدیگر مرتبط می‌ساخت.

## روش کار
معادله خروجی به صورت ثابت ۱ در نظر گرفته می‌شود که برابر با یک عبارت منطقی قرار می‌گیرد. این عبارت، یک عطف از زیرعبارت‌ها است، به طوری که برآورده شدن هر زیرعبارت، عملکرد صحیح یک گیت منفرد در مدار ورودی را تضمین می‌کند. در نتیجه، برآورده شدن کل عبارت خروجی، تضمین می‌کند که تمامی مدار ورودی به درستی عمل می‌کند.

برای هر گیت، یک متغیر جدید که نمایانگر خروجی آن است معرفی می‌شود. سپس یک عبارت CNF از پیش محاسبه‌شده کوچک که رابطه بین ورودی‌ها و خروجی گیت را بیان می‌کند، به عبارت خروجی اضافه می‌شود (از طریق عمل «و»). توجه داشته باشید که ورودی‌های این گیت‌ها می‌توانند یا همان گزاره‌های اصلی باشند یا متغیرهای معرفی‌شده‌ای که نمایانگر خروجی گیت‌های فرعی هستند.

اگرچه عبارت خروجی متغیرهای بیشتری نسبت به ورودی دارد، ولی همچنان هم‌برآوردپذیر باقی می‌ماند؛ یعنی اگر و تنها اگر معادله ورودی اصلی برآوردپذیر باشد، این عبارت نیز برآوردپذیر است. هنگامی که یک تخصیص برآورده‌کننده برای متغیرها پیدا شد، می‌توان مقادیر تخصیص‌یافته به متغیرهای معرفی‌شده را به سادگی کنار گذاشت.

در نهایت، یک بند نهایی که فقط شامل یک گزاره تکی است، اضافه می‌شود: متغیر خروجی گیت پایانی. اگر این گزاره مکمل شده باشد، آنگاه برآورده شدن این بند، عبارت خروجی را به نادرست مجبور می‌کند؛ در غیر این صورت، عبارت به درست مجبور می‌شود.

## مثال‌ها

فرمول زیر با نام \phi را در نظر بگیرید:
:\phi := ((p \lor q) \land r) \to (\neg s)

تمامی زیرفرمول‌ها (به جز متغیرهای ساده) را در نظر می‌گیریم:

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


برای هر زیرفرمول یک متغیر جدید معرفی می‌کنیم:

:
\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}


تمامی جایگزینی‌ها و همچنین جایگزینی مربوط به \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{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}


## منطق ترکیبی ساده

مدار زیر وقتی درست برمی‌گردد که حداقل برخی از ورودی‌هایش درست باشند، اما نه بیش از دو ورودی همزمان. این مدار معادله  را پیاده‌سازی می‌کند. برای خروجی هر گیت یک متغیر معرفی می‌شود که در اینجا با رنگ قرمز مشخص شده‌اند:

center

توجه کنید که خروجی اینورتری که x را به عنوان ورودی دارد، دو متغیر معرفی‌شده دارد. اگرچه این اضافی است، اما بر هم‌برآوردپذیر بودن معادله نهایی تأثیری ندارد. حال هر گیت را با زیرعبارت CNF مناسب آن جایگزین می‌کنیم:

متغیر خروجی نهایی، gate8 است، بنابراین برای اجباری کردن درست بودن خروجی این مدار، یک بند ساده نهایی اضافه می‌شود: (gate8). ترکیب این معادلات، نمونه نهایی مسئله SAT را تولید می‌کند:

: (gate1 ∨ x1) ∧ ( ∨ ) ∧ ( ∨ gate1) ∧ ( ∨ x2) ∧ 
: ( ∨ gate2 ∨ ) ∧ (gate3 ∨ x2) ∧ ( ∨ ) ∧ ( ∨ x1) ∧ 
: ( ∨ gate3) ∧ ( ∨ gate4 ∨ ) ∧ (gate5 ∨ x2) ∧ 
: ( ∨ ) ∧ ( ∨ gate5) ∧ ( ∨ x3) ∧ 
: ( ∨ gate6 ∨ ) ∧ (gate7 ∨ ) ∧ (gate7 ∨ ) ∧ 
: (gate2 ∨  ∨ gate4) ∧ (gate8 ∨ ) ∧ (gate8 ∨ ) ∧ 
: (gate6 ∨  ∨ gate7) ∧ (gate8) = 1

یک انتساب ممکن که این متغیرها را برآورده می‌کند:

مقادیر متغیرهای معرفی‌شده معمولاً دور ریخته می‌شوند، اما می‌توان از آنها برای ردیابی مسیر منطق در مدار اصلی استفاده کرد. در اینجا، (x1,x2,x3)=(0,0,1) واقعاً معیارهای خروجی درست مدار اصلی را برآورده می‌کند. برای یافتن پاسخ متفاوت، می‌توان بند (x1 ∨ x2 ∨ ) را اضافه کرد و دوباره حل‌کننده SAT را اجرا نمود.

## مشتق‌گیری
در زیر یک روش ممکن برای مشتق‌گیری زیرعبارت CNF برای برخی گیت‌های انتخاب‌شده ارائه شده است:

### گیت OR
یک گیت OR با دو ورودی *A* و *B* و یک خروجی *C* شرایط زیر را برآورده می‌کند: ۱. اگر خروجی *C* درست باشد، آنگاه حداقل یکی از ورودی‌هایش *A* یا *B* درست است، ۲. اگر خروجی *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})),

و با اعمال شرکت‌پذیری عطف، فرمول CNF به دست می‌آید:

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

### گیت NOT
گیت NOT زمانی به درستی عمل می‌کند که ورودی و خروجی آن در مقابل یکدیگر باشند. یعنی: ۱. اگر خروجی C درست باشد، ورودی A نادرست است ۲. اگر خروجی C نادرست باشد، ورودی A درست است

این شرایط را به صورت عبارتی که باید برآورده شود بیان می‌کنیم:

: 

### گیت NOR
گیت NOR زمانی به درستی عمل می‌کند که شرایط زیر برقرار باشند: ۱. اگر خروجی C درست باشد، آنگاه نه A و نه B درست هستند ۲. اگر خروجی C نادرست باشد، آنگاه حداقل یکی از A و 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))}}

## منابع
* G.S. Tseytin: On the complexity of derivation in propositional calculus. In: Slisenko, A.O. (ed.) Studies in Constructive Mathematics and Mathematical Logic, Part II, Seminars in Mathematics, pp.&nbsp;115&ndash;125. Steklov Mathematical Institute (1970). Translated from Russian: Zapiski Nauchnykh Seminarov LOMI 8 (1968), pp.&nbsp;234–259.
* G.S. Tseytin: On the complexity of derivation in propositional calculus. Presented at the Leningrad Seminar on Mathematical Logic held in September 1966.

رده:دروازه‌های منطقی
رده:منطق در علوم کامپیوتر