SudokuAreEz-SAT adalah project yang mengaplikasikan Satisfiability dalam Propositional Logic (Matematika Diskrit) untuk menyelesaikan permainan Sudoku dengan bantuan komputer.
Project ini, merupakan sarana untuk menerapakan ilmu yang telah diperoleh (Learning Purpose).
Disaranakan untuk menonaktifkan dark mode, ketika membaca Project Notes
Mohon maaf, jika pada bagian Project Notes tidak menggunakan bahasa baku atau tidak se-utuhnya menggunakan bahasa Indonesia yang baik dan benar, dan tidak menjelaskan istilah-istilah Matematika serta jika terdapat kesalahan atau kekurangan dalam penjelasan.
Any suggestion or question? Create new Discussion here!
Logika Matematika adalah ilmu berfikir atau penalaran untuk menyimpulkan dan verifikasi dari sebuah statement.
Contoh 1.1:
Perhatikan statement matematika berikut, dimana ℕ adalah bilang asli (1, 2, 3, ... [Silahkan buka Discussions baru di project ini untuk list lengkap bilangan bulat]).Statement tersebut adalah statement True.
Proof:
(1) Statement True untuk n = 1, P(1)
(2) n = k, Statement True untuk P(k)
(3) Statement juga True untuk P(k + 1)
Sehingga dapat disimpulkan bahwa statement tersebut adalah True .
Propositional Logic adalah cabang logika yang berkiatan dengan propositions. Propositions adalah statement yang memiliki Truth Value diantara True dan False, sebuah proposition tidak dapat memiliki dua nilai Truth Value.
Contoh 1.2:
(1) Indonesia Merdeka pada tahun 1945. Statement tersebut adalah True.
(2) Bandung adalah ibu kota Amerika Serikat. Statement tersebut adalah False 😂.
(3) Saya adalah orang Indonesia atau Saya adalah kuda. Statement tersebut adalah True karena saya adalah orang Indonesia, tidak peduli apakah saya kuda atau tidak 😅, statement tersbut tetap True.
... (3) Saya adalah orang Indonesia atau Saya adalah kuda adalah contoh dari compound proposition yang dihubungkan dengan logical connectives atau operator logika (i.e. Conjunction, Disjunction, Negation, Material Implication/Implies dan Bi-Implication)
(4) x + 2 = 10. Statement tersebut bukan merupakan propositions, dikarenakan Truth Value tersebut tergantung dengan nilai yang diberikan pada variable x.
... (4) Konsep ini dipelajari dalam First-Order Logic (FOL) yang mana merupakan pelengkap kekurangan dari propositions logic, karena proposition logic tidak dapat merepresentasikan semua jenis Statement Matematika. Pada Contoh 1.1 merupakan FOL, ketika sebuah nilai dari domain dimasukkan ke variable x pada predicate function maka statement tersebut akan menjadi proposition.
Logika Matematika memegang peran dalam dunia Teknologi Informasi, sebagai contoh penerapan logika, yaitu pada:
- Arsitektur Komputer
- Program Verification dan Validation
- Artificial Intelligence
- Automated Theorem Proving
- dll.
Pada project ini akan menerapkan Logika Matematika dalam menyelesaikan permainan Sudoku.
Sudoku merupakan permainan logic based, dengan tujuan permainan adalah mengisi penuh semua cell kosong dengan angka sesuai dengan jumlah cell pada Sudoku (e.g. Sudoku 9x9 maka mengisi angka 1-9).
Pada Sudoku 9x9 terdapat kotak kecil dengan ukuran 3x3, yang mana pada kotak kecil 3x3 terdapat cell kosong yang perlu disi penuh sesuai dengan syarat permainan Sudoku.
Gambar 1.1: Contoh permainan Sudoku, dari Sudoku.com
Syarat mengisi cell kosong tersebut yaitu:
- Baris dan Kolom pada cell kosong tersebut belum terdapat angka yang akan di masukkan (Baris dan kolom angkanya harus unique).
- Pada kotak kecil dibagian cell yang kosong belum terdapat angka yang akan dimasukkan.
Namun, yang perlu diperhatikan dalam mengisi cell kosong pada Sudoku adalah perhatikan lokasi angka atau kombinasi angka yang digunakan.
Terdapat berbagai macam teknik untuk menyelesaikan permaianan Sudoku dengan bantuan komputer, seperti Backtracking, SAT Problem, Stochastic search, dll. Pada project ini menggunakan teknik Satisfiability (SAT) Problem. SAT Problem dikategorikan di dalam NP-Complete.
SAT Problem adalah problem yang menentukan apakah sebuah Boolean Formula Satisfiable atau Unsatisfiable. Sebuah formula X disebut satisfiable jika paling tidak terdapat nilai True, pada Truth Table. Sedangkan, sebuah formula X adalah unsatisfiable jika dan hanya jika (iff) ¬X adalah Tautology atau dengan kata lain, X tidak memiliki truth value True sama sekali pada Truth Table.
Contoh 1.3:
(1) Misalkan, literal a adalah True sedangkan b adalah False.
Proposition diatas merupakan Satisfiable, karena terdapat truth value True, ketika a adalah True dan b adalah False.
(2) Misalkan literal a adalah True.
Proposition diatas merupakan Unsatisfiable, karena tidak terapat truth value True sekalipun pada Truth Table. Maka, negation dari compound proposition tersbeut adalah Tautology
Dalam SAT Problem, sebuah compound proposition harus dirubah ke dalam bentuk Conjunctive Normal Form (CNF).
Fakta menarik dari CNF adalah semua proposition dapat dibentuk kedalam bentuk CNF.
Every propositional formula can be converted into an equivalent formula that is in CNF. This transformation is based on rules about logical equivalences: double negation elimination, De Morgan's laws, and the distributive law.
Conjunctive normal form (Wikipedia)
Sebuah expression X dalam bentuk CNF jika memiliki pola atau diekspresikan sebagai Conjunction of Clauses, dimana Clauses adalah Disjunction of Literals (Conjunction Of Disjunction of Literals).
Contoh 1.4:
Berikut adalah contoh-contoh expression dalam bentuk CNF
Merupakan CNF, karena secara implisit terdapat Conjunction dengan clauses constant True.
Untuk contoh lebih, bisa dilihat di Conjunctive Normal Form (Wikipedia)
Algoritma untuk konversi bentuk propositional formula ke dalam bentuk CNF (sering digunakan):
- Merubah semua bi-implication [Jika ada]
- Merubah semua implication [Jika ada]
- Menerapakan De Morgan's Law [Jika bisa]
- Menerapkan Distributive Law [Jika bisa]
Contoh 1.5:
Pada contoh konversi ini akan mengambil contoh dari pertanyaan yang di ajukkan di stackoverflow.com
How to convert a propositional formula to conjunctive normal form (CNF)?
How can I convert this equation to CNF?
¬((p ∨ ¬Q) ⊃ R) ⊃ (P ∧ R))
Dari pertanyaan yang diajukan tersebut, tanda kurung pada propositions agak membingungkan. Sehingga terdapat dua kemungkinan yang dimaksudkan, yaitu: ¬[({p ∨ ¬Q} ⊃ R) ⊃ (P ∧ R)] atau ¬([p ∨ ¬Q] ⊃ R) ⊃ (P ∧ R).
Jika yang dimaksud adalah ¬[({p ∨ ¬Q} ⊃ R) ⊃ (P ∧ R)]
Bentuk akhirnya adalah ¬p ∧ q ∧ r ∧ p yang mana merupakan bentuk CNF dan DNF.
Jika yang dimaksud adalah ¬([p ∨ ¬Q] ⊃ R) ⊃ (P ∧ R)
Bentuk akhirnya adalah ¬p ∨ ¬r yang mana merupakan bentuk CNF dan DNF.
Note: Selalu lihat referensi, logical equivalent rule ketika konversi ke CNF!
Tools:
Project ini mengunakan SAT Solver MiniSAT untuk menyelesaikan Satisfiability Problem
Sudoku Database:
https://www.menneske.no/sudoku/eng/
Project Reference:
http://anytime.cs.umass.edu/aimath06/proceedings/P34.pdf
https://cse.buffalo.edu/~erdem/cse331/support/sat-solver/index.html
http://swtv.kaist.ac.kr/courses/cs453-fall12/sudoku.pdf
https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/SATLINK____DIMACS
http://www.cs.cmu.edu/~hjain/papers/sudoku-as-SAT.pdf
https://www.andrew.cmu.edu/user/vipuls/me/SudokuSATProjectReport.pdf