רדוקציה מ־SAT ל־3SAT בפיצול פסוקיות

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

שאלה

תארו רדוקציית many-one בזמן פולינומי מ־CNF-SAT ל־3SAT. בהינתן נוסחת CNF עם פסוקיות באורך שרירותי, הפיקו נוסחת 3CNF שוות־ספיקות. טפלו גם בפסוקיות באורך $1$ ו-$2$ וגם באורך לפחות $4$. הוכיחו את שני הכיוונים וחסומו את גודל הפלט.

רמז 1

אל תפיצו נוסחה בוליאנית כללית ל־CNF; התחילו מ־CNF ופצלו רק פסוקיות ארוכות.

רמז 2

עבור $(\ell_1\lor\ell_2\lor\cdots\lor\ell_t)$ עם $t\ge4$, הכניסו משתנים חדשים הקושרים שלשות חופפות.

פתרון מלא

מניחים שהקלט כבר ב־CNF (פלט קוק–לוין או המרת Tseitin קודמת). מעבדים כל פסוקית בנפרד.

• אורך $3$: משאירים.
• אורך $1$: מרפדים במשתנים טריים לשלשות שכופות את $\ell$.
• אורך $2$: ריפוד דומה.
• אורך $t\ge4$: מחליפים בשרשרת [ (\ell_1\lor\ell_2\lor y_1)\land(\neg y_1\lor\ell_3\lor y_2)\land\cdots\land(\neg y_\lor\ell_\lor\ell_t) ] עם $y_1,\ldots,y_{t-3}$ חדשים.

אם הליטרל המקורי $\ell_i$ מספק, מגדירים את משתני השרשרת בהתאם; ולהפך, סיפוק כל השלשות כופה ליטרל מקורי אמיתי אחד לפחות. מספר השלשות ליניארי באורך הקלט, ולכן הפלט פולינומי. העתקת זהות על קלט שאינו 3CNF אינה רדוקציה ל־3SAT.

נקודת ביקורת

יש להוכיח שוויון־ספיקות לשני הכיוונים בשרשרת; ריפוד פסוקיות קצרות לא יאפשר השמה המספקת בלי $\ell$.

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

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

הערת מקור

סינתזה מקורית מיושרת לקורס ולספרים של הנרמול הסטנדרטי SAT→3SAT באטלס. מטלות הביקורת על רדוקציות זהות שבורות (למשל תרגיל 3 תשפ״ו) מעודדות את התרגיל אך אינן מועתקות.

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

• Sipser 3e, sec. 7.5
• Garey-Johnson, משפחת LO
• מיפוי קטלוג: data/exercises.json; הניסוחים והפתרונות נכתבו באופן עצמאי.

פתיחה בגלריית ההמחשות: SAT → 3SAT