קידוד טבלת חישוב כ־SAT

בניית משתנים ואילוצים מקומיים של Cook–Levin והוכחת נכונות וגודל פולינומי.

שאלה

תהי $N$ מכונת טיורינג אי־דטרמיניסטית חד־סרטית המכריעה את $L$ בזמן $T(n)\ge n$. עבור $x$, בנו בזמן פולינומי נוסחה $\Phi_{N,x}$ ספיקה אם ורק אם ל-$N$ יש חישוב מקבל על $x$. הגדירו משתנים, יחידות, התחלה, מעבר וקבלה וחסמו את גודל הנוסחה.

דרישות קדם

נדרשת שליטה בהגדרות היחידה ובניתוח אורכי קידוד. יש להבחין בין טענה מותנית, רדוקציה ואלגוריתם.

רמז 1

השתמשו באלפבית משולב של סימני סרט וסימנים מסומני־מצב.

רמז 2

לכל תא בדיוק סימן אחד.

רמז 3

חוקיות בין שורות עוקבות נבדקת בחלונות ברוחב קבוע.

פתרון מלא

ננרמל את $N$ כך שמצב הקבלה יחיד ונשמר, ונרפד חישוב מקבל לאורך $T=T(|x|)$. הראש מגיע רק ל-$O(T)$ תאים, ולכן נבנה טבלה בגודל $(T+1)\times(2T+1)$. האלפבית $\Gamma'$ כולל סימני סרט וסימנים $[q,a]$ המציינים שהראש נמצא בתא, המצב $q$ והסימן הנסרק $a$. המשתנה $X_{t,i,s}$ אומר שבתא $(t,i)$ נמצא $s$.

לכל תא דורשים בדיוק סימן אחד: פסוקית $\bigvee_sX_{t,i,s}$ ופסוקיות זוגיות $(\neg X_{t,i,s}\vee\neg X_{t,i,s'})$. פסוקיות יחידה מקבעות את שורת ההתחלה לקלט, לרווחים ולמצב ההתחלתי.

הסימן בתא $i$ בשורה הבאה תלוי רק בחלון קבוע סביב $i$ ובמעבר נבחר של $N$. מאחר שהמכונה קבועה, יש מספר סופי של חלונות חוקיים. אוסרים כל זוג חלונות לא חוקי בעזרת פסוקית ברוחב קבוע. החפיפה בין החלונות מבטיחה ששורה שלמה היא יורשת חוקית; חלופות אי־דטרמיניסטיות מתאימות להשמות מספקות שונות.

לבסוף דורשים הופעת $q_{\rm acc}$, או מצב מקבל בשורה האחרונה לאחר ריפוד. מהשמה מספקת מתקבלת טבלה: אילוצי היחידות נותנים קונפיגורציה בכל שורה, אילוצי ההתחלה קובעים את הראשונה, אילוצי המקום מוכיחים שכל שורה יורשת חוקית, ואילוץ הקבלה נותן חישוב מקבל. בכיוון ההפוך חישוב מקבל משרה השמה מספקת.

מספר המשתנים $O(T^2|\Gamma'|)$; אילוצי היחידות הם לכל היותר $O(T^2|\Gamma'|^2)$, ואילוצי המעבר $O(T^2)$ בגודל קבוע. לכן הגודל פולינומי ב-$T$, וב-$n$ כאשר $T$ פולינומי. המרה ל-3CNF בעזרת משתני עזר מוסיפה גודל לינארי בלבד.

נקודות בדיקה

בדקו שהוכחתם את שני הכיוונים, שכל ענף או מכונה עוצרים, ושגודל הפלט וזמן הבנייה פולינומיים באורך הקלט.

טעויות נפוצות

• השמטת אילוצי בדיוק־אחד.
• הנחת יורש יחיד למכונה אי־דטרמיניסטית.
• ספירת תאים בלי גודל פסוקיות היחידות.

מקורות ואימות

• Merged summary, pp. 50-54
• 2026 transcripts 12-13
• Sipser 3e, sec. 7.4
• Arora-Barak draft, sec. 2.3
• מיפוי קטלוג: data/exercises.json; הניסוח והפתרון עצמאיים; הגשות אישיות אינן מקור סמכות.

הערת מקור וביטחון

התרגיל הוא סינתזה מקורית. רמת הביטחון משקפת אימות של הטענה המתמטית מול מקורות ספרי הלימוד המפורטים לעיל; מקורות הקורס משמשים רק כאשר זוהה כיסוי ישיר.

פתיחה בגלריית ההמחשות: טבלת קוק–לוין