sat.Incremental keeps one hot solver per tile: the shape's encoding is parsed once, a puzzle's givens are assumptions (gophersat's Assume) and known solutions are excluded by selector-guarded blocking clauses, so a count only searches beyond the solutions already known (adding a clue keeps a subset, removing one keeps all). Bindings are cleared before a blocking clause is appended, since AppendClause simplifies against the current bindings and would otherwise turn the block into a permanent selector unit. TestIncrementalMatchesEnumerate drives 360 puzzles on three shapes against fresh enumeration. Measurement, idle G=60 scatter seed a: 34.4 s -> 3.04 s wall (givens 33.3 s -> 2.7 s; SAT solves 108k -> 24k; heaviest tile 12.2 s -> 1.0 s). Output identical to the baseline; the 2x2 fixture still reproduces byte for byte, so gen.Version stays gen-v5.
- commit
- 10e678de9447b24e25d2265eb6f101a979b025cf
- parent
- 389b12137658cb53962f26fb8769c3f970cdfbe9
- author
- dami <gazey55@gmail.com>
| M | engine/ | 19 | ++- |
| M | engine/ | 7 | +- |
| A | engine/ | 189 | ++++++++++++++++++++++++++++++ |
| M | engine/ | 65 | ++++++++++ |
@@ -1370,13 +1370,24 @@ func (m *mosaic) removeClues(ctx context.Context, rng *rand.Rand, ti int, S [][]
13701370 gid := func(lx, ly int) int { return g.gid(m, ly*W+lx) }13711371 satCalls := 013721372 defer func() { m.addTimer(ti, func(t *TileTimer) { t.SatCalls += satCalls }) }()1373- countPT := func(puzzle []rules.Cell, sh rules.Shape, limit int) int {1373+ // one hot solver for this tile, and the solutions of the current1374+ // puzzle found so far: adding a clue keeps a subset of them, removing1375+ // one keeps all of them, so a count only ever has to look for1376+ // solutions beyond the known set (usually one solve, often none)1377+ inc := sat.NewIncremental(g.sh, rules.All)1378+ var known [][]rules.Cell1379+ countPT := func(puzzle []rules.Cell, _ rules.Shape, limit int) int {13741380 satCalls++1375- return countPT(puzzle, sh, limit)1381+ known = sat.Consistent(puzzle, known)1382+ known, _ = inc.Extend(puzzle, known, limit)1383+ return len(known)13761384 }1377- solutionsPT := func(puzzle []rules.Cell, sh rules.Shape, limit int) (rules.TileSolutions, bool) {1385+ solutionsPT := func(puzzle []rules.Cell, _ rules.Shape, limit int) (rules.TileSolutions, bool) {13781386 satCalls++1379- return solutionsPT(puzzle, sh, limit)1387+ known = sat.Consistent(puzzle, known)1388+ var ex bool1389+ known, ex = inc.Extend(puzzle, known, limit)1390+ return rules.TileSolutions(known), ex || len(known) >= limit13801391 }13811392 protect := map[int]bool{} // local indices never given: planted rectangles13821393 planted := r.R1 >= 0@@ -492,9 +492,14 @@ func TestReleaseClues(t *testing.T) {
492492 if _, still := m.seamOwner[id]; still {493493 t.Errorf("clue %d still owned after release", id)494494 }495- if len(tiles[owner].ownSeam) != before-1 {495+ if len(tiles[owner].ownSeam) >= before {496496 t.Errorf("owner %d still lists the clue", owner)497497 }498+ for _, v := range tiles[owner].ownSeam {499+ if v == id {500+ t.Errorf("owner %d still lists clue %d", owner, id)501+ }502+ }498503 found := false499504 for _, d := range dirty {500505 if d == owner {@@ -0,0 +1,189 @@
1+package sat2+3+import (4+ "fmt"5+6+ "mosaic-engine/rules"7+ "mosaic-engine/third_party/gophersat/solver"8+)9+10+// 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.18+type 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+}29+30+const incrementalSelectors = 51231+32+// NewIncremental builds the hot solver for the shape under the mask.33+func 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+}38+39+// rebuild parses the encoding afresh (also used when the selectors are40+// exhausted, dropping every blocking clause).41+func (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+}64+65+func 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+}72+73+// 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).76+func (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+}99+100+// assume binds the puzzle's givens and activates exactly the blocks of101+// the given solutions (adding blocks as needed, rebuilding on exhaustion).102+func (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+}148+149+// 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.153+func (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+}165+166+// Count is Extend for callers that only need the number (up to limit).167+func (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+}171+172+// Consistent keeps the known solutions that agree with the puzzle's173+// givens (a puzzle with more givens has a subset of the solutions).174+func 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+}@@ -237,3 +237,68 @@ func TestCompleteRegionKeepsNeighboursFeasible(t *testing.T) {
237237 t.Fatal("same seed, different joint completion")238238 }239239 }240+241+// TestIncrementalMatchesEnumerate drives one hot solver through many242+// puzzles on one shape (random givens, clues added and removed, wrong243+// values) and checks its solution sets against fresh enumeration.244+func TestIncrementalMatchesEnumerate(t *testing.T) {245+ for _, sh := range []rules.Shape{rules.Square(0, 0, 8), rules.Square(0, 0, 12), {W: 12, H: 12, Rects: [][4]int{{0, 0, 12, 6}, {2, 0, 8, 12}}}} {246+ if err := sh.Valid(); err != nil {247+ t.Fatal(err)248+ }249+ rng := rand.New(rand.NewPCG(21, uint64(sh.W)))250+ sol, _ := Complete(emptyShape(sh), sh, rng)251+ inc := NewIncremental(sh, rules.All)252+ puzzle := append([]rules.Cell(nil), sol...)253+ var known [][]rules.Cell254+ checks := 0255+ for step := 0; step < 120; step++ {256+ // mutate: remove a given, add one back, or flip one to a wrong value257+ cells := []int{}258+ for i, ok := range sh.Mask() {259+ if ok {260+ cells = append(cells, i)261+ }262+ }263+ i := cells[rng.IntN(len(cells))]264+ switch r := rng.Float64(); {265+ case r < 0.6:266+ puzzle[i] = rules.Empty267+ case r < 0.95:268+ puzzle[i] = sol[i]269+ default:270+ puzzle[i] = 1 - sol[i]271+ }272+ known = Consistent(puzzle, known)273+ var ex bool274+ known, ex = inc.Extend(puzzle, known, 5)275+ want, wex := Enumerate(puzzle, sh, rules.All, 5)276+ if len(known) != len(want) || ex != wex {277+ t.Fatalf("%dx%d step %d: incremental %d (exhausted %v) vs enumerate %d (%v)", sh.W, sh.H, step, len(known), ex, len(want), wex)278+ }279+ seen := map[string]bool{}280+ for _, s := range want {281+ seen[solKey(s)] = true282+ }283+ for _, s := range known {284+ if !seen[solKey(s)] {285+ t.Fatalf("%dx%d step %d: incremental returned a non-solution", sh.W, sh.H, step)286+ }287+ }288+ if puzzle[i] == 1-sol[i] {289+ puzzle[i] = rules.Empty // undo the wrong value290+ known = Consistent(puzzle, known)291+ }292+ checks++293+ }294+ t.Logf("%dx%d: %d puzzles agree; selectors used %d", sh.W, sh.H, checks, inc.used)295+ }296+}297+298+func emptyShape(sh rules.Shape) []rules.Cell {299+ c := make([]rules.Cell, sh.W*sh.H)300+ for i := range c {301+ c[i] = rules.Empty302+ }303+ return c304+}