1package sat23import (4 "math/rand/v2"5 "testing"6 "time"78 "mosaic-engine/rules"9)1011func empty(sh rules.Shape) []rules.Cell {12 c := make([]rules.Cell, sh.W*sh.H)13 for i := range c {14 c[i] = rules.Empty15 }16 return c17}1819func sq(n int) rules.Shape { return rules.Square(0, 0, n) }2021// tee is an 8-wide, 6-tall crossbar over a 4x2 stem (56 cells; valid22// under the pigeonhole bound)23func tee() rules.Shape {24 return rules.Shape{W: 8, H: 8, Rects: [][4]int{{0, 0, 8, 6}, {2, 6, 4, 2}}}25}2627func TestCompleteValidAndVaried(t *testing.T) {28 shapes := []rules.Shape{sq(6), sq(8), sq(10), sq(12), sq(14), sq(16), tee(),29 {W: 12, H: 8, Rects: [][4]int{{0, 0, 12, 8}}},30 {W: 12, H: 12, Rects: [][4]int{{0, 0, 12, 6}, {0, 0, 6, 12}}}, // L31 }32 for si, sh := range shapes {33 a, ok := Complete(empty(sh), sh, rand.New(rand.NewPCG(1, uint64(si))))34 if !ok {35 t.Fatalf("shape %d: no completion", si)36 }37 if err := rules.Single(sh, a).Validate(rules.All); err != nil {38 t.Fatalf("shape %d: completion invalid: %v", si, err)39 }40 for i, ok := range sh.Mask() {41 if ok != (a[i] != rules.Empty) {42 t.Fatalf("shape %d: cell %d filled=%v in shape=%v", si, i, a[i] != rules.Empty, ok)43 }44 }45 b, _ := Complete(empty(sh), sh, rand.New(rand.NewPCG(2, uint64(si))))46 if len(rules.Diff(a, b)) == 0 {47 t.Errorf("shape %d: two draws gave the same completion", si)48 }49 }50}5152func TestCompleteKeepsFixedCells(t *testing.T) {53 sh := sq(16)54 n := 1655 full, _ := Complete(empty(sh), sh, rand.New(rand.NewPCG(3, 3)))56 // all four sides fixed, interior blank: the case MRV backtracking spent57 // its whole timeout on58 cells := empty(sh)59 for k := 0; k < n; k++ {60 cells[k] = full[k]61 cells[(n-1)*n+k] = full[(n-1)*n+k]62 cells[k*n] = full[k*n]63 cells[k*n+n-1] = full[k*n+n-1]64 }65 start := time.Now()66 sol, ok := Complete(cells, sh, rand.New(rand.NewPCG(4, 4)))67 d := time.Since(start)68 if !ok {69 t.Fatal("four fixed sides: no completion")70 }71 for i, v := range cells {72 if v != rules.Empty && sol[i] != v {73 t.Fatalf("cell %d changed", i)74 }75 }76 if err := rules.Single(sh, sol).Validate(rules.All); err != nil {77 t.Fatal(err)78 }79 t.Logf("n=16 four sides fixed: completed in %s", d)80 if d > 2*time.Second {81 t.Errorf("too slow: %s", d)82 }83}8485func TestFeasibleRefutes(t *testing.T) {86 sh := sq(6)87 cells := empty(sh)88 cells[0], cells[6], cells[12] = 0, 0, 0 // three 0s down column 089 if Feasible(cells, sh, rules.All) {90 t.Fatal("a run of three should be infeasible")91 }92 cells[12] = 193 if !Feasible(cells, sh, rules.All) {94 t.Fatal("0,0,1 down column 0 should be feasible")95 }96 // on a T: three 0s along the stem's 4-row97 th := tee()98 c := empty(th)99 c[6*8+2], c[6*8+3], c[6*8+4] = 0, 0, 0100 if Feasible(c, th, rules.All) {101 t.Fatal("a run of three on a 4-line should be infeasible")102 }103}104105func TestEnumerateMatchesRulesSolver(t *testing.T) {106 rng := rand.New(rand.NewPCG(5, 5))107 for _, sh := range []rules.Shape{sq(6), sq(8), tee()} {108 for trial := 0; trial < 5; trial++ {109 full, _ := Complete(empty(sh), sh, rng)110 puzzle := append([]rules.Cell(nil), full...)111 for i := range puzzle {112 if puzzle[i] != rules.Empty && rng.Float64() < 0.6 {113 puzzle[i] = rules.Empty114 }115 }116 for _, mask := range []rules.Mask{rules.All, rules.Run | rules.Balance} {117 want, exhausted := rules.Single(sh, append([]rules.Cell(nil), puzzle...)).SolutionsBudget(mask, 12, rules.DefaultBudget)118 if !exhausted {119 continue120 }121 got, ex := Enumerate(puzzle, sh, mask, 12)122 if len(got) != len(want) || ex != (len(want) < 12) {123 t.Fatalf("%dx%d mask=%v: sat %d (exhausted %v) vs rules %d", sh.W, sh.H, mask.Names(), len(got), ex, len(want))124 }125 for _, s := range got {126 if err := rules.Single(sh, append([]rules.Cell(nil), s...)).Validate(mask); err != nil {127 t.Fatal(err)128 }129 for i, v := range puzzle {130 if v != rules.Empty && s[i] != v {131 t.Fatal("enumerated solution changed a given")132 }133 }134 }135 }136 }137 }138}139140func TestCountTiming(t *testing.T) {141 // a 14x14 at ~72% blank with all rules: the removal loop's inner call142 sh := sq(14)143 rng := rand.New(rand.NewPCG(6, 6))144 full, _ := Complete(empty(sh), sh, rng)145 puzzle := append([]rules.Cell(nil), full...)146 for i := range puzzle {147 if rng.Float64() < 0.72 {148 puzzle[i] = rules.Empty149 }150 }151 start := time.Now()152 c, ex := Count(puzzle, sh, rules.All, 4)153 t.Logf("n=14 72%% blank: count(limit 4) = %d exhausted=%v in %s", c, ex, time.Since(start))154}155156func TestDeterministicAndRaceFree(t *testing.T) {157 sh := sq(12)158 a, _ := Complete(empty(sh), sh, rand.New(rand.NewPCG(9, 9)))159 b, _ := Complete(empty(sh), sh, rand.New(rand.NewPCG(9, 9)))160 if len(rules.Diff(a, b)) != 0 {161 t.Fatal("same rng seed gave different completions")162 }163 puzzle := append([]rules.Cell(nil), a...)164 for i := range puzzle {165 if i%3 != 0 {166 puzzle[i] = rules.Empty167 }168 }169 want, _ := Enumerate(puzzle, sh, rules.All, 6)170 done := make(chan bool, 16)171 for k := 0; k < 16; k++ {172 go func() {173 got, _ := Enumerate(puzzle, sh, rules.All, 6)174 ok := len(got) == len(want)175 for i := range got {176 if ok && len(rules.Diff(got[i], want[i])) != 0 {177 ok = false178 }179 }180 done <- ok181 }()182 }183 for k := 0; k < 16; k++ {184 if !<-done {185 t.Fatal("concurrent enumeration differed")186 }187 }188}189190func TestCompleteRegionKeepsNeighboursFeasible(t *testing.T) {191 // a field with a 14-square, a T and a 12x6 rectangle overlapping it by192 // rectangles; complete the square jointly with the others, then each193 // neighbour must still be completable and fixed cells must be kept194 G := 30195 grid := make([]rules.Cell, G*G)196 for i := range grid {197 grid[i] = rules.Empty198 }199 target := rules.Square(2, 2, 14)200 th := tee()201 th.X0, th.Y0 = 12, 10 // crossbar overlaps the square's right part202 rect := rules.Shape{X0: 0, Y0: 14, W: 12, H: 8, Rects: [][4]int{{0, 0, 12, 8}}}203 others := []rules.Shape{th, rect}204 // fix the rectangle fully so the shared cells are constrained from205 // the other side206 far, _ := Complete(empty(rect), rect, rand.New(rand.NewPCG(11, 11)))207 for i, v := range far {208 if v != rules.Empty {209 grid[(rect.Y0+i/rect.W)*G+rect.X0+i%rect.W] = v210 }211 }212 for seed := uint64(1); seed <= 5; seed++ {213 sol, ok := CompleteRegion(grid, G, others, target, rand.New(rand.NewPCG(seed, seed)))214 if !ok {215 t.Fatalf("seed %d: no joint completion", seed)216 }217 if err := rules.Single(target, sol).Validate(rules.All); err != nil {218 t.Fatalf("seed %d: %v", seed, err)219 }220 trial := append([]rules.Cell(nil), grid...)221 for i, v := range sol {222 gid := (target.Y0+i/target.W)*G + target.X0 + i%target.W223 if grid[gid] != rules.Empty && grid[gid] != v {224 t.Fatalf("seed %d: fixed cell %d changed", seed, gid)225 }226 trial[gid] = v227 }228 for _, w := range others {229 if !Feasible(w.Local(trial, G), w, rules.All) {230 t.Fatalf("seed %d: neighbour at (%d,%d) left infeasible", seed, w.X0, w.Y0)231 }232 }233 }234 a, _ := CompleteRegion(grid, G, others, target, rand.New(rand.NewPCG(1, 1)))235 b, _ := CompleteRegion(grid, G, others, target, rand.New(rand.NewPCG(1, 1)))236 if len(rules.Diff(a, b)) != 0 {237 t.Fatal("same seed, different joint completion")238 }239}240241// 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.244func 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}297298func 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}305306// TestCoupledMatchesBacktracking: the SAT coupled count agrees with307// rules.CoupledSolutions on small random fields of squares.308func 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}352353// TestCompleteAll: a 2x2 grid of squares completed jointly is a valid354// coupled board, deterministic per rng, and refuses an impossible context.355func TestCompleteAll(t *testing.T) {356 G := 27357 board := make([]rules.Cell, G*G)358 for i := range board {359 board[i] = rules.Empty360 }361 ws := []rules.Shape{rules.Square(0, 0, 14), rules.Square(13, 0, 14), rules.Square(0, 13, 14), rules.Square(13, 13, 14)}362 a, ok := CompleteAll(board, G, ws, rand.New(rand.NewPCG(31, 31)))363 if !ok {364 t.Fatal("no joint completion")365 }366 full := append([]rules.Cell(nil), board...)367 for id, v := range a {368 full[id] = v369 }370 b := &rules.Board{W: G, H: G, Cells: full, Shapes: ws}371 if err := b.Validate(rules.All); err != nil {372 t.Fatal(err)373 }374 if !b.Complete() {375 t.Fatal("not complete")376 }377 a2, _ := CompleteAll(board, G, ws, rand.New(rand.NewPCG(31, 31)))378 for id, v := range a {379 if a2[id] != v {380 t.Fatal("not deterministic")381 }382 }383 // three equal cells down a column of the first square: impossible384 board[0], board[G], board[2*G] = 0, 0, 0385 if _, ok := CompleteAll(board, G, ws, rand.New(rand.NewPCG(31, 31))); ok {386 t.Fatal("completed an impossible context")387 }388}