בעיית SAT
מתוך ויקיפדיה, האנציקלופדיה החופשית
SAT הוא שמה של בעיית הכרעה הנחקרת במסגרת תורת החישוביות במדעי המחשב. בעיה זו הייתה הבעיה הראשונה עליה הוכח כי היא NP-שלמה (הוכחה זו היא משפט קוק-לוין), ובעזרתה ניתן להראות על בעיות רבות אחרות כי הן NP-שלמות. שם הבעיה הוא קיצור מהמילה satisfiability, ספיקות באנגלית.
[עריכה] תיאור הבעיה
בלוגיקה מתמטית נהוג לומר על נוסחה הנתונה בתחשיב פסוקים כי היא ספיקה אם קיימת השמה של ערכי אמת אשר עבורה הנוסחה היא אמיתית. למשל, הנוסחה "A או B" היא ספיקה, כי ניתן להציב ב-A ערך "אמת" ובכך לקבל ערך אמת עבור הנוסחה כולה. לעומת זאת, הנוסחה "A וגם לא A" אינה ספיקה, כי לא ייתכן כי גם "A" וגם "לא A" יהיו יחד בעלי הערך "אמת".
באופן כללי, בעיית SAT היא הבעיה הבאה: בהינתן נוסחה בתחשיב הפסוקים שמכילה רק קשרים מסוג "גם", "או" ו-"לא", האם קיימת השמה של ערכי אמת למשתנים כך שהנוסחה תקבל ערך אמת?
מכיוון שכל פסוק בתחשיב הפסוקים ניתן להצגה בצורה הנורמלית הקוניוקטיבית (CNF), לרוב הבעיה מנוסחת רק עבור נוסחאות הנתונות בצורה זו.
לבעיית ה-SAT חשיבות בתחומים רבים של מדעי המחשב, וביניהם אלגוריתמיקה, בינה מלאכותית ועיצוב חומרה.
ערך זה הוא קצרמר בנושא מחשבים. אתם מוזמנים לתרום לוויקיפדיה ולהרחיב אותו.
