פותרים את SAT: המקרים של HORNSAT ו-2SAT

בפוסטים הקודמים דיברתי על בעיית SAT ועל השיטה שבה ניתן להוכיח שפסוק CNF אינו ספיק, אבל כל מה שעשיתי עד כה היה מאוד באוויר – עדיין לא הסברתי איך אפשר בפועל לקחת פסוק CNF ולקבוע אם הוא ספיק או לא. ובכן, באופן כללי הבעיה היא קשה, לפחות מבחינה תיאורטית, אבל יש מקרים פרטיים מסויימים של …

רזולוציה – איך אפשר להוכיח שאי אפשר?

בפוסט הקודם תיארתי את בעיית SAT וסיימתי בכך שהבטחתי להסביר איך אפשר להשתכנע בכך שפסוק CNF אינו ספיק, מבלי שיהיה צורך לבדוק את כל ההשמות האפשריות עבורו. בפוסט הזה אציג את השיטה הנפוצה ביותר לשימוש כדי להוכיח זאת – רזולוציה. מובטח לנו שאם $latex \varphi$ הוא פסוק CNF לא ספיק, אז קיימת הוכחה לכך המבוססת …

מה זו בעיית SAT ולמה חשוב לפתור אותה?

אני רוצה לדבר על בעיה לא פתירה, ואיך שפותרים אותה. הבעיה נקראת SAT, קיצור של Satisfiability. הזכרתי אותה לא מעט בבלוג בעבר, אבל בואו נציג אותה מחדש, בלי הנחות מוקדמות. לפני שנגיע להגדרות הפורמליות, הנה הרעיון: נותנים לנו אוסף של אילוצים ושואלים אותנו אם אפשר לספק את כל האילוצים הללו בו זמנית. האילוצים הללו מקודדים …