1package sat23import (4 "fmt"56 "mosaic-engine/rules"7 "mosaic-engine/third_party/gophersat/solver"8)910// Incremental is one hot solver for one shape, reused across many11// questions about different puzzles on it. The shape's rules are parsed12// once; a puzzle's givens are passed as assumptions (gophersat's Assume:13// level-1 bindings retracted by the next Assume), and known solutions are14// excluded by guarded blocking clauses: (sel_k or "differs from solution15// k"), activated by assuming not sel_k and switched off by assuming16// sel_k. Parsing the encoding was three quarters of every fresh solve;17// with a hot solver the clue-removal loop only pays for the search.18type Incremental struct {19 sh rules.Shape20 mask rules.Mask21 p *problem22 s *solver.Solver23 nSel int // selectors reserved in the encoding24 used int // selectors consumed by blocking clauses so far25 sel map[string]int // solution key -> selector var id26 // per call27 lits []solver.Lit28}2930const incrementalSelectors = 5123132// NewIncremental builds the hot solver for the shape under the mask.33func NewIncremental(sh rules.Shape, mask rules.Mask) *Incremental {34 inc := &Incremental{sh: sh, mask: mask, p: problemFor(sh, mask), nSel: incrementalSelectors}35 inc.rebuild()36 return inc37}3839// rebuild parses the encoding afresh (also used when the selectors are40// exhausted, dropping every blocking clause).41func (inc *Incremental) rebuild() {42 p := inc.p43 cs := make([]solver.PBConstr, 0, len(p.constrs)+inc.nSel)44 for _, c := range p.constrs {45 lits := append([]int(nil), c.Lits...)46 var weights []int47 if c.Weights != nil {48 weights = append([]int(nil), c.Weights...)49 }50 cs = append(cs, solver.PBConstr{Lits: lits, Weights: weights, AtLeast: c.AtLeast})51 }52 // register the selector variables: one clause over all of them plus53 // a spare (selector 0) that is always assumed true, so the clause54 // constrains nothing and the variables exist55 reg := make([]int, 0, inc.nSel+1)56 for k := 0; k <= inc.nSel; k++ {57 reg = append(reg, p.nbVars+1+k)58 }59 cs = append(cs, solver.PropClause(reg...))60 inc.s = solver.New(solver.ParsePBConstrs(cs))61 inc.used = 062 inc.sel = map[string]int{}63}6465func solKey(sol []rules.Cell) string {66 b := make([]byte, len(sol))67 for i, v := range sol {68 b[i] = byte('0' + v + 1) // Empty -> '0', 0 -> '1', 1 -> '2'69 }70 return string(b)71}7273// block adds a guarded blocking clause for a solution (over every cell of74// the shape) and returns its selector; rebuilds when the selectors are75// spent (the caller re-blocks what it still needs).76func (inc *Incremental) block(sol []rules.Cell) int {77 key := solKey(sol)78 if v, ok := inc.sel[key]; ok {79 return v80 }81 if inc.used >= inc.nSel {82 return -183 }84 inc.used++85 v := inc.p.nbVars + 1 + inc.used86 lits := make([]solver.Lit, 0, len(inc.p.cells)+1)87 lits = append(lits, solver.IntToLit(int32(v)))88 for _, i := range inc.p.cells {89 l := int32(i + 1)90 if sol[i] == 1 {91 l = -l92 }93 lits = append(lits, solver.IntToLit(l))94 }95 inc.s.AppendClause(solver.NewClause(lits))96 inc.sel[key] = v97 return v98}99100// assume binds the puzzle's givens and activates exactly the blocks of101// the given solutions (adding blocks as needed, rebuilding on exhaustion).102func (inc *Incremental) assume(cells []rules.Cell, blocked [][]rules.Cell) {103 for attempt := 0; attempt < 2; attempt++ {104 // clear every binding first: AppendClause simplifies a new clause105 // against the current bindings, and under the last puzzle's106 // assumptions a blocking clause can collapse to its selector alone107 // (a permanent unit that switches the block off for good)108 inc.s.Assume(nil)109 active := map[int]bool{}110 ok := true111 for _, sol := range blocked {112 v := inc.block(sol)113 if v < 0 {114 ok = false115 break116 }117 active[v] = true118 }119 if !ok {120 inc.rebuild()121 continue122 }123 inc.lits = inc.lits[:0]124 for _, i := range inc.p.cells {125 v := cells[i]126 if v == rules.Empty {127 continue128 }129 l := int32(i + 1)130 if v == 0 {131 l = -l132 }133 inc.lits = append(inc.lits, solver.IntToLit(l))134 }135 inc.lits = append(inc.lits, solver.IntToLit(int32(inc.p.nbVars+1))) // the spare136 for k := 1; k <= inc.used; k++ {137 v := int32(inc.p.nbVars + 1 + k)138 if active[int(v)] {139 v = -v140 }141 inc.lits = append(inc.lits, solver.IntToLit(v))142 }143 inc.s.Assume(inc.lits)144 return145 }146 panic(fmt.Sprintf("sat: %d blocks do not fit %d selectors", len(blocked), inc.nSel))147}148149// Extend finds solutions of the puzzle (givens in cells) that are not in150// known, appending to known until it holds limit solutions or none is151// left. exhausted is true when every solution of the puzzle is in the152// returned set. Every solution in known must be a solution of the puzzle.153func (inc *Incremental) Extend(cells []rules.Cell, known [][]rules.Cell, limit int) (out [][]rules.Cell, exhausted bool) {154 out = known155 for len(out) < limit {156 inc.assume(cells, out)157 if solve(inc.s) != solver.Sat {158 return out, true159 }160 sol := inc.p.model(inc.s, nil)161 out = append(out, sol)162 }163 return out, false164}165166// Count is Extend for callers that only need the number (up to limit).167func (inc *Incremental) Count(cells []rules.Cell, known [][]rules.Cell, limit int) (n int, exhausted bool) {168 out, ex := inc.Extend(cells, known, limit)169 return len(out), ex170}171172// Consistent keeps the known solutions that agree with the puzzle's173// givens (a puzzle with more givens has a subset of the solutions).174func Consistent(cells []rules.Cell, known [][]rules.Cell) [][]rules.Cell {175 var out [][]rules.Cell176 for _, s := range known {177 ok := true178 for i, v := range cells {179 if v != rules.Empty && s[i] != v {180 ok = false181 break182 }183 }184 if ok {185 out = append(out, s)186 }187 }188 return out189}