|
| 1 | +package solver |
| 2 | + |
| 3 | +import ( |
| 4 | + "context" |
| 5 | + |
| 6 | + "github.com/irifrance/gini/inter" |
| 7 | + "github.com/irifrance/gini/z" |
| 8 | +) |
| 9 | + |
| 10 | +type choice struct { |
| 11 | + prev, next *choice |
| 12 | + index int // index of next unguessed literal |
| 13 | + candidates []z.Lit |
| 14 | +} |
| 15 | + |
| 16 | +type guess struct { |
| 17 | + m z.Lit // if z.LitNull, this choice was satisfied by a previous assumption |
| 18 | + index int // index of guessed literal in candidates |
| 19 | + children int // number of choices introduced by making this guess |
| 20 | + candidates []z.Lit |
| 21 | +} |
| 22 | + |
| 23 | +type search struct { |
| 24 | + s inter.S |
| 25 | + lits *litMapping |
| 26 | + assumptions map[z.Lit]struct{} // set of assumed lits - duplicates guess stack - for fast lookup |
| 27 | + guesses []guess // stack of assumed guesses |
| 28 | + headChoice, tailChoice *choice // deque of unmade choices |
| 29 | + heap []choice |
| 30 | + position int |
| 31 | + tracer Tracer |
| 32 | + result int |
| 33 | + buffer []z.Lit |
| 34 | +} |
| 35 | + |
| 36 | +func (h *search) PushGuess() { |
| 37 | + c := h.PopChoiceFront() |
| 38 | + g := guess{ |
| 39 | + m: z.LitNull, |
| 40 | + index: c.index, |
| 41 | + candidates: c.candidates, |
| 42 | + } |
| 43 | + if g.index < len(g.candidates) { |
| 44 | + g.m = g.candidates[g.index] |
| 45 | + } |
| 46 | + |
| 47 | + // Check whether or not this choice can be satisfied by an |
| 48 | + // existing assumption. |
| 49 | + for _, m := range g.candidates { |
| 50 | + if _, ok := h.assumptions[m]; ok { |
| 51 | + g.m = z.LitNull |
| 52 | + break |
| 53 | + } |
| 54 | + } |
| 55 | + |
| 56 | + h.guesses = append(h.guesses, g) |
| 57 | + if g.m == z.LitNull { |
| 58 | + return |
| 59 | + } |
| 60 | + |
| 61 | + installable := h.lits.InstallableOf(g.m) |
| 62 | + for _, constraint := range installable.Constraints() { |
| 63 | + var ms []z.Lit |
| 64 | + for _, dependency := range constraint.order() { |
| 65 | + ms = append(ms, h.lits.LitOf(dependency)) |
| 66 | + } |
| 67 | + if len(ms) > 0 { |
| 68 | + h.guesses[len(h.guesses)-1].children++ |
| 69 | + h.PushChoiceBack(choice{candidates: ms}) |
| 70 | + } |
| 71 | + } |
| 72 | + |
| 73 | + if h.assumptions == nil { |
| 74 | + h.assumptions = make(map[z.Lit]struct{}) |
| 75 | + } |
| 76 | + h.assumptions[g.m] = struct{}{} |
| 77 | + h.s.Assume(g.m) |
| 78 | + h.result, h.buffer = h.s.Test(h.buffer) |
| 79 | +} |
| 80 | + |
| 81 | +func (h *search) PopGuess() { |
| 82 | + g := h.guesses[len(h.guesses)-1] |
| 83 | + h.guesses = h.guesses[:len(h.guesses)-1] |
| 84 | + if g.m != z.LitNull { |
| 85 | + delete(h.assumptions, g.m) |
| 86 | + h.result = h.s.Untest() |
| 87 | + } |
| 88 | + for g.children > 0 { |
| 89 | + g.children-- |
| 90 | + h.PopChoiceBack() |
| 91 | + } |
| 92 | + c := choice{ |
| 93 | + index: g.index, |
| 94 | + candidates: g.candidates, |
| 95 | + } |
| 96 | + if g.m != z.LitNull { |
| 97 | + c.index++ |
| 98 | + } |
| 99 | + h.PushChoiceFront(c) |
| 100 | +} |
| 101 | + |
| 102 | +func (h *search) PushChoiceFront(c choice) { |
| 103 | + if h.headChoice == nil { |
| 104 | + h.headChoice = &c |
| 105 | + h.tailChoice = &c |
| 106 | + return |
| 107 | + } |
| 108 | + h.headChoice.prev = &c |
| 109 | + c.next = h.headChoice |
| 110 | + h.headChoice = &c |
| 111 | +} |
| 112 | + |
| 113 | +func (h *search) PopChoiceFront() choice { |
| 114 | + c := h.headChoice |
| 115 | + if c.next != nil { |
| 116 | + c.next.prev = nil |
| 117 | + } else { |
| 118 | + h.tailChoice = nil |
| 119 | + } |
| 120 | + h.headChoice = c.next |
| 121 | + return *c |
| 122 | + |
| 123 | +} |
| 124 | +func (h *search) PushChoiceBack(c choice) { |
| 125 | + if h.tailChoice == nil { |
| 126 | + h.headChoice = &c |
| 127 | + h.tailChoice = &c |
| 128 | + return |
| 129 | + } |
| 130 | + h.tailChoice.next = &c |
| 131 | + c.prev = h.tailChoice |
| 132 | + h.tailChoice = &c |
| 133 | +} |
| 134 | + |
| 135 | +func (h *search) PopChoiceBack() choice { |
| 136 | + c := h.tailChoice |
| 137 | + if c.prev != nil { |
| 138 | + c.prev.next = nil |
| 139 | + } else { |
| 140 | + h.headChoice = nil |
| 141 | + } |
| 142 | + h.tailChoice = c.prev |
| 143 | + return *c |
| 144 | +} |
| 145 | + |
| 146 | +func (h *search) Result() int { |
| 147 | + return h.result |
| 148 | +} |
| 149 | + |
| 150 | +func (h *search) Lits() []z.Lit { |
| 151 | + result := make([]z.Lit, 0, len(h.guesses)) |
| 152 | + for _, g := range h.guesses { |
| 153 | + if g.m != z.LitNull { |
| 154 | + result = append(result, g.m) |
| 155 | + } |
| 156 | + } |
| 157 | + return result |
| 158 | +} |
| 159 | + |
| 160 | +func (h *search) Do(ctx context.Context, anchors []z.Lit) (int, []z.Lit, map[z.Lit]struct{}) { |
| 161 | + for _, m := range anchors { |
| 162 | + h.PushChoiceBack(choice{candidates: []z.Lit{m}}) |
| 163 | + } |
| 164 | + |
| 165 | + for { |
| 166 | + // Need to have a definitive result once all choices |
| 167 | + // have been made to decide whether to end or |
| 168 | + // backtrack. |
| 169 | + if h.headChoice == nil && h.result == unknown { |
| 170 | + h.result = h.s.Solve() |
| 171 | + } |
| 172 | + |
| 173 | + // Backtrack if possible, otherwise end. |
| 174 | + if h.result == unsatisfiable { |
| 175 | + h.tracer.Trace(h) |
| 176 | + if len(h.guesses) == 0 { |
| 177 | + break |
| 178 | + } |
| 179 | + h.PopGuess() |
| 180 | + continue |
| 181 | + } |
| 182 | + |
| 183 | + // Satisfiable and no decisions left! |
| 184 | + if h.headChoice == nil { |
| 185 | + break |
| 186 | + } |
| 187 | + |
| 188 | + // Possibly SAT, keep guessing. |
| 189 | + h.PushGuess() |
| 190 | + } |
| 191 | + |
| 192 | + lits := h.Lits() |
| 193 | + set := make(map[z.Lit]struct{}, len(lits)) |
| 194 | + for _, m := range lits { |
| 195 | + set[m] = struct{}{} |
| 196 | + } |
| 197 | + result := h.Result() |
| 198 | + |
| 199 | + // Go back to the initial test scope. |
| 200 | + for len(h.guesses) > 0 { |
| 201 | + h.PopGuess() |
| 202 | + } |
| 203 | + |
| 204 | + return result, lits, set |
| 205 | +} |
| 206 | + |
| 207 | +func (h *search) Installables() []Installable { |
| 208 | + result := make([]Installable, 0, len(h.guesses)) |
| 209 | + for _, g := range h.guesses { |
| 210 | + if g.m != z.LitNull { |
| 211 | + result = append(result, h.lits.InstallableOf(g.candidates[g.index])) |
| 212 | + } |
| 213 | + } |
| 214 | + return result |
| 215 | +} |
| 216 | + |
| 217 | +func (h *search) Conflicts() []AppliedConstraint { |
| 218 | + return h.lits.Conflicts(h.s) |
| 219 | +} |
0 commit comments