בעיית הספיקות בתחשיב הפסוקים (בקיצור: SAT - קיצור של המילה האנגלית Satisfiability, שמשמעותה ספיקות) הוא שמה של בעיית הכרעה הנחקרת במסגרת תורת הסיבוכיות במדעי המחשב. בעיה זו הייתה הבעיה הראשונה עליה הוכח כי היא NP-שלמה (הוכחה זו היא משפט קוק-לוין), משמע אם קיים לה פתרון אלגוריתמי הרץ בזמן פולינומי אזי קיים פתרון כזה לכל בעיה ב-NP (מחלקת כל הבעיות שעבורן קיים מוודא בזמן פולינומי). בעיה זו משמשת בהוכחות רבות עבור בעיות NP-שלמות אחרות.

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

באופן כללי, בעיית SAT היא הבעיה הבאה: בהינתן נוסחה בתחשיב הפסוקים שמכילה רק קשרים מסוג "גם", "או" ו"לא", האם קיימת השמה של ערכי אמת למשתנים כך שהנוסחה תקבל ערך אמת?

ניתן להראות שגם אם נגביל את הבעיה לנוסחאות הניתנות בצורה הנורמלית הקוניונקטיבית (CNF), הבעיה תישאר NP-קשה. לכן, בשל נוחות העבודה עם נוסחאות בצורת CNF, מקובל לנסח את הבעיה רק עבור נוסחאות הנתונות בצורה זו (וריאנט זה של הבעיה נקרא לעיתים CNF-SAT או CSAT).

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

מקובל להתייחס בשם ${\displaystyle k{\text{-SAT}}}$ לבעיית סיפוק נוסחאות בצורת CNF אשר כל הפסוקיות המופיעות בהן מאורך ${\displaystyle \ k}$. ניתן לראות כי הבעיות ${\displaystyle 1{\text{-SAT}}}$ ו${\displaystyle \ 2{\text{-SAT}}}$ ניתנות לפתרון בזמן פולינומי. (כלומר, שייכות ל-P), בעוד שעבור ${\displaystyle \ k\geq 3}$ הבעיה המתקבלת ‏NP-שלמה (כלומר, צמצום הבעיה לפסוקיות מאורך ${\displaystyle \ k}$ בלבד לא הופך אותה לקלה יותר)

בעזרת למת המקומיות של לובאס ניתן להראות כי אם כל משתנה מופיע בלכל היותר ${\displaystyle 2^{k}/4k}$ פסוקיות, אזי קיימת השמה מספקת. מאידך, ייתכן כי לא ניתן למצוא את ההשמה המספקת בזמן פולינומי.

בהינתן נוסחת CNF בעלת ${\displaystyle \ m}$ פסוקיות, ניתן לשאול מה מספר הפסוקיות המקסימלי אשר ניתן לספק באמצעות השמת ערכי אמת. (אם הנוסחה ספיקה, מספר זה הוא ${\displaystyle \ m}$) בעיה זו מכונה בעיית ספיקות מקסימלית. (באנגלית, Max-Sat) ניתן להוסיף ולהכליל בעיה זו באמצעות קביעת משקל ${\displaystyle \ w_{i}}$ לכל פסוקית, ומציאת השמת ערכי אמת עבורה משקל הפסוקיות המסופקות יהיה מקסימלי. גרסה זו של הבעיה נקראת בעיית הספיקות המשוקללת המקסימלית. (באנגלית Max-W-Sat)

נמצאו אלגוריתמי קירוב רבים לבעיות אלה, אשר נותנים קירובים שונים, (1/2^[1], 2/3^[2], 3/4^[3][4] ואף יותר מכך), אך הוכח^[5] בשנת 1997 כי לא ייתכן אלגוריתם פולינומי אשר מבטיח פתרון טוב יותר מאשר 7/8-קירוב. (אלא אם כן P=NP) לכן, שייכות הבעיות Max-Sat ו-Max-W-Sat למחלקה APX אך לא ל-PTAS. (אלא אם כן, P=NP, ואז שתי המחלקות הנ"ל שוות)

• חיפוש מקומי

מדיה וקבצים בנושא בעיית הספיקות בוויקישיתוף

• אלגוריתמים מקורבים לפתרון בעיית הספיקות המרבית
• בעיית הספיקות, באתר MathWorld (באנגלית)

ערך זה הוא קצרמר בנושא מדעי המחשב. אתם מוזמנים לתרום לוויקיפדיה ולהרחיב אותו.