-
Notifications
You must be signed in to change notification settings - Fork 0
/
cdcl-sat-solvers.saty
1216 lines (1167 loc) · 51.6 KB
/
cdcl-sat-solvers.saty
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
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
@require: class-slydifi/theme/arctic
@require: ruby/ruby
@require: easytable/easytable
@require: bibyfi/bibyfi
@require: bibyfi/bibyfi-IEEETran
@require: azmath/azmath
@require: matrix/matrix
@require: colorbox/colorbox
@require: arrows/arrows
@require: arrows/commands
@require: fss/fss
@require: fss/fonts
@require: latexcmds/latexcmds
@require: fss/style
@require: base/list-ext
@require: enumitem/enumitem
@import: Colors
@import: tikzyfi
@import: references
@import: presets
@import: theorems
@import: mymath
@import: utils
@import: diagrams
@import: dpll-machine
let bw = SlydifiOverlay.between
open LatexCmds
open SlydifiOverlay
open FigBox
open ArrowCommands
open MyMath
open EasyTableAlias
open TikZyFi
let math-int i = math-char MathInner (arabic i)
type 'a phantomer = 'a -> 'a constraint 'a :: (|phantom: bool|)
let phantom: 'a phantomer = fun dcf -> phantom (select-from-two dcf true false)
let-math \dec lit = ${#lit^\mathrm{d}}
let-math \Dec lit = ${\mathop{\mathrm{Decide}} #lit}
let-math \UP lit = ${\mathop{\mathrm{UnitProp}} #lit}
let-math \Bt lit = ${\mathop{\mathrm{Backtrack}} #lit}
let-math \Bj lit = ${\mathop{\mathrm{Backjump}} #lit}
let-math \true args = math-color Colors.green args
let-math \conflict args = math-color Colors.red args
let-math \false args = math-color (Colors.gray 0.6) args
let-math \leads-to = math-char MathRel `⤳`
let-math \rewrites-to reason =
let backsp r = text-in-math MathOrd
(fun ctx -> inline-skip (get-font-size ctx *' (0. -. r)))
in let back1 = backsp 0.2
in let back2 = backsp 0.5
in ${-#back1\p{#reason}#back2\longrightarrow}
let-inline ctx \eqref key =
match get-cross-reference (`eq:` ^ key ^ `:num`) with
| Some(label) ->
read-inline ctx (embed-string (`(` ^ label ^ `)`))
| None -> read-inline ctx { (??) }
let-math \eqrefm key = ${\text!{\eqref(key);}}
let-block ctx +small arg =
read-block (ctx |> set-font-size 18pt) arg
let-inline ctx \small arg =
read-inline (ctx |> set-font-size 18pt) arg
let-block ctx +x-small arg =
read-block (ctx |> set-font-size 15pt) arg
let-inline ctx \x-small arg =
read-inline (ctx |> set-font-size 15pt) arg
let-block ctx +xx-small arg =
read-block (ctx |> set-font-size 12pt) arg
let-inline ctx \xx-small arg =
read-inline (ctx |> set-font-size 12pt) arg
let-math \SAT = ${\mathrm{SAT}}
let-math \CNF = ${\mathrm{CNF}}
let-math \NP = ${\mathrm{NP}}
let sudoku ctx =
let dx = 36pt
in List.concat
[ [ stroke 2.5pt Color.black
(Gr.line (dx *' 2., 0pt) (dx *' 2., dx *' 4.))
; stroke 2.5pt Color.black
(Gr.line (0pt, dx *' 2.) (dx *' 4., dx *' 2.))
]
; List.concat
(Utils.generate 4
(fun j ->
List.concat (Utils.generate 4
(fun i ->
(
let imath = math-int (i + 1) in
let jmath = math-int (j + 1) in
let name = read-inline ctx {${d_{#imath#jmath}}} in
let (w, h, d) = get-natural-metrics name in
[ draw-text
( dx *' float i +' (dx -' w) *' 0.5
, dx *' float j +' (dx -' h) *' 0.5
)
name
; stroke 1pt Color.black
(Gr.rectangle
(dx *' float i , dx *' float j)
(dx *' float (i+1) , dx *' float (j+1))
)
])
)
)))
]
let-block ctx +item ?:cond it blk =
read-block ctx
(match cond with
| Some(cond) ->
'< +phantom(cond)< +item{#it;}<#blk;> > >
| None -> '<+item{#it;}<#blk;>>
)
let override-node-when cond names f =
select-from-two cond (override-node names f) Fn.id
in
document '<
+set-config(slydifi-cfg);
+make-title(|
title = {|充足可能性ソルバ (SATソルバ) の原理|};
author = {|Hiromi ISHII|};
date = {
|2024-03-10
|Tsukuba Computer Mathematics Seminar 2024
|\small{Slides available on \url(`https://konn-san.com/math/cdcl-sat-solvers.pdf`);}
|};
|);
+section{|充足可能性ソルバ (SATソルバ) の原理|}<
+frame{本日の話題：充足可能性問題とSATソルバ}<
+itemize<
+item{\emph{充足可能性問題}：与えられた\emph{命題論理式}が\emph{（古典的に）充足可能}かどうかを判定する問題}<
+item{\emph{古典命題論理式}：\emph{命題変数}${P_1, \ldots, Q_1, \ldots,} を${\land}（かつ）、${\lor}（または）、${\to}（ならば）、${¬}（でない）で結んで得られる論理式}<>
+item{\emph{古典的充足可能性}: 与えられた式を真とするような、命題変数への真偽値${\circ}（真）または${\times}（偽）の割り当てが存在するか？}<>
>
+item{充足可能性（\emph{SAT}isfiability）を略して SAT と呼ぶ。}<>
+item{\emph{NP-完全}：総当たりで解けるような任意の問題が SAT に帰着できる}<
+item{本来 ${\SAT} は判定問題だが、具体的な求解まで含めて${\SAT}と呼ぶ事が多い}<>
>
+item{色々な問題が SAT （やその拡張である SMTソルバ）で解け、実用上も重要}<>
>
>
+frame{SATで解ける問題の例：論理パズル}<
+question?:({三人の島民 \cite[`Smullyan:2008`];})?:(false){
常に嘘だけをいう嘘吐きと、本当のことだけをいう正直者だけが住む島で、A, B, C三人の島民に出会った。彼らのいうことには：
\listing{
* A：「BとCはどちらも正直者だ」
* B：「Aは嘘吐きで、Cは正直者だ」
}
A, B, C はそれぞれ正直者か、嘘吐きか？
}
>
+frame{三人の島民：回答}<
+itemize<
+item{${A, B, C}を「Aが正直者」「Bが正直者」「Cが正直者」を表す命題変数とする}<>
+item{情報を命題論理式に変換して${\eqrefm!(`q1-cond1`) \land \eqrefm!(`q1-cond2`)}を充足する解を求めればよい：
\align(${
| A | \longleftrightarrow B \land C \label?:!(`PA`)!(`q1-cond1`)
| B | \longleftrightarrow \lnot A \land C \label?:!(`PB`)!(`q1-cond2`)
|
});
}<>
+item{真理表を書いてみると、\emph{全員嘘吐き}だとわかる。}<>
>
+x-small< +centering(
let show p = if p then {${\circ}} else {${\times}} in
let iff p q = (p && q) || ((not p) && (not q)) in
let mkRow a b c =
(let one = iff a (b && c) in
let two = iff b (not a && c) in
List.map show [a; b; c; one; two; one && two]
) in
let mkTable as0 bs cs =
List.append
{| ${A} | ${B} | ${C} | ${\eqrefm!(`q1-cond1`)} | ${\eqrefm!(`q1-cond2`)}
| ${\eqrefm!(`q1-cond1`) \land \eqrefm!(`q1-cond2`)}
|}
(Utils.concat-map
(fun a ->
Utils.concat-map
(fun b -> Utils.concat-map (mkRow a b) cs)
bs
)
as0
)
in {
\easytable[c;c;c;c;c;c](mkTable [true] [true; false] [true; false]);
\quad;
\easytable?:[t; b; m 1; bg-r (Color.rgb 0.4 1.0 0.6) 4 5][c;c;c;c;c;c]
(mkTable [false] [true; false] [true; false]);
});>
>
+frame{SATで解ける問題の例：数独}<
+fig-on-right(from-graphics-given-context (150pt, 150pt) sudoku)<
+itemize<
+item{簡単な例として、 ${4 \times 4} の小さな数独の問題を SAT で解くことを考える。}<>
+item{${i, j, k \leq 4} に対し命題変数 ${P^{=k}_{ij}} を用意する（${d_{ij} = k} というきもち）。}<>
>
>
+itemize<
+item{各マスには ${1, 2, 3, 4} のいずれかの数字一つを入れる。
\gather?:(AZMathEquation.notag)(${|
\bigwedge_{i \leq 4} \bigwedge_{j \leq 4} \pb{
\p{P^{=1}_{ij} \vee P^{=2}_{ij} \vee P^{=3}_{ij} \vee P^{=4}_{ij}} \land
\bigwedge_{k \leq 4} \bigwedge_{l \neq k} \paren{P^{=k}_{ij} \longrightarrow \lnot P^{=l}_{ij}}
}
|});}<>
>
>
+frame{SATで解ける問題の例：数独（続）}<
+itemize<
+item{各行、各列、各 ${2 \times 2} の小ブロックには各数字 ${1, \ldots, 4} が一つずつ入る。}<
+item{「各行」は次のように書ける（「各列」も${i,j}の役割を入れ換え同様）：
\eqn?:(AZMathEquation.notag)(${
\bigwedge_{i \leq 4} \bigwedge_{k \leq 4} (P^{=k}_{i1} \vee P^{=k}_{i2} \vee P^{=k}_{i3} \vee P^{=k}_{i4})
});
}<>
+item{\emph{演習問題}：「一意性」の条件が要らない理由を考えてみよう。}<>
+item{\emph{演習問題}：「各ブロック」の条件を書き下してみよう。}<>
>
+item{あとは盤面の情報を${P_{ij}^{=k}}のandで与えれば個別の問題を解ける！}<>
>
>
+frame{SATで解ける問題の例：命題論理の定理自動証明}<
+itemize<
+item{SATソルバは定理の自動証明にも使える}<>
>
+thm?:({古典命題論理の完全性定理および健全性定理 (Gödel)})?:(false){
任意の古典命題論理式 ${\phi} に対し、${\phi} がどんな真偽値の割り当てに対しても真であることと、${\phi} が証明可能であることは同値である。
}
+cor?:({証明可能性の特徴付け})?:(false){
任意の古典命題論理式 ${\phi} が証明可能である必要十分条件は、${\lnot \phi} が充足可能でないことである。
}
+itemize<
+item{${\lnot \phi} が充足可能でない事がわかれば、${\phi} が証明できたことになる！}<>
>
>
+frame{SATで解ける問題の例：SMTソルバへ}<
+itemize<
+item{SATだけでも強力だが、更に\emph{述語論理}（${\forall}とか${\exists}とかを入れたやつ）に拡張した \emph{SMT （SAT Modulo Theories）ソルバ}の研究も盛んに行われている}<
+item{代表的なソルバ：Z3, CvC5, etc.}<>
>
+item{SMT で扱える理論の例：線型計画法、整数計画問題、同値関係、配列、etc.}<
+item{数独なんかは配列の理論とかを使ったほうが綺麗}<>
+item{\emph{工学的}にもこれらはかなり重要}<>
+item{定理証明系で人間が手で書きたくない補題の自動証明にも使える}<>
>
+item{SMT は SAT ソルバを外部の理論ソルバと協業させこれらの問題を解く}<
+item{\emph{SAT を如何に速く解くか}が SMT の実装にも重要}<>
>
+item{Disclaimer: 今回は SMT の話はしません}<>
>
>
>
+section{|SATソルバの原理|}<
+frame{SATは「難しい」}<
+itemize<
+item{論理パズルの解法で見たように、すべての命題変数の有り得る真偽値の割り当てを\emph{総当たり}して、\emph{真理表}をつくれば原理的には解ける}<
+item{これは命題変数の数を ${n} とすると \emph{${2^n} 通りの場合分けが必要}になる}<>
+item{もっと効率的な方法はないか？}<>
>
+item{実は\emph{「総当たりで解ける問題」は全て SAT に帰着できる}（${\SAT}は\emph{${\NP}-完全}である）ことが知られている}<
+item{${P \neq \NP} 予想が正しければ、\emph{本質的に効率的な解法は存在しない}}<>
>
+item{本質的に速くなくても\emph{実用的な問題に対し十分速い}手法が研究されている}<
+item{以下ではその中でも主流な\emph{CDCL 法}の原理を簡単に紹介（参考文献\cite[`Zeljic:2019`; `鍋島:2010`; `岩沼:2010`; `Torlak:2003`];）}<>
>
>
>
+frame-nofooter{連言標準形（CNF）}<
+itemize<
+item{SAT ソルバは\emph{連言標準形} (CNF) と呼ばれる形の論理式を扱うことが多い}<
+item{CNF: ${(P \lor \lnot Q \lor R) \land (Q \lor \lnot R) \land (R) \land (S \lor \lnot T)}みたいな論理式}<>
>
>
+x-small<+defn?:({CNFの定義})?:(false){
\enumerate{
* 命題変数${P_i}とその否定${\lnot P_i}を合わせて\emph{リテラル}と呼ぶ。以下、リテラルを表すメタ変数を${l, l_i}などと書く。
* 0個以上のリテラルを「または」で繋いだもの ${l_1 \lor \ldots \lor l_k}を\emph{節}と呼ぶ。以下、節を表すメタ変数を${C, C_i}などと書く。
* 0個以上の節を「かつ」で繋いだ${C_1 \land \ldots \land C_m}の形の論理式を\emph{連言標準形}（Conjunctive Normal Form, \emph{CNF}）と呼ぶ。
}
\emph{注意}：空の節は\emph{矛盾}に、空のCNFは\emph{恒真}に対応する。
}>
>
+frame-nofooter?:(7){任意の命題論理式はCNFで表せる}<
+thm?:({命題論理式のCNFへの変換})?:(false){
任意の命題論理式 ${\phi}は同値なCNF ${\phi_{\CNF}}を持つ。
}
+itemize<
+item{de Morgan 則と分配則を使って変換すればよいが、自乗のオーダーかかる}<>
+item{充足可能性だけを考えればよいのなら、結合子ごとに追加の命題変数${n_i}を導入し、各節のサイズが高々 ${3} のCNF（\emph{${3\text!{-}\CNF}}）に変換できる}<>
>
+fig-on-right(
let overrider ctx =
ctx
|> override-node-when (bw 3 4) [`root`]
[fc Colors.red; tc Colors.white]
|> override-node-when (only 5) [`l`]
[fc Colors.red; tc Colors.white]
|> override-node-when (only 6) [`ld`]
[fc Colors.red; tc Colors.white]
|> override-node-when (only 7) [`r`]
[fc Colors.red; tc Colors.white]
in let diag =
{ \phantom(from 2){\tikzy?:(|
default with
default-node-style =
(|default-node-style with padding=2pt|)
|> circle |> distance 1.25cm
|> style [set-font-size 12pt]
|)
(
let label ctx = ctx |> plain |> distance 3pt |> style [set-font-size 10pt]
in overrider
[ node-at?:[named `root`] (coord (0pt, 0pt)) {${\lor}}
; node-at?:[label] (north-of `root`) {${n_0}}
; node-at?:[named `l`] (south-west-of `root`) {${\lnot}}
; node-at?:[label] (west-of `l`) {${n_1}}
; node-at?:[named `ld`; distance 1cm] (south-of `l`) {${\land}}
; node-at?:[label] (west-of `ld`) {${n_2}}
; node-at?:[named `P`] (south-west-of `ld`) {${P}}
; node-at?:[named `Q`] (south-east-of `ld`) {${Q}}
; node-at?:[named `R`] (south-east-of `root`) {${R}}
; arrow (south-west-of `root`) (north-of `l`)
; arrow (south-east-of `root`) (north-of `R`)
; arrow (south-of `l`) (north-of `ld`)
; arrow (south-west-of `ld`) (north-of `P`)
; arrow (south-east-of `ld`) (north-of `Q`)
]);
}}
in textbox-with-width 6cm diag
)<
+itemize<
+item?:(from 1){論理式 ${\lnot (P \land Q) \lor (R \land S)} のCNFへの変換例：
\phantom(from 2){\x-small{\align?:(AZMathEquation.notag)(${
| \math-color?:!(only 3)!(Colors.red){n_0}
| \land \math-color?:!(only 4)!(Colors.red){(\lnot n_0 \lor n_1 \lor R) \land (\lnot n_1 \lor n_0) \land (\lnot R \lor n_0)}
| | \land \math-color?:!(only 5)!(Colors.red){(\lnot n_1 \lor \lnot n_2) \land (n_1 \lor n_2)}
| | \land \math-color?:!(only 6)!(Colors.red){(\lnot n_2 \lor P) \land (\lnot n_2 \lor Q) \land (\lnot P \lor \lnot Q \lor n_2)}
|});
}}
}<>
+item?:(from 7){\emph{演習問題}：他の結合子の変換規則を考えてみよう。}<>
>
>
>
+frame-nofooter{DPLL: CDCL の祖先}<
+itemize<
+item{CDCLの基礎はDavis–Putnam–Logemann–Loveland (\emph{DPLL})アルゴリズム}<>
+item{基本的な考え方：CNFの節やリテラルを\emph{削れるまで削ってから}場合分け}<
+item{充足された節は削除できる→節が一つもなくなれば充足可能！}<>
+item{偽なリテラルがあれば、節から削除できる→空な節ができたら充足不能！}<>
>
+item{以下の規則に従ってCNFを変形する：}<
+item{\emph{単位節伝播}：リテラル一つだけの節${\pb{l}}があれば${l\equiv\top}とし${\lnot l}を削除}<>
+item{\emph{純リテラル}：肯定または否定のみ出現するリテラル${l}があれば${l\equiv\top}としそのリテラルを含む節を削除（コスト面から\emph{実装しない}事が多い）}<>
+item{\emph{Decide}：他規則が適用できないならリテラルを一つ選び\emph{場合分け}}<
+item{真偽を仮決めし継続。失敗したら巻き戻し (\emph{Backtrack}) 否定で確定し継続}<>
>
>
>
>
+frame?:(7)({DPLL の動作例})(
open DPLL in
let cnf = [[neg 1; pos 2]; [pos 3; pos 4]; [neg 5; neg 6]; [neg 2; neg 5; pos 6]] in
'<
+itemize<
+item{${\pretty-cnf!(cnf)} を DPLL で解いてみよう（\cite[`Zeljic:2019`];の例）。}<>
+item{今後は CNF しか出て来ないので、${\cnf!(cnf)}と略記する}<>
>
+small<
+derive?:(2)
[[neg 1; pos 2]; [pos 3; pos 4]; [neg 5; neg 6]; [neg 2; neg 5; pos 6]]
[ ( dec 1
, [ [ff (-1); pos 2]; [pos 3; pos 4]
; [neg 5; neg 6]; [neg 2; neg 5; pos 6]
]
, [dd 1]
)
; ( unit-prop 2
, [ [ff (-1); tt 2]; [pos 3; pos 4]
; [neg 5; neg 6]; [neg 2; neg 5; pos 6]
]
, [dd 1; lit 2]
)
; ( dec 3
, [ [ff (-1); tt 2]; [tt 3; pos 4]
; [neg 5; neg 6]; [ff (-2); neg 5; pos 6]
]
, [dd 1; lit 2; dd 3]
)
; ( dec 5
, [ [ff (-1); tt 2]; [tt 3; pos 4]
; [ff (-5); neg 6]; [ff (-2); ff (-5); pos 6]
]
, [dd 1; lit 2; dd 3; dd 5]
)
; ( unit-prop 6
, [ [ff (-1); tt 2]; [tt 3; pos 4]
; [ff (-5); xx (-6)]; [ff (-2); ff (-5); tt 6]
]
, [dd 1; lit 2; dd 3; dd 5; xx 6]
)
; ( bt
, [ [ff (-1); tt 2]; [tt 3; pos 4]
; [tt (-5); neg 6]; [ff (-2); tt (-5); pos 6]
]
, [dd 1; lit 2; dd 3; lit (-5)]
)
];
>
>);
+frame-nofooter({Backtrack しまくる DPLL の動作例})(open DPLL in '<
+x-small<
+derive
[ [lit (-1); lit (-2); lit (-3); lit (-4); lit 5]
; [lit (-3); lit (-4); lit (-6)]
; [lit (-5); lit 6; lit (-1); lit 7]
; [lit (-7); lit 8]
; [lit (-2); lit (-7); lit 9]
; [lit (-8); lit (-9); lit 10]
; [lit (-10); lit 11]
; [lit (-11); lit 12]
; [lit (-10); lit (-2); lit (-12)]
]
[ (rule ${\Decide[1\text!{-}4]}
, [ [ff (-1); ff (-2); ff (-3); ff (-4); lit 5]
; [ff (-3); ff (-4); lit (-6)]
; [lit (-5); lit 6; ff (-1); lit 7]
; [lit (-7); lit 8]
; [ff (-2); lit (-7); lit 9]
; [lit (-8); lit (-9); lit 10]
; [lit (-10); lit 11]
; [lit (-11); lit 12]
; [lit (-10); ff (-2); lit (-12)]
]
, [somit; dd 4]
)
; (rule ${\UnitProp[5\text!{-}11]}
, [ [ff (-1); ff (-2); ff (-3); ff (-4); tt 5]
; [ff (-3); ff (-4); tt (-6)]
; [ff (-5); ff 6; ff (-1); tt 7]
; [ff (-7); tt 8]
; [ff (-2); ff (-7); tt 9]
; [ff (-8); ff (-9); tt 10]
; [ff (-10); tt 11]
; [ff (-11); lit 12]
; [ff (-10); ff (-2); lit (-12)]
]
, [somit; dd 4; somit; lit 11]
)
; ( unit-prop 12
, [ [ff (-1); ff (-2); ff (-3); ff (-4); tt 5]
; [ff (-3); ff (-4); tt (-6)]
; [ff (-5); ff 6; ff (-1); tt 7]
; [ff (-7); tt 8]
; [ff (-2); ff (-7); tt 9]
; [ff (-8); ff (-9); tt 10]
; [ff (-10); tt 11]
; [ff (-11); xx 12]
; [ff (-10); ff (-2); xx (-12)]
]
, [somit; dd 4; somit; lit 11; xx 12]
)
; (bt
, [ [ff (-1); ff (-2); ff (-3); tt (-4); lit 5]
; [ff (-3); tt (-4); lit (-6)]
; [lit (-5); lit 6; ff (-1); lit 7]
; [lit (-7); lit 8]
; [ff (-2); lit (-7); lit 9]
; [lit (-8); lit (-9); lit 10]
; [lit (-10); lit 11]
; [lit (-11); lit 12]
; [lit (-10); ff (-2); lit (-12)]
]
, [somit; lit (-4)]
)
; (rule ${\Decide[5\text!{-}7]}
, [ [ff (-1); ff (-2); ff (-3); tt (-4); tt 5]
; [ff (-3); tt (-4); ff (-6)]
; [ff (-5); tt 6; ff (-1); tt 7]
; [ff (-7); lit 8]
; [ff (-2); ff (-7); lit 9]
; [lit (-8); lit (-9); lit 10]
; [lit (-10); lit 11]
; [lit (-11); lit 12]
; [lit (-10); ff (-2); lit (-12)]
]
, [somit; lit (-4); somit; dd 7]
)
; (rule ${\UnitProp[8\text!{-}11]}
, [ [ff (-1); ff (-2); ff (-3); tt (-4); tt 5]
; [ff (-3); tt (-4); ff (-6)]
; [ff (-5); tt 6; ff (-1); tt 7]
; [ff (-7); tt 8]
; [ff (-2); ff (-7); tt 9]
; [ff (-8); ff (-9); tt 10]
; [ff (-10); tt 11]
; [ff (-11); xx 12]
; [ff (-10); ff (-2); xx (-12)]
]
, [somit; lit (-4); somit; lit 11]
)
; ( bt
, [ [ff (-1); ff (-2); ff (-3); tt (-4); tt 5]
; [ff (-3); tt (-4); ff (-6)]
; [ff (-5); tt 6; ff (-1); ff 7]
; [tt (-7); lit 8]
; [ff (-2); tt (-7); lit 9]
; [lit (-8); lit (-9); lit 10]
; [lit (-10); lit 11]
; [lit (-11); lit 12]
; [lit (-10); ff (-2); lit (-12)]
]
, [somit; lit (-4); somit; lit (-7)]
)
; ( rule ${\cdots}
, [ [ff (-1); ff (-2); ff (-3); tt (-4); tt 5]
; [ff (-3); tt (-4); ff (-6)]
; [ff (-5); tt 6; ff (-1); ff 7]
; [tt (-7); tt 8]
; [ff (-2); tt (-7); tt 9]
; [ff (-8); ff (-9); tt 10]
; [ff (-10); tt 11]
; [ff (-11); xx 12]
; [ff (-10); ff (-2); xx (-12)]
]
, [somit; lit (-4); somit; lit 11]
)
; ( bt
, [ [ff (-1); ff (-2); ff (-3); tt (-4); tt 5]
; [ff (-3); tt (-4); tt (-6)]
; [ff (-5); ff 6; ff (-1); lit 7]
; [lit (-7); lit 8]
; [ff (-2); lit (-7); lit 9]
; [lit (-8); lit (-9); lit 10]
; [lit (-10); lit 11]
; [lit (-11); lit 12]
; [lit (-10); ff (-2); lit (-12)]
]
, [somit; lit (-4); somit; lit (-6)]
)
; ( rule ${\cdots}
, [ [ff (-1); ff (-2); ff (-3); tt (-4); tt 5]
; [ff (-3); tt (-4); tt (-6)]
; [ff (-5); ff 6; ff (-1); tt 7]
; [ff (-7); tt 8]
; [ff (-2); ff (-7); tt 9]
; [ff (-8); ff (-9); tt 10]
; [ff (-10); tt 11]
; [ff (-11); xx 12]
; [ff (-10); ff (-2); xx (-12)]
]
, [somit; lit (-4); somit; lit 11]
)
; ( bt
, [ [ff (-1); ff (-2); ff (-3); tt (-4); ff 5]
; [ff (-3); tt (-4); lit (-6)]
; [tt (-5); lit 6; ff (-1); lit 7]
; [lit (-7); lit 8]
; [ff (-2); lit (-7); lit 9]
; [lit (-8); lit (-9); lit 10]
; [lit (-10); lit 11]
; [lit (-11); lit 12]
; [lit (-10); ff (-2); lit (-12)]
]
, [somit; lit (-4); somit; lit (-5)]
)
; ( rule ${\mathrm{Bt} \mathrel{\text!{ on }} 7,8,10,11}
, [ [ff (-1); ff (-2); ff (-3); tt (-4); ff 5]
; [ff (-3); tt (-4); lit (-6)]
; [tt (-5); lit 6; ff (-1); lit 7]
; [tt (-7); lit 8]
; [ff (-2); tt (-7); lit 9]
; [tt (-8); lit (-9); ff 10]
; [tt (-10); lit 11]
; [lit (-11); lit 12]
; [tt (-10); ff (-2); lit (-12)]
]
, [somit; lit (-5); lit (-7); lit (-8); lit (-10); lit (-11)]
)
];
>
>);
+frame{CDCL: Conflict-Driven Clause Learning}<
+itemize<
+item{単純総当たりよりDPLLは賢いが、Backtrack で得られる情報が少ない}<
+item{折角 Backtrack でいったん真偽値が確定しても、更に Backtrack すればその情報は消えてしまう}<>
>
+item{Backtrack は一段階ずつしか戻らない}<
+item{\emph{場合分けが入れ子}になっている場合、実は直近の場合分けより\emph{もっと早くに}矛盾が起きていても延々と\emph{一段階ずつ} Backtrack してしまう}<>
>
+item{矛盾からに過程を辿っていって矛盾の原因となった「理由」を見付け。\emph{学習節}としてCNFに追加してそこまで\emph{一気に巻き戻そう} (\emph{Backjump})！}<
+item{これが\emph{矛盾からの節学習}(Conflict-Driven Clause Learning, \emph{CDCL})}<>
>
>
>
+frame{CDCL: どういう学習節が望ましいか？}<
+itemize<
+item{学習節が\emph{元々の入力の帰結}であること}<
+item{任意のタイミングで Backjump が起き得る}<>
+item{いつでも使えるように、仮定が本質的には増えていてはならない}<>
>
+item{「\emph{すぐに使える}」学習節であること}<
+item{Backjump した直後に、\emph{新しい情報}が得られないと意味がない}<>
+item{特に、\emph{巻き戻した段階で単位節になっている}ようにしたい}<>
>
+item{なるべく\emph{小さい}ほうがよい}<
+item{単位節や矛盾が比較的すぐ出るようにしたい}<>
>
+item{\emph{含意グラフ}を考えるとこれらを満たす学習節を得られる}<>
>
>
+frame{CDCL：\emph{含意グラフ}}<
+itemize<
+item{これまでに\emph{真偽を割り当てたリテラルを頂点}として持つ有向グラフ}<>
+item{単位伝播で真になったリテラルへ、\emph{根拠となったリテラルから辺}を伸ばす}<
+item{単位伝播＝「他のリテラルが真にならなかったので最後の一つを真にする」}<>
+item{「根拠」：つまり、\emph{真偽を確定させた節}に含まれる\emph{他のリテラルの否定}}<>
+item{ただ一つのリテラルを持つ単位節のリテラルや、場合分けリテラルの場合入次数はゼロ}<>
>
+item{以下は最初の ${\cnf!(open DPLL in [[neg 1; pos 2]; [pos 3; pos 4]; [neg 5; neg 6]; [neg 2; neg 5; pos 6]])} に対する含意グラフの例}<>
>
+fig-on-right(
let prev ctx = ctx
|> fc Colors.black
|> tc Colors.white
in let contra ctx = ctx
|> fc Colors.red
|> tc Colors.white
in let cfg = (|default with
default-node-style = default-node-style |> circle |> padding 5pt;
unit-length = 1.25cm;
|)
in textbox-with-width 5cm {\x-small{
\tikzy?:(cfg)[
matrix
[ [node?:[prev] {${3}}; node?:[named`5`] {${5}}; node?:[contra; named`6`] {${6}}; ]
; [node?:[named `1`; prev] {${1}}; node?:[named `2`] {${2}}; node?:[named `-6`; contra] {${\widebar{6}}}]
]
; arrow (east-of `5`) (west-of `6`)
; arrow (east-of `1`) (west-of `2`)
; arrow (north-east-of `2`) (south-west-of `6`)
; arrow (east-of `2`) (west-of `-6`)
];
}}
)<
+itemize<
+item{黒丸はこれよりも前の場合分けで仮置きされたリテラル}<>
+item{赤丸は互いに矛盾したリテラル}<>
>
>
>
+frame{CDCL：含意グラフと学習節1 - カットと矛盾原因}<
+itemize<
+item{含意グラフを\emph{conflict side}と\emph{reason side}の二つの集合に\emph{カット}すると、矛盾への\emph{原因}が得られる}<
+item{直接矛盾した頂点は必ず\emph{conflict side}に入れる}<>
+item{現在の場合分けの起点以前のものは全て\emph{reason side}に入れる}<>
+item{それ以外のリテラルはどちらに割り当ててもいい}<>
>
+item{このとき、\emph{reason side}のリテラルはconflict side の\emph{原因}になっている}<
+item{特に\emph{conflict sideに向かう辺を持つreason sideの頂点}があれば十分}<>
>
>
+fig-center(
let prev ctx = ctx
|> fc Colors.black
|> tc Colors.white
in let contra ctx = ctx
|> fc Colors.red
|> tc Colors.white
in let cfg = (|default with
default-node-style = default-node-style |> circle |> padding 5pt;
unit-length = 2cm;
|)
in textbox {\x-small{
\tikzy?:(cfg)[
matrix
[ [ node?:[named `3`; prev] {${3}}
; node?:[named`5`] {${5}}
; node?:[contra; named`6`] {${6}};
]
; [ node?:[named `1`; prev] {${1}}
; node?:[named `2`] {${2}}
; node?:[named `-6`; contra] {${\widebar{6}}}
]
]
; arrow (east-of `5`) (west-of `6`)
; arrow (east-of `1`) (west-of `2`)
; arrow (north-east-of `2`) (south-west-of `6`)
; arrow (east-of `2`) (west-of `-6`)
; node-at?:[plain] (between (south-east-of `6`) (north-east-of `-6`))
{\xx-small{conflict side}}
; node-at?:[plain] (between (south-west-of `3`) (north-west-of `1`))
{\xx-small{reason side}}
; polyline
?:[ pc Colors.purple; lw 2pt ]
[ between (north-west-of `5`) (north-east-of `6`)
; between (south-east-of `1`) (south-west-of `2`)
]
];
}}
);
>
+frame-nofooter{Cutと学習節の例：多段Backtrackの例の序盤}<
+x-small< +eqn?:(AZMathEquation.notag)(${
\cnf!(open DPLL in
[ [ff (-1); ff (-2); ff (-3); ff (-4); tt 5]
; [ff (-3); ff (-4); tt (-6)]
; [ff (-5); ff 6; ff (-1); tt 7]
; [ff (-7); tt 8]
; [ff (-2); ff (-7); tt 9]
; [ff (-8); ff (-9); tt 10]
; [ff (-10); tt 11]
; [ff (-11); xx 12]
; [ff (-10); ff (-2); xx (-12)]
]
)
});>
+xx-small< +centering{
\tikzy?:(|
large-graph-cfg
with
default-node-style =
large-graph-cfg#default-node-style
|> padding 3pt
|> distance 4pt
; unit-length = 1cm
|)(
let cut = fun xs -> xs |> pc Colors.purple |> lw 2pt in
let cut-label = fun xs -> xs |> plain
|> tc Colors.purple
|> style [set-font-size 15pt] in
List.append
large-graph-nodes
[ % Cut 1
node-at?:[cut-label; named `cut1`; distance 0.5cm]
(proj (between (south-east-of `4`) (south-west-of `-6`))
(south-of `-6`, south-of `9`)
)
{Cut ${A}}
; spline?:[cut]
[ proj (between (north-of `2`) (north-of `10`)) (north-of `1`, north-of `2`)
; between (center-of `2`) (center-of `8`)
; between (center-of `1`) (center-of `5`)
; proj
(between (center-of `4`) (center-of `5`))
( between (center-of `2`) (center-of `8`)
, between (center-of `1`) (center-of `5`)
)
; between (center-of `4`) (center-of `5`)
; north-of `cut1`
]
% Cut #2
; node-at?:[cut-label; named `cut2`; distance 0.5cm]
(proj
(center-of `1`)
(south-of `-6`, south-of `9`)
)
{Cut ${B}}
; spline?:[cut]
[ proj (between (north-of `8`) (north-of `-12`)) (north-of `1`, north-of `2`)
; between (north-of `8`) (north-of `-12`)
; between (center-of `8`) (center-of `9`)
; north-of `cut2`
]
% Cut #3
; node-at?:[cut-label; named `cut3`; distance 0.5cm]
(between (south-of `9`) (south-of `11`)) {Cut ${C}}
; spline?:[cut]
[ proj (center-of `11`)
(north-of `1`, north-of `2`)
; between (center-of `10`) (center-of `-12`)
; north-of `cut3`
]
]
);
}>
+listing(open DPLL in {
* Cut A: ${\cnf![[lit (-1);lit (-2);lit (-3);lit (-4)]]} → ${3} の場合分け直後へ飛び、${\widebar{4}}が単位節伝播
* Cut B: ${\cnf![[lit (-2);lit (-7);lit (-8)]]} → ${2} の場合分け直後へ飛ぶが何もわからない
* Cut C: ${\cnf![[lit (-2);lit (-10)]]} → ${2} の場合分け直後へ飛び、${\widebar{10}}が単位節伝播
** 単位節になっているものとなっていないものの違いは何か？
});
>
+frame{単位節とUIP}<
+itemize(open DPLL in '<
+item{Cutに対応する学習節が\emph{単位節}になるのは、\emph{一意相互作用点}（Unique Interaction Point, \emph{UIP}）と呼ばれる頂点の直後でCutした時}<
+item{頂点${l}が\emph{UIP}である${\Longleftrightarrow}グラフから${l}を取り除くと、直近の決定リテラルから少なくとも一方の矛盾頂点へのパスが消える（「\emph{必ず通る点}」）}<>
>
+item{前の例では${4, 7, 10}が\emph{UIP}で、Cut ${A, C}が頂点${4, 10} の直後のCutに相当}<>
+item{「学習節が単位節になる」ためには UIP で切ればよい（逆もまた真）}<
+item{\emph{決定リテラル自身もUIP}なので、少なくとも一つUIPは存在する}<>
+item{\emph{矛盾に一番近いUIP}、\emph{1-UIP}のCutがよいことが経験的に知られている\cite[`Zhang:2001`];}<>
+item{前の例では、${\cnf![[lit (-2);lit (-10)]]}に対応する${10}で切ったCut ${C}が1-UIP}<>
+item{conflicting side が増えるほど必要な仮定も増えそうなので、直感的ではある}<>
>
>);
>
+frame{1-UIP学習節の生成と導出規則}<
+itemize<
+item{含意グラフは概念上でわかりやすいが、直接実装する必要はない}<
+item{矛盾節に\emph{導出}規則 (\emph{Resolution}) を単位節になるまで繰り返し適用すればよい}<>
>
>
+thm?:({導出規則})?:(false){
以下の導出規則は古典論理の派生規則：
\eqn?:(AZMathEquation.notag)(
${\frac{c \lor \Phi, \mquad \lnot c \lor \Psi}{\Phi \lor \Psi}}
);
}
+itemize<
+item{古典的に${c \lor \Phi}は${\lnot c \rightarrow \Phi}と、${\lnot c \lor \Psi}は${c \rightarrow \Psi}とそれぞれ同値}<>
+item{更に排中律があるので${c \lor \lnot c}が成り立つから、結局${\Phi \lor \Psi}が結論できる}<>
>
>
+frame?:(6){導出の繰り返しで1-UIP学習節を作る}<
+enumerate{
* 矛盾した二つの節の矛盾リテラルに導出規則を適用
* 単位節になるまで、仮学習節の中で「一番最後に真偽が確定した命題変数」を選び、その真偽を確定させた節と導出規則を適用
\listing{* 「単位節になる」＝最後の場合分け以後の命題変数が一つになる}
}
+listing{
* 学習節の導出の例：
}
+phantom(from 2)<
+fig-center(
hconcat
[ textbox {\xx-small{\tikzy?:(|
large-graph-cfg
with
default-node-style =
large-graph-cfg#default-node-style
|> padding 3pt
|> distance 4pt
; unit-length = 0.75cm
|)(
let overrider sty = sty
|> override-node-when (from 3) [`-12`; `12`]
[ fc Colors.white
; tc Colors.black
]
|> override-node-when (bw 3 4) [`2`; `10`; `11`]
[ fc Colors.yellow
; tc Colors.black
]
|> override-node-when (from 5) [`2`; `10`]
[ fc Colors.orange
; tc Colors.white
]
in overrider large-graph-nodes
);
}}
; gap 1cm
; textbox {
\small{
\tikzy?:
(| default with
default-node-style = default-node-style |> padding 2pt
; path-offset = -7.5mm
; unit-length = 6mm
|)(open DPLL in [
matrix
[ [node?:[named `-12`] {${\cnf![[lit (-2); lit (-10); lit (-12)]]}}]
; [ empty; empty; empty
; node?:[named `res-1`; phantom (until 2)] {${\cnf![[lit (-2); lit (-10); lit (-11)]]}}
; node?:[lc slydifi-cfg#color-bg; rect; fc slydifi-cfg#color-bg
; padding 2pt; named `stop`; distance 2.5mm] {\hskip(2cm);}
; node?:[named `res-2`; phantom (until 4)] {${\cnf![[lit (-2); lit (-10)]]}}
]
; [node?:[named `12`] {${\cnf![[lit (-11); lit 12]]}}]
]
; arrow?:[phantom (until 2)] (east-of `-12`) (north-west-of `res-1`)
; arrow?:[phantom (until 2)] (east-of `12`) (south-west-of `res-1`)
; arrow?:[phantom (until 3)] (east-of `res-1`) (west-of `res-2`)
; node-at?:[phantom (until 3)] (north-of `stop`)
{\x-small{${\cnf![[lit (-10); lit 11]]}}}
]);
}
}
]
);>
+phantom(from 6)<+listing{
* 根拠となる節で導出を繰り返す事が、「原因」を手繰っていく事に対応
}>
>
+frame-nofooter({同じ例の CDCL の動作})(open DPLL in '<
+centering {
長い例で学習節ありの Backjump がどう振る舞うか見てみよう
}
+xx-small<
+derive
[ [lit (-1); lit (-2); lit (-3); lit (-4); lit 5]
; [lit (-3); lit (-4); lit (-6)]
; [lit (-5); lit 6; lit (-1); lit 7]
; [lit (-7); lit 8]
; [lit (-2); lit (-7); lit 9]
; [lit (-8); lit (-9); lit 10]
; [lit (-10); lit 11]
; [lit (-11); lit 12]
; [lit (-10); lit (-2); lit (-12)]
]
[ ( rule ${\cdots}
, [ [ff (-1); ff (-2); ff (-3); ff (-4); tt 5]
; [ff (-3); ff (-4); tt (-6)]
; [ff (-5); ff 6; ff (-1); tt 7]
; [ff (-7); tt 8]
; [ff (-2); ff (-7); tt 9]
; [ff (-8); ff (-9); tt 10]
; [ff (-10); tt 11]
; [ff (-11); xx 12]
; [ff (-10); ff (-2); xx (-12)]
]
, [somit; dd 4; somit; lit 11; xx 12]
)
; (bj
, [ [ff (-1); ff (-2); lit (-3); lit (-4); lit 5]
; [lit (-3); lit (-4); lit (-6)]
; [lit (-5); lit 6; ff (-1); lit 7]
; [lit (-7); lit 8]
; [ff (-2); lit (-7); lit 9]
; [lit (-8); lit (-9); lit 10]
; [lit (-10); lit 11]
; [lit (-11); lit 12]
; [lit (-10); ff (-2); lit (-12)]
; [lit (-10); ff (-2)]
]
, [dd 1; dd 2]
)
; (unit-prop (-10)
, [ [ff (-1); ff (-2); lit (-3); lit (-4); lit 5]
; [lit (-3); lit (-4); lit (-6)]
; [lit (-5); lit 6; ff (-1); lit 7]
; [lit (-7); lit 8]
; [ff (-2); lit (-7); lit 9]
; [lit (-8); lit (-9); ff 10]
; [tt (-10); lit 11]
; [lit (-11); lit 12]
; [tt (-10); ff (-2); lit (-12)]
; [tt (-10); ff (-2)]
]
, [dd 1; dd 2; lit (-10)]
)
; (rule ${\Decide [3\text!{-}4]}
, [ [ff (-1); ff (-2); ff (-3); ff (-4); lit 5]
; [ff (-3); ff (-4); lit (-6)]
; [lit (-5); lit 6; ff (-1); lit 7]
; [lit (-7); lit 8]
; [ff (-2); lit (-7); lit 9]
; [lit (-8); lit (-9); ff 10]
; [tt (-10); lit 11]
; [lit (-11); lit 12]
; [tt (-10); ff (-2); lit (-12)]
; [tt (-10); ff (-2)]
]
, [lit (-10); somit; dd 4]
)
; (rule ${\UnitProp[5\text!{-}8]}
, [ [ff (-1); ff (-2); ff (-3); ff (-4); tt 5]
; [ff (-3); ff (-4); tt (-6)]