Pada makalah ini penulis membuat sistem pemecah sudoku interaktif menggunakan logika proposisi dalam
Python. Sudoku merupakan sebuah permainan teka-teki logika yang mana pemain harus mengisi matriks
N × N, yang berisi beberapa petunjuk, sehingga setiap baris, kolom, dan submatrix n × n berisi setiap bi-
langan bulat dari 1 hingga N tepat satu kali. Salah satu metode yang cukup dikenal untuk penyelesaian
sudoku adalah Constraint programming. Makalah ini menyajikan proses pemecahan sudoku sebagai ma-
salah keterpenuhan formula proposisional dalam Python. Aturan sudoku akan diubah menjadi formula
logika proposisi. Lalu formula digunakan sebagai masukan SAT solver untuk menemukan solusi sudoku.
Python digunakan karena implementasinya yang sederhana. Sistem menghasilkan keluaran dari masukan
pengguna secara interaktif. Fungsionalitas dari sistem diuji dengan metode pengujian kotak hitam. Sistem
dapat memenuhi semua spesifikasi pada rencana uji yang dibuat. Penulis juga menguji performansi sistem.
Selain itu penulis menemukan banyak klausa yang dibutuhkan SAT solver untuk menemukan solusi dari
sebuah sudoku di setiap iterasinya. Sistem dapat menemukan ? 100 solusi dari sudoku.