Binairo Puzzle

ปริศนาบินไนโร

การแนะนำ

โปรเจ็กต์นี้ประกอบด้วยการไขปริศนา Binairo (ดูเกมออนไลน์ที่นี่) หรือที่เรียกว่า Takuzu และอธิบายไว้ดังต่อไปนี้ เรามีตารางของเซลล์ nxn ที่อาจมีวงกลมสีขาวหรือวงกลมสีดำ การกำหนดค่าเริ่มต้นจะให้ค่าของเซลล์บางส่วน และส่วนที่เหลือจะต้องเต็มไปด้วยวงกลมตามกฎต่อไปนี้:

• แต่ละแถวและแต่ละคอลัมน์จะต้องมีจำนวนวงกลมของแต่ละสีเท่ากัน นั่นคือ n/2 กรณีของแต่ละกรณี

• จะต้องมีวงกลมสีเดียวกันติดต่อกันไม่เกิน 2 วงในทิศทางใดๆ (แนวตั้งหรือแนวนอน)

• ไม่สามารถมีสองแถวหรือสองคอลัมน์ที่มีการกำหนดค่าเดียวกันได้

ตัวอย่างของการกำหนดค่าเบื้องต้นและวิธีแก้ปัญหาที่เกี่ยวข้องสามารถดูได้ด้านล่าง

การนำไปปฏิบัติ

มันจะเข้ารหัสสถานการณ์ทั้งเป็นปัญหา SAT และโปรแกรม ASP

ซึ่งใช้ไฟล์ ASCII ที่มีตารางเริ่มต้นซึ่งแต่ละเซลล์มีอักขระ: '0' (วงกลมสีขาว), '1' (วงกลมสีดำ) หรือ '.' (เซลล์ว่างที่จะเติม) บรรทัดแรกประกอบด้วยเลขคู่ n>=2 ระบุจำนวนแถวและคอลัมน์ (เรามีตารางสี่เหลี่ยม) ตัวอย่างเช่น ตัวอย่างในภาพด้านบนจะแสดงเป็น:

 6
......
.11.0.
01....
....00
.1....
0..1..

โปรแกรมนี้จะสร้างไฟล์ DIMACS และทำการเรียกจากภายนอกเพื่อ ประสาน เมื่อใช้ SAT หรือ clingo เมื่อใช้ ASP เพื่อรับวิธีแก้ปัญหา นอกจากนี้ยังจะถอดรหัสกลับเอาต์พุตและพิมพ์โซลูชันที่สมบูรณ์ดังต่อไปนี้:

 100110
011001
010011
101100
110010
001101

การดำเนินการ

ตามค่าเริ่มต้น จะใช้ ASP และโฟลเดอร์ตัวอย่างประกอบด้วยชุดการวัดประสิทธิภาพที่มีขนาดแตกต่างกัน (6, 8, 10, 14, 20) โดยที่ domX.txt เป็นไฟล์อินพุต และ solX.txt เป็นโซลูชันที่สอดคล้องกัน

 ./binairo.py [-h] [-a] [-c input] input

-h            show this help message and exit
-a            use ASP to solve
-c            compare the result with this file
-input        route of the binairo puzzle instance