-
Notifications
You must be signed in to change notification settings - Fork 0
/
README.md.old
130 lines (96 loc) · 11.1 KB
/
README.md.old
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
# About
**SudokuAreEz-SAT** adalah project yang mengaplikasikan _Satisfiability_ dalam _Propositional Logic_ (Matematika Diskrit) untuk menyelesaikan permainan [Sudoku](https://en.wikipedia.org/wiki/Sudoku) dengan bantuan komputer.
Project ini, merupakan sarana untuk menerapakan ilmu yang telah diperoleh **(Learning Purpose)**.
# Note To Reader
**Disaranakan** untuk menonaktifkan dark mode, ketika membaca [Project Notes](#project-notes)
Mohon maaf, jika pada bagian [Project Notes](#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!](https://github.com/afifabroory/SudokuAreEz-SAT/discussions)
# Project Notes
Logika Matematika adalah ilmu berfikir atau penalaran untuk menyimpulkan dan verifikasi dari sebuah statement.
***Contoh 1.1:*** \
Perhatikan statement matematika berikut, &space;=&space;1&space;+&space;2&space;+&space;...&space;+&space;n&space;=&space;\frac{n\left(n&space;+&space;1\right)}{2}\right]) dimana ℕ adalah bilang asli (1, 2, 3, ... [Silahkan buka [_Discussions_](https://github.com/afifabroory/SudokuAreEz-SAT/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 &space;\implies&space;P(n&space;+&space;1)&space;\right&space;]).
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 :joy:. \
(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 :sweat_smile:, statement tersbut tetap True.
> ... (3) Saya adalah orang Indonesia **atau** Saya adalah kuda adalah contoh dari _compound proposition_ yang dihubungkan dengan [_logical connectives_](https://en.wikipedia.org/wiki/Logical_connective) 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)](https://en.wikipedia.org/wiki/First-order_logic) 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.
<br>
[Sudoku](https://en.wikipedia.org/wiki/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](https://en.wikipedia.org/wiki/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. \
}_\text{T}) \
Proposition diatas merupakan Satisfiable, karena terdapat truth value True, ketika a adalah True dan b adalah False.
(2) Misalkan literal a adalah True. \
}_\text{F}) \
Proposition diatas merupakan Unsatisfiable, karena tidak terapat truth value True sekalipun pada Truth Table. Maka, negation dari compound proposition tersbeut adalah Tautology &space;\leftrightarrow&space;\text{T})
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)](https://en.wikipedia.org/wiki/Conjunctive_normal_form#Conversion_into_CNF)
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 \
}^\text{Disj.%20of%20Literals}%20\wedge%20\overbrace{(q%20\vee%20\neg%20r)}^\text{Disj.%20of%20Literals}%20\wedge%20\overbrace{(r%20\vee%20\neg%20p)}^\text{Disj.%20of%20Literals}%20}_\text{Conjunction%20of%20Clauses})
 Merupakan CNF, karena secara implisit terdapat Conjunction dengan clauses constant True. 
> Untuk contoh lebih, bisa dilihat di [Conjunctive Normal Form (Wikipedia)](https://en.wikipedia.org/wiki/Conjunctive_normal_form#Examples_and_non-examples)
**Algoritma untuk konversi bentuk propositional formula ke dalam bentuk CNF (sering digunakan):**
> 1) Merubah semua bi-implication [Jika ada] \
> 
> 2) Merubah semua implication [Jika ada] \
> 
> 3) Menerapakan De Morgan's Law [Jika bisa] \
> 
> 4) Menerapkan Distributive Law [Jika bisa] \
> 
***Contoh 1.5:*** \
Pada contoh konversi ini akan mengambil contoh dari pertanyaan yang di ajukkan di [stackoverflow.com](https://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))`
>
> [stackoverflow.com](https://stackoverflow.com/questions/655261/how-to-convert-a-propositional-formula-to-conjunctive-normal-form-cnf)
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](minisat.se) 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
