מפת הסיבוכיות
EN
פיצול פסוקיות במשתנה עזר

SAT ≤p 3SAT

SAT≤p3SAT\mathrm{SAT}\le_p\mathrm{3SAT}, ולכן 3SAT\mathrm{3SAT} היא NP-שלמה.

הבנייה

צעד הפיצול (אלגוריתם 1). על נוסחת CNF φ\varphi:

  1. אם φ\varphi כבר 3CNF — החזר אותה.
  2. אחרת תהי C=ℓ1∨ℓ2∨⋯∨ℓkC=\ell_1\vee\ell_2\vee\dots\vee\ell_k הפסוקית הראשונה עם k>3k>3 ליטרלים. נגדיר C′=ℓ1∨ℓ2∨z,C′′=ℓ3∨⋯∨ℓk∨zˉ,C'=\ell_1\vee\ell_2\vee z,\qquad C''=\ell_3\vee\dots\vee\ell_k\vee\bar z, כאשר zz הוא משתנה חדש שאינו מופיע ב-φ\varphi.
  3. החזר את φ^\hat\varphi, המתקבלת מ-φ\varphi בהחלפת CC ב-C′∧C′′C'\wedge C''.

הרדוקציה. כל עוד φ\varphi אינה 3CNF, הרץ את צעד הפיצול, כשבכל הפעלה נבחר משתנה עזר חדש שלא הופיע קודם; לבסוף החזר את φ\varphi. קלט שאינו קידוד תקין של נוסחת CNF מוחלף בנוסחת 3CNF קבועה ובלתי-ספיקה, למשל (y)∧(yˉ)(y)\wedge(\bar y).

עצירה. פסוקית באורך k>3k>3 מוחלפת בפסוקיות באורכים 33 ו-k−1k-1, ופסוקיות באורך ≤3\le3 אינן משתנות. לכן הגודל ∑∣C∣>3(∣C∣−3)\sum_{|C|>3}(|C|-3) יורד בדיוק ב-11 בכל איטרציה, והוא טבעי אי-שלילי — אז הלולאה עוצרת ובפלט כל הפסוקיות באורך ≤3\le3.

המחשה

בנייה מודרכת

SAT → 3SAT

שלב 1 מתוך 6
פסוקית מקור(a ∨ b ∨ c ∨ d ∨ e)
SAT ל־3SAT בפיצול פסוקיותפסוקית בת חמישה ליטרלים מוחלפת בשלוש שלשות חופפות הקשורות בשני משתנים חדשים.פסוקית מקור
משתנה טרישלשת פלט

נכונות — שני הכיוונים

SAT ∈ ⟹ 3SAT ∈

די להוכיח את הלמה על צעד יחיד: φ\varphi ספיקה   ⟺  \iff φ^\hat\varphi ספיקה, ואז לשרשר באינדוקציה.

נניח ש-φ\varphi ספיקה, ותהי vv השמה מספקת. בפרט vv מספקת את C=ℓ1∨⋯∨ℓkC=\ell_1\vee\dots\vee\ell_k, ולכן קיים tt עם v(ℓt)=1v(\ell_t)=1. נרחיב את vv ל-zz:

  • אם t∈{1,2}t\in\{1,2\} — נקבע v(z)=0v(z)=0. אז C′=ℓ1∨ℓ2∨zC'=\ell_1\vee\ell_2\vee z מסופקת על ידי ℓt\ell_t, ו-C′′C'' מסופקת על ידי zˉ\bar z.
  • אחרת t≥3t\ge3 — נקבע v(z)=1v(z)=1. אז C′C' מסופקת על ידי zz, ו-C′′C'' מסופקת על ידי ℓt\ell_t.

יתר הפסוקיות לא השתנו ו-zz אינו מופיע בהן, ולכן הן נשארות מסופקות. לכן φ^\hat\varphi ספיקה.

3SAT ∈ ⟹ SAT ∈

נניח ש-φ^\hat\varphi ספיקה, ותהי vv השמה מספקת אותה. נצמצם את vv למשתני φ\varphi (כלומר נשכח את הערך שהיא נתנה ל-zz) ונראה שהיא מספקת את φ\varphi.

כל פסוקית של φ\varphi פרט ל-CC מופיעה ללא שינוי ב-φ^\hat\varphi ואינה מכילה את zz, ולכן היא מסופקת. נותר CC. נפריד לפי v(z)v(z):

  • אם v(z)=1v(z)=1: הפסוקית C′′=ℓ3∨⋯∨ℓk∨zˉC''=\ell_3\vee\dots\vee\ell_k\vee\bar z מסופקת, ו-zˉ\bar z מקבל 00, ולכן קיים t≥3t\ge3 עם v(ℓt)=1v(\ell_t)=1. אותו ליטרל מופיע ב-CC, ולכן CC מסופקת.
  • אם v(z)=0v(z)=0: הפסוקית C′=ℓ1∨ℓ2∨zC'=\ell_1\vee\ell_2\vee z מסופקת ו-zz מקבל 00, ולכן v(ℓ1)=1v(\ell_1)=1 או v(ℓ2)=1v(\ell_2)=1. שוב ליטרל של CC, ולכן CC מסופקת.

בשני המקרים vv מספקת את CC, ולכן את φ\varphi כולה.

מכיוון שהלמה מתקיימת לכל צעד, ובאינדוקציה על φ0=φ,φ1,…,φm\varphi_0=\varphi,\varphi_1,\dots,\varphi_m (הפלט), מתקבל φ\varphi ספיקה   ⟺  \iff φm\varphi_m ספיקה — כלומר ⟨φ⟩∈SAT  ⟺  ⟨φm⟩∈3SAT\langle\varphi\rangle\in\mathrm{SAT}\iff\langle\varphi_m\rangle\in\mathrm{3SAT}.

סיבוכיות הרדוקציה

זמןO(|φ|²)
מקוםO(|φ|)
גודל הפלטO(|φ|) symbols, O(|φ| log |φ|) bits

מספר האיטרציות הוא בדיוק ∑∣C∣>3(∣C∣−3)≤L≤∣φ∣\sum_{|C|>3}(|C|-3)\le L\le|\varphi|, כאשר LL הוא מספר מופעי הליטרלים. כל איטרציה מוסיפה בדיוק 22 מופעי ליטרלים, ולכן Lfinal≤L+2L=3LL_{\text{final}}\le L+2L=3L — הנוסחה אינה מתנפחת אלא נשארת לינארית. איטרציה בודדת עולה O(∣φ∣)O(|\varphi|) (סריקה והעתקה), ולכן סך הכול O(∣φ∣2)O(|\varphi|^2).

ברמת הביטים: הרדוקציה מוסיפה עד LL משתנים חדשים, וקידוד אינדקס עולה O(log⁡L)O(\log L) ביטים, ולכן אורך הפלט בביטים הוא O(∣φ∣log⁡∣φ∣)O(|\varphi|\log|\varphi|) — עדיין פולינומי.

מה זה קונה

יחד עם קוק–לוין (SAT\mathrm{SAT} NP-קשה) ועם הטרנזיטיביות של ≤p\le_p: כל A∈NPA\in\mathrm{NP} מקיימת A≤pSAT≤p3SATA\le_p\mathrm{SAT}\le_p\mathrm{3SAT}, ולכן 3SAT\mathrm{3SAT} היא NP-שלמה. מכאן ואילך כמעט כל רדוקציה בקורס מתחילה מ-3SAT\mathrm{3SAT} ולא מ-SAT\mathrm{SAT} — המבנה הנוקשה של שלושה ליטרלים לפסוקית קל בהרבה להעתקה לגרפים ולקבוצות.

מלכודות

  • C′∧C′′C'\wedge C'' אינה שקולה ל-CC. היא רק שקולת-ספיקות: אם vv מספקת את CC אפשר להרחיב אותה ל-zz כך שתספק את שתיהן, ולהפך. השקילות הלוגית נשברת — למשל השמה שנותנת 11 ל-ℓ1\ell_1 ו-11 ל-zz מספקת את CC אך לא את C′∧C′′C'\wedge C''.

  • המשתנה zz חייב להיות חדש בכל איטרציה. אם משתמשים באותו zz פעמיים, שתי פסוקיות שונות נקשרות זו לזו דרך אותו משתנה, וההרחבה של ההשמה בכיוון הראשון עלולה לדרוש בו-זמנית z=0z=0 ו-z=1z=1.

  • אסור לפרק את CC בעזרת חוק הפילוג. הפיכת CNF ארוכה ל-3CNF שקולה לוגית מנפחת את הנוסחה מעריכית. משתנה העזר קונה בדיוק את הוויתור על השקילות הלוגית תמורת גודל לינארי.

השרשרת

נשענת על

מאיפה זה נקרא