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

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

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

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

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

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