תקציר

בעיית הסינתזה הבוליאנית היא בעיית היצירה של פונקציות בוליאניות ממפרט בוליאני מאחר ולבעיה זו שימושים רבים, כמו למשל המתאר קשרים בין משתני קלט ופלט.

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

ראשית, נראה כי בשונה ממופעים אקראיים של בעיית הסינתזה הבוליאנית, מופעים תעשייתיים או מופעים "מהעולם האמיתי" מציגים מודולריות גרף גבוהה עבור הגרפים המייצגים המנותחים בעבודה זו, ואף בצורה משמעותית יותר מכפי שנמצא במקרה של בעיית SAT ברצף העבודות המוזכר לעיל.

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

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

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