ההוכחה הארוכה ביותר בהיסטוריה! (או: איך פותרי SAT מתגברים על בעיות קומבינטוריות, אבל היי זה שם פחות מפוצץ)

לפני חודש וקצת הצליחה תוצאה מתמטית נחמדה להיכנס אל החדשות לא בשל הסיבות שבגללן היא טובה, אלא בעיקר אלו שבגללן היא בעייתית: ההוכחה שלה היא (לכאורה) בגודל מפלצתי של 200 טרה-בייט. כמה זה הרבה? נאמר, זה פי 40 יותר מידע מאשר היה בשרתי ויקיפדיה ב-2010, ויש עוד שלל המחשות. בקיצור, זה הרבה מאוד. הנתון הזה …

פותרים את SAT – אלגוריתם CDCL

בפוסט הקודם על פתרונות לבעיית SAT ראינו את אלגוריתם DPLL – זה היה פחות או יותר האלגוריתם הבסיסי שרוב פותרי ה-SAT המדוייקים (להבדיל מהסתברותיים) מבוססים עליו, אבל מן הסתם פותרים מודרניים הולכים רחוק יותר ממנו, ובפוסט הזה אני רוצה להציג אלגוריתם קצת יותר מודרני שמתבסס על DPLL אבל עושה עוד דברים מתוחכמים – אלגוריתם CDCL, …

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

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