Z3 Sudoku

זהו מאמר המשך למאמר הקודם למאמר הראשון

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

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

להורדת הקוד של המאמר
להורדת של התרגיל שהצגתי בסרטון

להלן סרטון המדגים כיצד לבצע את התהליך:

כך, אם נסתכל על לוח הסודו מהאתר הבא:

נוכל לחלק אותו ל-4 החוקים הבאים:

• בכל תא עלינו להזין מספר מ-1 ועד 9
• כל שורה חייבת להכיל מספרים ייחודיים
• כל עמודה חייבת להכיל מספרים ייחודיים
• כל ריבוע קטן של 3 על 3 חייב להכיל מספרים ייחודיים

כעת ניקח חוקים אלו ונהפוך אותם לקוד, שלב אחר שלב.

נתחיל עם הגדרת המשתנים:

המשתנים:

• game – יכיל את כל המשחק ברשימה כאשר כל תא ב-game הוא שורה בלוח
• board_rules – יכיל את החוק שעל כל תא להיות מספר בין 1 ל-9
• row_rules – יכיל את החוק שעל כל שורה להיות ייחודית
• column_rules – יכיל את החוק שעל כל עמודה להיות ייחודית
• cube_3x3_rules – יכיל את החוק שעל כל קובייה קטנה להיות ייחודית


לאחר שהגדרנו את המשתנים שלנו נעבור להגדרת החוקים, נגדיר את game להכיל את המשתנים מסוג Int ונגדיר שכל תא חייב להיות בין 1 ל-9 באמצעות And בצורה הבאה:

כדי לדאוג שבכל שורה יש לנו מספרים ייחודיים נשתמש ב-Distinct כך:

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

נעבור להגדרת חוקיי הקובייה הקטנה של ה-3 על 3, כדי לעשות זאת נגדיר משתנה עזר שיכיל את כל הקוביות:

כעת נגדיר מספר תנאים שיחלקו את כל הערכים ב-[game[x][y לפי הקוביות:

לאחר שנסיים לחלק את כל הערכים לפי המיקום שלהם לקוביות נבצע Distinct על כל קובייה בנפרד ונשמור את התוצאה ב-cube_3x3_rules.

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

ונגדיר את המצב ההתחלתי כך:

] כך נגדיר תנאי בZ3- באמצעות If, התנאי יבדוק האם הערך במקום ה-[game[x][y הוא 0 אז לא ניצור שום חוק אחרת אם יש לנו מספר כלשהו אז הערך במקום ה-[game[x][y חייב להיות שווה למספר הזה.

כעת עלינו להוסיף את כל החוקים האלה לתוך הSolver- של Z3 אשר יפתור בשבילנו את התרגיל:

נעשה בדיקה האם החוקים שהגדרנו הגיוניים והסודוקו שלנו פתיר ולאחר מכן נפתור את הסודוקו באמצעות Model כך:

התוצאה תראה כך: