Proyek ini terdiri dari pemecahan teka-teki Binairo (lihat di sini game online), juga disebut Takuzu, dan dijelaskan sebagai berikut. Kami memiliki kisi sel nxn yang mungkin berisi lingkaran putih atau lingkaran hitam. Konfigurasi awal menyediakan beberapa nilai sel dan sisanya harus diisi lingkaran sesuai aturan berikut:
Setiap baris dan kolom harus berisi jumlah lingkaran yang sama untuk setiap warna, yaitu n/2 instance dari setiap kasus.
Tidak boleh ada lebih dari 2 lingkaran berurutan dengan warna yang sama ke segala arah (vertikal atau horizontal).
Tidak boleh ada dua baris atau dua kolom dengan konfigurasi yang sama.
Contoh konfigurasi awal dan solusi terkait dapat dilihat di bawah.
Ini akan mengkodekan skenario baik sebagai masalah SAT dan sebagai program ASP.
Ini mengambil file ASCII dengan grid awal di mana setiap sel berisi karakter: '0' (lingkaran putih), '1' (lingkaran hitam) atau '.' (sel kosong untuk diisi). Baris pertama berisi bilangan genap n>=2 yang menentukan jumlah baris dan kolom (kita memiliki kotak persegi). Misalnya, contoh pada gambar di atas akan direpresentasikan sebagai:
6
......
.11.0.
01....
....00
.1....
0..1..
Program ini akan menghasilkan file DIMACS dan membuat panggilan eksternal ke gesper saat menggunakan SAT atau clingo saat menggunakan ASP untuk mendapatkan solusi. Ini juga akan memecahkan kode kembali keluaran dan mencetak solusi lengkap sebagai berikut:
100110
011001
010011
101100
110010
001101
Secara default, ini menggunakan ASP dan folder contoh berisi sekumpulan tolok ukur dengan ukuran berbeda (6, 8, 10, 14, 20), dengan domX.txt sebagai file input dan solX.txt sebagai solusi terkait.
./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