6.7.2. בדיקת מודל מבוססת SAT – Bounded Model Checkingהמטרה שלנו היא להשתמש ב-SAT Solvers כדי לבצע בדיקת מודל. בהנתן נוסחה ומבנה קריפקה M, נרצה לקודד בדיקת מודל לנוסחה פסוקית. נציג כדוגמא טיפול בנוסחאות במבנה , כאשר נוסחה בוליאנית. הגישה שנציג היא הפרכה ולא אימות: נקודד נוסחה פסוקית כך שאם יש השמה המספקת אותה יתקיים כי . במידה וההשמה אינה מספקת את הנוסחה איננו יודעים את המבנה מספק את הנוסחה, ונצטרך לבדוק נוסחה חדשה. נבצע בדיקת מודל חסומה. הגדרת הבעיה: בהינתן מודל M, נוסף (שקולה ל-) וחסם , צריך לבדוק האם קיים מסלול ב-M באורך קטן או שווה ל- ממצב התחלתי שמוביל למצב המספק . אם מצאנו השמה מספקת אז יתקיים כי , כלומר . אם לא מצאנו השמה מספקת נגדיל את . עצירה: נעצור את התהליך במקרים הבאים: א. התפוצצות זכרון/זמן. ב. נמצא מסלול המוביל למצב המספק . ג. הגעה לחסם מקסימלי על אורך המסלול, כך שאם אין שגיאה עד חסם זה מובטח שאין שגיאה בכלל ומתקיים . בדיקת מודל חסומה עבור M ו-:
נקודת מפתח להבנת נושא SAT: SAT מקבלת נוסחה ומחזירה האם קיימת לה השמה מספקת. אם במקרה שלנו הנוסחה מייצגת מבנה של מסלול חוקי, SAT מחזירה האם קיים מסלול כזה. אם קיימים מספר מסלולים, SAT תחזיר רק את קיומו של אחד מהם. (לכן SAT נוחה להוכחת E ולא להוכחת A). מתי אפשר לעצור את האלגוריתם?
איך מקבלים את הנתונים? איך בונים את הנוסחה הפסוקית שנשלח אל SAT?
בניית הפונקציות:
דוגמא
אנחנו רוצים לבדוק האם . כדי לבצע זאת נבדוק את השלילה: ומכאן: נרשום את הנוסחאות עבור : דוגמא להשמה מספקת:
נשים לב שקיימת גם השמה מספקת באורך : .
אין תגובות!
|
תוכן העניינים:
קישורים רלוונטיים:שיתוף: |