1package sat23import (4 "mosaic-engine/third_party/gophersat/solver"56 "mosaic-engine/rules"7)89// 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.19func 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}