موضوع مقاله: تبدیل تسیتین | مخاطب: عمومی | لحن: دانشنامه‌ای | ساختار: عنوان، مقدمه، 3 بخش، جمع‌بندی | مقاله: | # تبدیل تسیتین | مقدمه: تبدیل تسیتین (که گاهی به صورت Tseitin نیز نوشته می‌شود)، یک مدار منطقی ترکیبی دلخواه را به عنوان ورودی می‌گیرد و یک فرمول بولی در شکل فرم نرمال اشتراکی (CNF) تولید می‌کند که از نظر برآوردپذیری معادل مدار است. | ## بخش 1: تبدیل تسیتین | بردارهای ورودی که باعث می‌شوند خروجی مدار «درست» شود، یک تناظر یک‌به‌یک با انتساب‌های متغیرهایی دارند که فرمول را برآورده می‌کنند. این تبدیل، مسئله برآوردپذیری مدار برای هر مداری (از جمله هر فرمولی) را به مسئله برآوردپذیری روی فرمول‌های CNF با حداکثر ۳ لیترال در هر بند (3-CNF) تقلیل می‌دهد. انگیزه رویکرد ساده‌لوحانه این است که مدار را به صورت یک عبارت بولی نوشته و با به‌کارگیری قوانین دمورگان و خاصیت توزیع‌پذیری، آن را به شکل عطفی نرمال (CNF) تبدیل کنیم. تبدیل تسیتین اما فرمولی تولید می‌کند که اندازه‌اش به‌طور خطی نسبت به اندازه مدار ورودی رشد می‌کند. کاربرد نخستین این روش، ساخت «سوارکارهای آماری» (مجموعه‌های آماری از سفرها) برای یک شرکت حمل‌ونقل نوردیک از روی بلیت‌های سفر تکسیره روزانه بود که به‌طور مؤثر، سفرهای بدون برچسبی را که می‌توانستند متعلق به یک مسافر واحد باشند، به یکدیگر مرتبط می‌ساخت. روش کار معادله خروجی به صورت ثابت ۱ در نظر گرفته می‌شود که برابر با یک عبارت منطقی قرار می‌گیرد. این عبارت، یک عطف از زیرعبارت‌ها است، به طوری که برآورده شدن هر زیرعبارت، عملکرد صحیح یک گیت منفرد در مدار ورودی را تضمین می‌کند. | ## بخش 2: تبدیل تسیتین | در نتیجه، برآورده شدن کل عبارت خروجی، تضمین می‌کند که تمامی مدار ورودی به درستی عمل می‌کند. سپس یک عبارت CNF از پیش محاسبه‌شده کوچک که رابطه بین ورودی‌ها و خروجی گیت را بیان می‌کند، به عبارت خروجی اضافه می‌شود (از طریق عمل «و»). توجه داشته باشید که ورودی‌های این گیت‌ها می‌توانند یا همان گزاره‌های اصلی باشند یا متغیرهای معرفی‌شده‌ای که نمایانگر خروجی گیت‌های فرعی هستند. اگرچه عبارت خروجی متغیرهای بیشتری نسبت به ورودی دارد، ولی همچنان هم‌برآوردپذیر باقی می‌ماند؛ یعنی اگر و تنها اگر معادله ورودی اصلی برآوردپذیر باشد، این عبارت نیز برآوردپذیر است. هنگامی که یک تخصیص برآورده‌کننده برای متغیرها پیدا شد، می‌توان مقادیر تخصیص‌یافته به متغیرهای معرفی‌شده را به سادگی کنار گذاشت. در نهایت، یک بند نهایی که فقط شامل یک گزاره تکی است، اضافه می‌شود: متغیر خروجی گیت پایانی. اگر این گزاره مکمل شده باشد، آنگاه برآورده شدن این بند، عبارت خروجی را به نادرست مجبور می‌کند؛ در غیر این صورت، عبارت به درست مجبور می‌شود. | ## بخش 3: تبدیل تسیتین | مثال‌ها فرمول زیر با نام را در نظر بگیرید: تمامی زیرفرمول‌ها (به جز متغیرهای ساده) را در نظر می‌گیریم: برای هر زیرفرمول یک متغیر جدید معرفی می‌کنیم: تمامی جایگزینی‌ها و همچنین جایگزینی مربوط به را با هم عطف می‌کنیم: همه این جایگزینی‌ها را می‌توان به CNF تبدیل کرد. برای مثال: منطق ترکیبی ساده مدار زیر وقتی درست برمی‌گردد که حداقل برخی از ورودی‌هایش درست باشند، اما نه بیش از دو ورودی همزمان. برای خروجی هر گیت یک متغیر معرفی می‌شود که در اینجا با رنگ قرمز مشخص شده‌اند: center توجه کنید که خروجی اینورتری که x را به عنوان ورودی دارد، دو متغیر معرفی‌شده دارد. برای یافتن پاسخ متفاوت، می‌توان بند (x1 ∨ x2 ∨ ) را اضافه کرد و دوباره حل‌کننده SAT را اجرا نمود. مشتق‌گیری در زیر یک روش ممکن برای مشتق‌گیری زیرعبارت CNF برای برخی گیت‌های انتخاب‌شده ارائه شده است: گیت OR یک گیت OR با دو ورودی A و B و یک خروجی C شرایط زیر را برآورده می‌کند: ۱. می‌توانیم این دو شرط را به صورت عطف دو شرطی بیان کنیم: با جایگزینی شرطی‌ها با عبارات معادل فقط شامل عطف، فصل و نقیض به دست می‌آید: که تقریباً در حال حاضر به شکل شرط عطفی نرمال است. با دو بار توزیع کردن بند سمت راست: و با اعمال شرکت‌پذیری عطف، فرمول CNF به دست می‌آید: گیت NOT گیت NOT زمانی به درستی عمل می‌کند که ورودی و خروجی آن در مقابل یکدیگر باشند. | ## جمع‌بندی | اگر خروجی C نادرست باشد، ورودی A درست است این شرایط را به صورت عبارتی که باید برآورده شود بیان می‌کنیم: گیت NOR گیت NOR زمانی به درستی عمل می‌کند که شرایط زیر برقرار باشند: ۱.