The idle G=200 scatter run sat 24 minutes at 100% CPU inside rules.CoupledSolutions: plain backtracking in tile-id order enumerates combinations of unconnected tiles before reaching a conflict and does not finish at ~450 tiles. sat.Coupled encodes one selector per (tile, solution), exactly one per tile, and a clause per incompatible pair on each overlap, counting with blocking clauses; gen and the assertion test use it. TestCoupledMatchesBacktracking cross-checks the counts.
- commit
- 349e2727edc5a52bf8110fec00342a8acfd55ceb
- parent
- ad5c952e941757ab4c0844a02a689ece013fb95a
- author
- dami <gazey55@gmail.com>
| M | engine/ | 2 | +- |
| M | engine/ | 2 | +- |
| A | engine/ | 97 | ++++++++++++++++++++++++++++++ |
| M | engine/ | 47 | +++++++++++++++ |
@@ -745,7 +745,7 @@ func generateAttempt(ctx context.Context, p Params, L *pack.Layout, attempt int)
745745 if !settled {746746 continue747747 }748- count, _ := rules.CoupledSolutions(shapes, sols, 2)748+ count, _ := sat.Coupled(shapes, sols, 2)749749 if count == 1 {750750 break751751 }@@ -233,7 +233,7 @@ func checkAssertions(t *testing.T, o *Output) {
233233 t.Fatalf("seam given %d listed by %d tiles, owned by %d", id, len(listed), len(owners[id]))234234 }235235 }236- count, _ := rules.CoupledSolutions(shapes, sols, 2)236+ count, _ := sat.Coupled(shapes, sols, 2)237237 if count != 1 {238238 t.Fatalf("mosaic has %d coupled solutions", count)239239 }@@ -0,0 +1,97 @@
1+package sat2+3+import (4+ "mosaic-engine/third_party/gophersat/solver"5+6+ "mosaic-engine/rules"7+)8+9+// Coupled counts (up to limit) the choices of one solution per shape such10+// that every pair of shapes agrees on every shared cell, and returns the11+// choices found (indexes into sols per shape). It answers the same12+// question as rules.CoupledSolutions, as SAT: one selector variable per13+// (shape, solution), exactly one selector true per shape, and for every14+// overlapping pair a clause forbidding each incompatible pair of15+// selectors; found models are blocked and the solver re-run. The plain16+// backtracking version enumerates combinations of unconnected tiles17+// before it reaches a conflict and does not finish at a few hundred18+// tiles; this is milliseconds.19+func Coupled(ws []rules.Shape, sols []rules.TileSolutions, limit int) (int, [][]int) {20+ masks := make([][]bool, len(ws))21+ for i, s := range ws {22+ masks[i] = s.Mask()23+ }24+ // selector ids25+ base := make([]int, len(ws)+1)26+ for t := range ws {27+ base[t+1] = base[t] + len(sols[t])28+ }29+ sel := func(t, i int) int { return base[t] + i + 1 }30+ var cs []solver.PBConstr31+ for t := range ws {32+ if len(sols[t]) == 0 {33+ return 0, nil34+ }35+ lits := make([]int, len(sols[t]))36+ for i := range lits {37+ lits[i] = sel(t, i)38+ }39+ cs = append(cs, solver.AtLeast(append([]int(nil), lits...), 1), solver.AtMost(append([]int(nil), lits...), 1))40+ }41+ for a := range ws {42+ for b := a + 1; b < len(ws); b++ {43+ wa, wb := ws[a], ws[b]44+ x0, x1 := max(wa.X0, wb.X0), min(wa.X0+wa.W, wb.X0+wb.W)45+ y0, y1 := max(wa.Y0, wb.Y0), min(wa.Y0+wa.H, wb.Y0+wb.H)46+ var cells [][2]int47+ for gy := y0; gy < y1; gy++ {48+ for gx := x0; gx < x1; gx++ {49+ la := (gy-wa.Y0)*wa.W + gx - wa.X050+ lb := (gy-wb.Y0)*wb.W + gx - wb.X051+ if masks[a][la] && masks[b][lb] {52+ cells = append(cells, [2]int{la, lb})53+ }54+ }55+ }56+ if len(cells) == 0 {57+ continue58+ }59+ for i, sa := range sols[a] {60+ for j, sb := range sols[b] {61+ ok := true62+ for _, c := range cells {63+ if sa[c[0]] != sb[c[1]] {64+ ok = false65+ break66+ }67+ }68+ if !ok {69+ cs = append(cs, solver.PropClause(-sel(a, i), -sel(b, j)))70+ }71+ }72+ }73+ }74+ }75+ var found [][]int76+ for len(found) < limit {77+ s := solver.New(solver.ParsePBConstrs(copyConstrs(cs)))78+ if solve(s) != solver.Sat {79+ break80+ }81+ m := s.Model()82+ choice := make([]int, len(ws))83+ block := make([]int, 0, len(ws))84+ for t := range ws {85+ for i := range sols[t] {86+ if m[sel(t, i)-1] {87+ choice[t] = i88+ block = append(block, -sel(t, i))89+ break90+ }91+ }92+ }93+ found = append(found, choice)94+ cs = append(cs, solver.PropClause(block...))95+ }96+ return len(found), found97+}@@ -302,3 +302,50 @@ func emptyShape(sh rules.Shape) []rules.Cell {
302302 }303303 return c304304 }305+306+// TestCoupledMatchesBacktracking: the SAT coupled count agrees with307+// rules.CoupledSolutions on small random fields of squares.308+func TestCoupledMatchesBacktracking(t *testing.T) {309+ rng := rand.New(rand.NewPCG(21, 21))310+ for trial := 0; trial < 6; trial++ {311+ X, n := 2+trial%2, 6312+ var ws []rules.Shape313+ for ty := 0; ty < X; ty++ {314+ for tx := 0; tx < X; tx++ {315+ ws = append(ws, rules.Square(tx*(n-1), ty*(n-1), n))316+ }317+ }318+ sols := make([]rules.TileSolutions, len(ws))319+ sq := rules.Square(0, 0, n)320+ for i := range ws {321+ k := 2 + rng.IntN(3)322+ for j := 0; j < k; j++ {323+ sol, _ := Complete(empty(sq), sq, rand.New(rand.NewPCG(uint64(trial*100+i*10+j), 1)))324+ sols[i] = append(sols[i], sol)325+ }326+ }327+ want, _ := rules.CoupledSolutions(ws, sols, 50)328+ got, found := Coupled(ws, sols, 50)329+ if got != want {330+ t.Fatalf("trial %d: sat %d vs backtracking %d", trial, got, want)331+ }332+ for _, choice := range found {333+ // every pair agrees on shared cells334+ for a := range ws {335+ for b := a + 1; b < len(ws); b++ {336+ for gy := 0; gy < X*(n-1)+1; gy++ {337+ for gx := 0; gx < X*(n-1)+1; gx++ {338+ if ws[a].Contains(gx, gy) && ws[b].Contains(gx, gy) {339+ va := sols[a][choice[a]][(gy-ws[a].Y0)*n+gx-ws[a].X0]340+ vb := sols[b][choice[b]][(gy-ws[b].Y0)*n+gx-ws[b].X0]341+ if va != vb {342+ t.Fatalf("trial %d: choice disagrees on (%d,%d)", trial, gx, gy)343+ }344+ }345+ }346+ }347+ }348+ }349+ }350+ }351+}