בעיית הספיקות

בעיית הספיקות בתחשיב הפסוקים (SAT) עוסקת בשאלה אם קיימת השמה של ערכי אמת למשתנים כך שנוסחה תהיה אמת. היא הייתה הבעיה הראשונה שהוכחה NP-שלמה במשפט קוק-לוין. משמעות הדבר: אם נמצא אלגוריתם פולינומי ל-SAT, אז ניתן לפתור גם כל בעיה אחרת ב‑NP בזמן פולינומי.
נוסחה נקראת ספיקה אם אפשר לתת ערכים שמשאירים אותה אמיתית. לדוגמה, "A או B" ספיקה כי אפשר להגדיר A כאמיתי. לעומת זאת, "A וגם לא A" אינה ספיקה, כי אי אפשר ששתי האפשרויות יהיו אמיתיות יחד.
במטפלים מעשיים נוח לעבוד עם נוסחאות בצורת CNF. CNF (צורה נורמלית קוניונקטיבית) פירושה שהנוסחה היא 'וגם' של פסוקיות, שכל אחת מהן היא 'או' של משתנים או השלשות שלהם. גם כאשר מגבילים את הבעיה ל‑CNF (השם CNF-SAT או CSAT), הבעיה נשארת NP-קשה.
מגדירים k‑SAT כשכל פסוקית מכילה בדיוק k ליטרלים (משתנים או הכפלה שלהם ב'לא'). הבעיות 1‑SAT ו‑2‑SAT ניתנות לפתרון בזמן פולינומי. לעומת זאת, לכל k ≥ 3 הבעיה היא NP-שלמה, כלומר לא הופכת לקלה רק כי הגבלנו את אורך הפסוקיות.
יש תוצאות שמראות תנאים שמבטיחים סיפוק. למשל, באמצעות למת המקומיות של לובאץ' מראים שאם כל משתנה מופיע רק מעט פסוקיות, אז יש בהכרח השמה מספקת.
בבעיה הנגזרת Max-SAT שואלים כמה פסוקיות אפשר לספק במקסימום בנוסחת CNF עם m פסוקיות. ב‑Max‑W‑SAT מוסיפים משקלים w_i לכל פסוקית ומנסים למקסם את סכום המשקולות של הפסוקיות המסופקות.
נמצאו אלגוריתמי קירוב שנותנים פתרונות קרובים (למשל שיעורים כמו 1/2, 2/3, 3/4 ועוד). בשנת 1997 הוכח שאינו אפשרי אלגוריתם פולינומי שמבטיח קירוב טוב מ‑7/8, אלא אם כן P=NP. לכן Max-SAT ו‑Max-W-SAT שייכות למחלקת APX אך לא ל‑PTAS, שוב בהנחת P≠NP.

SAT היא שאלה במחשבים. שואלים אם אפשר לתת לכל משתנה אמת או שקר. מטרת השאלה היא לראות אם המשפט הכולל יהיה אמיתי.
משפט נקרא ספיקה אם יש דרך לבחור ערכים כך שהוא יהיה אמיתי. למשל, "A או B" ספיקה. אפשר לשים A כאמיתי. אבל "A וגם לא A" לא אפשרי.
לעיתים כותבים את הנוסחאות בצורה שנקראת CNF. זו צורה שבה יש הרבה "פסוקיות". כל פסוקית היא רשימת ו\ו"או" של משתנים.
קיים מושג בשם k-SAT. זה אומר שכל פסוקית כוללת בדיוק k משתנים. אם k הוא 1 או 2, אפשר לפתור את הבעיה יחסית בקלות. אם k גדול או שווה ל‑3, הבעיה קשה מאוד.
שואלים גם כמה פסוקיות אפשר לגרום להן להיות נכונות ביחד. זאת נקרא Max-SAT. אם נותנים משקל לכל פסוקית, זו גרסה משוקללת בשם Max-W-SAT.
יש תוכניות שמקרבות את התשובה. יש גבול שנמצא ב‑1997 שאומר שלא תמיד אפשר להבטיח פתרון טוב יותר מ‑7/8, אלא אם כן בעיות מסוימות הופכות קלות יותר מחשבים.