─────╷────────── $𝖘𝖑𝖑𝖐/𝖘𝖑𝖎𝖙𝖍𝖊𝖗𝖑𝖎𝖓𝖐-𝖗𝖚𝖑𝖊𝖘.𝖘𝖆𝖕𝖕𝖍𝖎𝖗𝖊 ────────────────────────────────────────────────────
0┊-------------------------------| Slitherlink Rules in Sapphire |--------------------------------
1┊--|∙An∙n×m∙grid∙of∙cells,∙n>1,∙m>1,∙some∙cells∙are∙shown∙containing∙numbers∙from∙0∙to∙3.
2┊--|∙The∙solution∙is∙a∙single,∙non-intersecting∙loop∙on∙the∙edges,∙where∙the∙number∙of∙edges
3┊--|∙used∙around∙each∙pime∙cell∙is∙equal∙to∙the∙number∙given.
4┊
5┊--|∙borders∙are∙defined∙to∙be∙0
6┊--|∙pim∙-∙a∙map∙from∙the∙n×m∙cells∙to∙{0⋯3};∙number∙of∙the∙cells∙edges∙in∙the∙loop
7┊--|∙hrz∙-∙a∙map∙of∙the∙n×(m+1)∙horizontal∙edges∙to∙{0∙1};∙1∙means∙in∙the∙solution
8┊--|∙vrt∙-∙a∙map∙of∙the∙(n+1)×m∙vertical∙edges∙to∙{0∙1};∙1∙means∙in∙the∙solution
9┊--|∙flo∙-∙the∙number∙of∙edges∙connected∙to∙each∙of∙the∙(n+1)×(m+1)∙vertices
10┊--|∙dst∙-∙⦗dst∙a∙b∙c∙d⦘∙is∙the∙distance∙between∙two∙vertices∙on∙the∙path;∙A0∙if∙unconnected
11┊
12┊--|∙The∙border∙of∙both∙hrz∙and∙vrt∙are∙padded∙with∙0
13┊--|∙The∙constraint∙on∙pim∙means∙1×1∙cell∙puzzles∙aren't∙allowed
14┊--|∙flo∙enforces∙non-intersection∙and∙the∙solution∙is∙one∙or∙more∙loops
15┊--|∙dst∙enforces∙single∙loop∙connectivity
16┊--|∙∙∙a∙relation∙indicating∙connectivity∙can∙be∙satisfied∙simply∙by∙enforcing∙connectivity
17┊
18┊
19┊∀a∈{0⋯n}∙⦗vrt∙a∙⨪1⦘=0∙∧∙⦗vrt∙a∙m⦘=0∙∧∙∀b∈{0⋯m⨫1}∙⦗vrt∙a∙b⦘∈{0∙1}
20┊∀b∈{0⋯m}∙⦗hrz∙⨪1∙b⦘=0∙∧∙⦗hrz∙n∙b⦘=0∙∧∙∀a∈{0⋯n⨫1}∙⦗hrz∙a∙b⦘∈{0∙1}
21┊
22┊∀a∈{⨪1⋯n+1}∙⦗flo∙a∙⨪1⦘=0∙∧∙⦗flo∙a∙m+1⦘=0
23┊∀b∈{⨪1⋯m+1}∙⦗flo∙⨪1∙b⦘=0∙∧∙⦗flo∙n+1∙b⦘=0
24┊
25┊∀⟨a∙b⟩∈{0⋯n⨫1}×{0⋯m⨫1}∙⦗pim∙a∙b⦘∈{0⋯4}∙∧∙⦗pim∙a∙b⦘=⦗vrt∙a∙b⦘+⦗vrt∙a+1∙b⦘+⦗hrz∙a∙b⦘+⦗hrz∙a∙b+1⦘
26┊
27┊∀⟨a∙b⟩∈{0⋯n}×{0⋯m}
28┊∙∙⦗flo∙a∙b⦘∈{0∙2}∙∧∙⦗flo∙a∙b⦘=⦗vrt∙a∙b⨫1⦘+⦗vrt∙a∙b⦘+⦗hrz∙a⨫1∙b⦘+⦗hrz∙a∙b⦘
29┊
30┊
31┊--|∙Before∙single∙loop∙constraint,∙define∙cells∙as∙interior∙or∙exterior
32┊
33┊∀⟨x∙y⟩∈{0⋯n⨫1}×{0⋯m⨫1}
34┊∙∙⦗in?∙x∙y⦘∈{0∙1}
35┊∙∙x=0∙∙∙⇒∙⦗in?∙x∙y⦘=⦗vrt∙x∙y⦘
36┊∙∙x>0∙∙∙⇒∙(⦗in?∙x∙y⦘=⦗in?∙x⨫1∙y⦘∙⇐⇒∙⦗vrt∙x∙y⦘=0)
37┊∙∙x<n⨫1∙⇒∙(⦗in?∙x∙y⦘=⦗in?∙x+1∙y⦘∙⇐⇒∙⦗vrt∙x+1∙y⦘=0)
38┊∙∙x=n⨫1∙⇒∙⦗in?∙x∙y⦘=⦗vrt∙x+1∙y⦘
39┊∙∙y=0∙∙∙⇒∙⦗in?∙x∙y⦘=⦗hrz∙x∙y⦘
40┊∙∙y>0∙∙∙⇒∙(⦗in?∙x∙y⦘=⦗in?∙x∙y⨫1⦘∙⇐⇒∙⦗hrz∙x∙y⦘=0)
41┊∙∙y<m⨫1∙⇒∙(⦗in?∙x∙y⦘=⦗in?∙x∙y+1⦘∙⇐⇒∙⦗hrz∙x∙y+1⦘=0)
42┊∙∙y=m⨫1∙⇒∙⦗in?∙x∙y⦘=⦗hrz∙x∙y+1⦘
43┊
44┊
45┊dc=(n+1)·(m+1)
46┊
47┊x0∈{0⋯n}∙∧∙y0∈{0⋯m}∙∧∙⦗id∙x0∙y0⦘=0
48┊
49┊--|∙path∙goes∙clockwise∙around∙the∙interior
50┊∀⟨x∙y⟩∈{0⋯n⨫1}×{0⋯m⨫1}
51┊∙∙⦗in?∙x∙y⦘=1∙⇒
52┊∙∙∙∙⦗hrz∙x∙y⦘=1∙⇐⇒∙⦗id∙x+1∙y⦘=⦗id∙x∙y⦘+1
53┊∙∙∙∙⦗vrt∙x+1∙y⦘=1∙⇐⇒∙⦗id∙x+1∙y+1⦘=⦗id∙x+1∙y⦘+1
54┊∙∙∙∙⦗hrz∙x∙y+1⦘=1∙⇐⇒∙⦗id∙x∙y+1⦘=⦗id∙x+1∙y+1⦘+1
55┊∙∙∙∙⦗vrt∙x∙y⦘=1∙⇒∙⦗id∙x∙y⦘=⦗id∙x∙y+1⦘+1∙∨∙⦗id∙x∙y⦘=0
56┊∙∙∙∙y0<=y∙∧∙(y0=y∙⇒∙x0<=x)
57┊
58┊∙∙⦗in?∙x∙y⦘=0∙⇒
59┊∙∙∙∙⦗hrz∙x∙y⦘=1∙⇐⇒∙⦗id∙x∙y⦘=⦗id∙x+1∙y⦘+1
60┊∙∙∙∙⦗vrt∙x+1∙y⦘=1∙⇐⇒∙⦗id∙x+1∙y⦘=⦗id∙x+1∙y+1⦘+1∨⦗id∙x+1∙y⦘=0
61┊∙∙∙∙⦗hrz∙x∙y+1⦘=1∙⇐⇒∙⦗id∙x+1∙y+1⦘=⦗id∙x∙y+1⦘+1
62┊∙∙∙∙⦗vrt∙x∙y⦘=1∙⇒∙⦗id∙x∙y+1⦘=⦗id∙x∙y⦘+1
63┊
64┊
65┊∀⟨x∙y⟩∈{0⋯n}×{0⋯m}
66┊∙∙⦗id∙x∙y⦘∈{0⋯dc}
67┊∙∙⦗id∙x∙y⦘=0∙⇐⇒∙x=x0∙∧∙y=y0
68┊∙∙⦗flo∙x∙y⦘=0∙⇐⇒∙⦗id∙x∙y⦘=dc
69┊∙∙--|∙⦗flo∙x∙y⦘=2∙⇒∙y0<=y∙∧∙(y0=y∙⇒∙x0<=x)
70┊∙∙--|∙∀⟨x'∙y'⟩∈{0⋯n}×{0⋯m}
71┊∙∙--|∙∙∙⦗id∙x∙y⦘¬=0∧⦗id∙x∙y⦘¬=dc∙⇒
72┊∙∙--|∙∙∙⦗id∙x∙y⦘=⦗id∙x'∙y'⦘∙⇐⇒∙x=x'∧y=y'∨⦗id∙x∙y⦘=dc∧⦗id∙x'∙y'⦘=dc
73┊ --| ⦗id x y⦘=0 ⇒ x<n ∧ y<m ∧ (⦗id x' y'⦘<=⦗id x y+1⦘ ∧ (y'>y ∨ y'=y ∧ x'>=x) ∨ ⦗id x' y'⦘=dc
74┊
75┊∙∙--|∙(∀⟨x'∙y'⟩∈{0⋯n}×{0⋯m}∙y'<y∙∨∙y'=y∧x'<x∙⇒∙⦗id∙x'∙y'⦘=dc)∙⇒∙⦗id∙x∙y⦘∈{0∙dc}
76┊∙∙--|∙really∙want∙to∙make∙use∙of∙the∙following∙and∙its∙contrapositive
77┊∙∙--|∙⦗id∙x∙y⦘=0∙⇒∙∀⟨x'∙y'⟩∈{0⋯n}×{0⋯m}∙y'<y∙∨∙y'=y∧x'<x∙⇒∙⦗id∙x'∙y'⦘=dc
─────╵────────────────────────────────────────────────────────────────────────────────────────────────