splr 0.19.0

A modern CDCL SAT solver in Rust
Documentation 
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

#import "@preview/lovelace:0.3.1": *
#set text(
  font: ((name: "New Computer Modern", covers: "latin-in-cjk"), "Hiragino Mincho Pro"),
  size: 11pt)
#let title = [Main search loop in Splr-0.19 (src/solver/search.rs)]

#pseudocode-list(booktabs: true, hooks: 0.2em, line-gap: 6pt, stroke: 0.3pt, title: strong[Main search loop in Splr-0.19 (src/solver/search.rs)])[
  + *Output:* satifiability of the given CNF
  + *begin*
    + *let* $s: "int" <- 8192$;
    + *let* *mut* $l: "Luby" <- "Luby"."new"()$;
    + *let* *mut* $i: "int" <- 0$;
    + *while* _there is an unassignd or unpropagated var_ *do*
      + `SelectDecisionVar`();
      + *if* `BCP`() $!=$ CONFLICT *then*
        + *continue*;
      + *if* _decision level_ $= 0$ *then*
        + *return* UNSAT;
      + `ConflictAnalysis`();
      + `BackTrack`();
      + $i <- i + 1$;
      + *if* $i = s$ *then*
        +  `SelectRephaseScheme`([WALK]);
      + *if* $i >= l."value" times s$ *then*
        + $i <- 0$;
        + $l$.`next`();
        + `Restart`();
        + `Reduce`();
        + `Vivify`();
        + `Eliminate`();
        + `SelectRephaseScheme`([FALSE, TRUE, RANDOM, BEST, POLARITY]);
        + `SelectVarActivityScheme`([LRB, VMTF]);
    + *return* SAT:
]

#pagebreak()

#pseudocode-list(booktabs: true, hooks: 0.2em, line-gap: 6pt, stroke: 0.3pt, title: strong[Search in Splr-0.18(?)])[
+ *Input*: CNF
+ *Output*: satisfiability of the given CNF
+ ``
+ *while* _there is an unassigned or unpropagated var_ *do*
  + *if* _there is no unpropagated var_ *then*
    + select a decision var and its phase
  + *if* `BCP()` == conflict *then*
    + *if* _decision level_ $=$ _root level_ *then*
      + *return* UNSAT
    + `ConflictAnalysis`()
    + `Backtrack`()
  + *if* _restart condition holds or the current stage ends_ *then*
    + `Restart`()
    + *if* _a new stage begins_ *then*
        + `Reduce`()
        + update restart conditions
        + *if* _a new cycle begins_ *then*
            + `Vivify`()
            + select var phases (rephase)
            + *if* _a new segment begins_ *then*
              + `Eliminate`()
              + rescale var activities
+ *return* SAT
]

#pagebreak()

#pseudocode-list(booktabs: true, hooks: 0.2em, line-gap: 6pt, stroke: 0.3pt, title: strong[Search in Splr-0.17])[
+ *Input*: CNF
+ *Output*: satisfiability of the given CNF
+ ``
+ While([_there is an unassigned or unpropagated var_],
  + If([_there is no unpropagated var_], kw3: none,
    + Line([select a decision var and its phase])
  + If([BCP() _returns an conflict_], kw3: none,
    + If([_decision level is root level_], kw3: none,
      + {Return[UNSAT]}
    + ConflictAnalysis[]
    + BackTrack[]
  + If([_restart condition holds or the current stage ends_], kw3: none,
    + Restart[]
    + If([_a new stage begins_], kw3: none,
      + Reduce[]
      + Line([update restart condition])
      + If([_a new cycle begins_], kw3: none,
        + Vivify[]
        + Line([select var phases])
        + If([_a new segment begins_], kw3: none,
          + Eliminate[]
          + Line([rescale var activities])
  + Return[SAT]
]