rules: a Board is a grid plus shapes (rect unions); every maximal run of a shape's cells is a line; run/balance/unique per line; propagation with rule attribution, technique ladder, flip rectangles on shared lines, coupled CSP over shared cells, Shape.Valid with the distinct-lines bound. sat: gophersat encoding per line (cardinality for balance, XOR aux for uniqueness); Feasible/Complete/Enumerate/Count and CompleteRegion (joint completion over neighbouring shapes); Solve serialised because gophersat keeps a package-level buffer.
- commit
- acb987513cacad71971a4945b8c0ade7f844d25a
- parent
- a65f9ff488501777c8a7f3530c603c40149ba0e5
- author
- dami <gazey55@gmail.com>
| A | engine/ | 7 | + |
| A | engine/ | 2 | + |
| A | engine/ | 957 | ++++++++++++++++++++++++++++++ |
| A | engine/ | 382 | ++++++++++++ |
| A | engine/ | 432 | ++++++++++++++ |
| A | engine/ | 239 | +++++++ |
@@ -0,0 +1,957 @@
1+// Package rules is the only place Takuzu rules exist. A Board is a global2+// grid plus a set of shapes; every shape is a Takuzu on its own, played on3+// its lines: each maximal horizontal or vertical run of the shape's cells.4+// A cell in two shapes is constrained by both; that is the only rule that5+// crosses a shape. Nothing here knows about games, tiles as a concept6+// beyond "shape", or the solution.7+package rules8+9+import (10+ "fmt"11+ "sort"12+ "sync"13+)14+15+// Cell is 0, 1, or Empty.16+type Cell int817+18+const Empty Cell = -119+20+// Mask selects which rules are active.21+type Mask uint822+23+const (24+ Run Mask = 1 << iota // no three equal in a row along a line25+ Balance // each line has len/2 of each value26+ Unique // no two equal lines of one orientation and length in a shape27+ All = Run | Balance | Unique28+)29+30+var maskNames = []struct {31+ m Mask32+ name string33+}{{Run, "run"}, {Balance, "balance"}, {Unique, "unique"}}34+35+// Names lists the active rule names in a mask, in a fixed order.36+func (m Mask) Names() []string {37+ out := []string{}38+ for _, mn := range maskNames {39+ if m&mn.m != 0 {40+ out = append(out, mn.name)41+ }42+ }43+ return out44+}45+46+// Shape is a tile: a union of axis-aligned rectangles (local coordinates47+// inside a W x H bounding box) placed at (X0, Y0) on the board. Every48+// maximal horizontal and vertical run of its cells is a line; the rules49+// apply per line. A square n x n is Square(x0, y0, n).50+type Shape struct {51+ X0, Y0, W, H int52+ Rects [][4]int // local [lx, ly, rw, rh]53+}54+55+func Square(x0, y0, n int) Shape {56+ return Shape{X0: x0, Y0: y0, W: n, H: n, Rects: [][4]int{{0, 0, n, n}}}57+}58+59+// Mask returns the local W*H membership of the shape's cells.60+func (s Shape) Mask() []bool {61+ m := make([]bool, s.W*s.H)62+ for _, r := range s.Rects {63+ for y := r[1]; y < r[1]+r[3]; y++ {64+ for x := r[0]; x < r[0]+r[2]; x++ {65+ if x >= 0 && y >= 0 && x < s.W && y < s.H {66+ m[y*s.W+x] = true67+ }68+ }69+ }70+ }71+ return m72+}73+74+// Cells counts the shape's cells.75+func (s Shape) Cells() int {76+ n := 077+ for _, b := range s.Mask() {78+ if b {79+ n++80+ }81+ }82+ return n83+}84+85+// Contains reports whether the global cell (gx, gy) is in the shape.86+func (s Shape) Contains(gx, gy int) bool {87+ lx, ly := gx-s.X0, gy-s.Y088+ if lx < 0 || ly < 0 || lx >= s.W || ly >= s.H {89+ return false90+ }91+ for _, r := range s.Rects {92+ if lx >= r[0] && lx < r[0]+r[2] && ly >= r[1] && ly < r[1]+r[3] {93+ return true94+ }95+ }96+ return false97+}98+99+// Lines lists the shape's lines as local indexes (ly*W+lx), horizontal runs100+// first (top to bottom, left to right), then vertical runs.101+func (s Shape) Lines() [][]int {102+ m := s.Mask()103+ var out [][]int104+ for y := 0; y < s.H; y++ {105+ var run []int106+ for x := 0; x <= s.W; x++ {107+ if x < s.W && m[y*s.W+x] {108+ run = append(run, y*s.W+x)109+ continue110+ }111+ if len(run) > 0 {112+ out = append(out, run)113+ run = nil114+ }115+ }116+ }117+ for x := 0; x < s.W; x++ {118+ var run []int119+ for y := 0; y <= s.H; y++ {120+ if y < s.H && m[y*s.W+x] {121+ run = append(run, y*s.W+x)122+ continue123+ }124+ if len(run) > 0 {125+ out = append(out, run)126+ run = nil127+ }128+ }129+ }130+ return out131+}132+133+// Valid reports whether the shape can carry the rules: every line has an134+// even length of at least 4 (balance needs even; a line of two is a coin),135+// the cells are 4-connected, and the bounding box is tight.136+func (s Shape) Valid() error {137+ if s.W <= 0 || s.H <= 0 || len(s.Rects) == 0 {138+ return fmt.Errorf("empty shape")139+ }140+ m := s.Mask()141+ rowUsed := make([]bool, s.H)142+ colUsed := make([]bool, s.W)143+ first := -1144+ for i, b := range m {145+ if b {146+ rowUsed[i/s.W] = true147+ colUsed[i%s.W] = true148+ if first < 0 {149+ first = i150+ }151+ }152+ }153+ if first < 0 {154+ return fmt.Errorf("empty shape")155+ }156+ for y, u := range rowUsed {157+ if !u {158+ return fmt.Errorf("row %d of the bounding box is unused", y)159+ }160+ }161+ for x, u := range colUsed {162+ if !u {163+ return fmt.Errorf("column %d of the bounding box is unused", x)164+ }165+ }166+ parallel := map[[2]int]int{} // (row?, length) -> count167+ for _, ln := range s.Lines() {168+ if len(ln) < 4 || len(ln)%2 != 0 {169+ return fmt.Errorf("line of length %d at local %d (need even, >= 4)", len(ln), ln[0])170+ }171+ row := 0172+ if len(ln) == 1 || ln[1] == ln[0]+1 {173+ row = 1174+ }175+ parallel[[2]int{row, len(ln)}]++176+ }177+ // uniqueness is a pigeonhole: a shape may hold at most half as many178+ // parallel lines of one length as there are distinct valid lines of179+ // that length (decided 2026-08-26; the generator needs room to leave180+ // tiles under-determined, not just satisfiable)181+ for k, c := range parallel {182+ if max := DistinctLines(k[1]) / 2; c > max {183+ return fmt.Errorf("%d parallel lines of length %d, at most %d allowed (%d distinct valid lines exist)", c, k[1], max, DistinctLines(k[1]))184+ }185+ }186+ // connectivity187+ seen := make([]bool, len(m))188+ stack := []int{first}189+ seen[first] = true190+ count := 0191+ for len(stack) > 0 {192+ c := stack[len(stack)-1]193+ stack = stack[:len(stack)-1]194+ count++195+ x, y := c%s.W, c/s.W196+ for _, d := range [][2]int{{1, 0}, {-1, 0}, {0, 1}, {0, -1}} {197+ nx, ny := x+d[0], y+d[1]198+ if nx < 0 || ny < 0 || nx >= s.W || ny >= s.H {199+ continue200+ }201+ id := ny*s.W + nx202+ if m[id] && !seen[id] {203+ seen[id] = true204+ stack = append(stack, id)205+ }206+ }207+ }208+ if count != s.Cells() {209+ return fmt.Errorf("shape is not connected")210+ }211+ return nil212+}213+214+// DistinctLines is the number of distinct balanced, no-three binary lines215+// of length L (even): the ceiling on how many parallel lines of that216+// length one shape can hold under the uniqueness rule.217+func DistinctLines(L int) int {218+ distinctMu.Lock()219+ defer distinctMu.Unlock()220+ if n, ok := distinct[L]; ok {221+ return n222+ }223+ n := 0224+ var rec func(prev []Cell, ones int)225+ rec = func(prev []Cell, ones int) {226+ if len(prev) == L {227+ if ones == L/2 {228+ n++229+ }230+ return231+ }232+ for v := Cell(0); v <= 1; v++ {233+ k := len(prev)234+ if k >= 2 && prev[k-1] == v && prev[k-2] == v {235+ continue236+ }237+ o := ones238+ if v == 1 {239+ o++240+ }241+ if o > L/2 || (len(prev)+1-o) > L/2 {242+ continue243+ }244+ rec(append(prev, v), o)245+ }246+ }247+ rec(nil, 0)248+ distinct[L] = n249+ return n250+}251+252+var (253+ distinctMu sync.Mutex254+ distinct = map[int]int{} // L -> DistinctLines(L); 4:6, 6:14, 8:34, 10:84, 12:208, 14:518, 16:1296255+)256+257+// Local extracts the shape's window from a board-sized slice (row-major,258+// width W) as a local W*H slice; cells outside the shape are Empty.259+func (s Shape) Local(board []Cell, boardW int) []Cell {260+ m := s.Mask()261+ out := make([]Cell, s.W*s.H)262+ for i := range out {263+ out[i] = Empty264+ if m[i] {265+ out[i] = board[(s.Y0+i/s.W)*boardW+s.X0+i%s.W]266+ }267+ }268+ return out269+}270+271+// Line is one run of a shape's cells on a board, as global cell ids.272+type Line struct {273+ Shape int274+ Row bool275+ Cells []int276+}277+278+// geometry is what a board derives from its shapes once; clones share it.279+type geometry struct {280+ lines []Line281+ linesAt [][]int // per global cell: indexes into lines282+ shapeCells [][]int // per shape: global cell ids (row-major)283+ cells []int // every cell of any shape, in first-seen order284+ shapesAt [][]int // per global cell: shapes containing it285+}286+287+// Board is a W-by-H grid of cells and the shapes that constrain it.288+type Board struct {289+ W, H int290+ Cells []Cell291+ Shapes []Shape292+ geo *geometry293+}294+295+func NewBoard(w, h int) *Board {296+ b := &Board{W: w, H: h, Cells: make([]Cell, w*h)}297+ for i := range b.Cells {298+ b.Cells[i] = Empty299+ }300+ return b301+}302+303+// Single makes a board that is exactly one shape at the origin of its own304+// bounding box, with the given local cells (Empty outside the shape).305+func Single(s Shape, cells []Cell) *Board {306+ sh := Shape{X0: 0, Y0: 0, W: s.W, H: s.H, Rects: s.Rects}307+ return &Board{W: s.W, H: s.H, Cells: cells, Shapes: []Shape{sh}}308+}309+310+func (b *Board) Clone() *Board {311+ c := &Board{W: b.W, H: b.H, Cells: make([]Cell, len(b.Cells)), Shapes: b.Shapes, geo: b.geo}312+ copy(c.Cells, b.Cells)313+ return c314+}315+316+func (b *Board) Idx(x, y int) int { return y*b.W + x }317+func (b *Board) At(x, y int) Cell { return b.Cells[y*b.W+x] }318+func (b *Board) Set(x, y int, v Cell) { b.Cells[y*b.W+x] = v }319+320+// Geometry derives lines and ownership; built once per board and shared321+// by clones. Call it after changing Shapes.322+func (b *Board) Geometry() *geometry {323+ if b.geo != nil {324+ return b.geo325+ }326+ g := &geometry{327+ linesAt: make([][]int, b.W*b.H),328+ shapesAt: make([][]int, b.W*b.H),329+ }330+ seen := make([]bool, b.W*b.H)331+ for si, s := range b.Shapes {332+ m := s.Mask()333+ var cells []int334+ for i, ok := range m {335+ if !ok {336+ continue337+ }338+ id := (s.Y0+i/s.W)*b.W + s.X0 + i%s.W339+ cells = append(cells, id)340+ g.shapesAt[id] = append(g.shapesAt[id], si)341+ if !seen[id] {342+ seen[id] = true343+ g.cells = append(g.cells, id)344+ }345+ }346+ g.shapeCells = append(g.shapeCells, cells)347+ for _, ln := range s.Lines() {348+ // a horizontal run's local indexes step by 1, a vertical run's by W349+ l := Line{Shape: si, Row: len(ln) == 1 || ln[1] == ln[0]+1}350+ for _, local := range ln {351+ id := (s.Y0+local/s.W)*b.W + s.X0 + local%s.W352+ l.Cells = append(l.Cells, id)353+ g.linesAt[id] = append(g.linesAt[id], len(g.lines))354+ }355+ g.lines = append(g.lines, l)356+ }357+ }358+ b.geo = g359+ return g360+}361+362+// Lines exposes the derived lines.363+func (b *Board) Lines() []Line { return b.Geometry().lines }364+365+// excludes returns the rules under which placing v at global cell id is366+// illegal, each rule evaluated independently of the others, over every367+// line through the cell.368+func (b *Board) excludes(id int, v Cell, mask Mask) Mask {369+ var out Mask370+ g := b.Geometry()371+ for _, li := range g.linesAt[id] {372+ ln := g.lines[li]373+ n := len(ln.Cells)374+ pos := 0375+ for k, c := range ln.Cells {376+ if c == id {377+ pos = k378+ break379+ }380+ }381+ at := func(k int) Cell { return b.Cells[ln.Cells[k]] }382+ if mask&Run != 0 {383+ if (pos >= 2 && at(pos-1) == v && at(pos-2) == v) ||384+ (pos >= 1 && pos < n-1 && at(pos-1) == v && at(pos+1) == v) ||385+ (pos <= n-3 && at(pos+1) == v && at(pos+2) == v) {386+ out |= Run387+ }388+ }389+ if mask&(Balance|Unique) != 0 {390+ countV, filled := 0, 0391+ for k := 0; k < n; k++ {392+ c := at(k)393+ if c != Empty {394+ filled++395+ if c == v {396+ countV++397+ }398+ }399+ }400+ if mask&Balance != 0 && countV >= n/2 {401+ out |= Balance402+ }403+ if mask&Unique != 0 && out&Unique == 0 &&404+ (filled == n-1 || (filled == n-2 && mask&Balance != 0)) {405+ for oi, other := range g.lines {406+ if oi == li || other.Shape != ln.Shape || other.Row != ln.Row || len(other.Cells) != n {407+ continue408+ }409+ if b.lineWouldDuplicate(ln, pos, v, other) {410+ out |= Unique411+ break412+ }413+ }414+ }415+ }416+ }417+ return out418+}419+420+// lineWouldDuplicate reports whether placing v at position pos of line ln421+// makes it equal to the complete line other: every filled cell already422+// agrees, the placed cell agrees, and with at most one further blank423+// balance would fill it identically.424+func (b *Board) lineWouldDuplicate(ln Line, pos int, v Cell, other Line) bool {425+ blanks := 0426+ for k := range ln.Cells {427+ a, o := b.Cells[ln.Cells[k]], b.Cells[other.Cells[k]]428+ if k == pos {429+ a = v430+ }431+ if o == Empty {432+ return false433+ }434+ if a == Empty {435+ blanks++436+ continue437+ }438+ if a != o {439+ return false440+ }441+ }442+ return blanks <= 1443+}444+445+// Step is one cell fixed by propagation.446+type Step struct {447+ X, Y int448+ V Cell449+ Rules []string // rules that excluded the other value; "bifurcation" when found by search450+}451+452+// Validate reports the first violated rule among filled cells of any shape.453+func (b *Board) Validate(mask Mask) error {454+ g := b.Geometry()455+ for li, ln := range g.lines {456+ n := len(ln.Cells)457+ c0, c1 := 0, 0458+ for k, id := range ln.Cells {459+ c := b.Cells[id]460+ switch c {461+ case 0:462+ c0++463+ case 1:464+ c1++465+ }466+ if mask&Run != 0 && k >= 2 && c != Empty && c == b.Cells[ln.Cells[k-1]] && c == b.Cells[ln.Cells[k-2]] {467+ return fmt.Errorf("run: three %d in line %d of shape %d", c, li, ln.Shape)468+ }469+ }470+ if mask&Balance != 0 && (c0 > n/2 || c1 > n/2) {471+ return fmt.Errorf("balance: line %d of shape %d exceeds %d", li, ln.Shape, n/2)472+ }473+ }474+ if mask&Unique != 0 {475+ for i, a := range g.lines {476+ for j := i + 1; j < len(g.lines); j++ {477+ o := g.lines[j]478+ if o.Shape != a.Shape || o.Row != a.Row || len(o.Cells) != len(a.Cells) {479+ continue480+ }481+ eq := true482+ for k := range a.Cells {483+ if b.Cells[a.Cells[k]] == Empty || b.Cells[a.Cells[k]] != b.Cells[o.Cells[k]] {484+ eq = false485+ break486+ }487+ }488+ if eq {489+ return fmt.Errorf("unique: lines %d and %d equal in shape %d", i, j, a.Shape)490+ }491+ }492+ }493+ }494+ return nil495+}496+497+// Complete reports whether every cell of every shape is filled.498+func (b *Board) Complete() bool {499+ for _, id := range b.Geometry().cells {500+ if b.Cells[id] == Empty {501+ return false502+ }503+ }504+ return true505+}506+507+// Propagate fixes every cell that the active rules force, to a fixpoint,508+// then (depth > 0) bifurcates: a value whose assumption propagates (at509+// depth-1) to a contradiction is excluded. Returns the steps in order and510+// false on contradiction. The board is mutated.511+func (b *Board) Propagate(mask Mask, depth int) ([]Step, bool) {512+ var steps []Step513+ for {514+ for {515+ st, ok := b.propagateOnce(mask)516+ if !ok {517+ return steps, false518+ }519+ if len(st) == 0 {520+ break521+ }522+ steps = append(steps, st...)523+ }524+ if depth <= 0 {525+ return steps, true526+ }527+ found := false528+ for _, id := range b.Geometry().cells {529+ if b.Cells[id] != Empty {530+ continue531+ }532+ var bad [2]bool533+ for v := Cell(0); v <= 1; v++ {534+ t := b.Clone()535+ t.Cells[id] = v536+ if _, ok := t.Propagate(mask, depth-1); !ok {537+ bad[v] = true538+ }539+ }540+ if bad[0] && bad[1] {541+ return steps, false542+ }543+ if bad[0] || bad[1] {544+ v := Cell(0)545+ if bad[0] {546+ v = 1547+ }548+ b.Cells[id] = v549+ steps = append(steps, Step{X: id % b.W, Y: id / b.W, V: v, Rules: []string{"bifurcation"}})550+ found = true551+ break552+ }553+ }554+ if !found {555+ return steps, true556+ }557+ }558+}559+560+// propagateOnce evaluates every empty cell once against every line561+// through it and fixes those with a single admissible value. Rule562+// attribution is the union over lines of the rules excluding the rejected563+// value.564+func (b *Board) propagateOnce(mask Mask) ([]Step, bool) {565+ var steps []Step566+ type ex struct {567+ id int568+ e [2]Mask569+ }570+ var exs []ex571+ for _, id := range b.Geometry().cells {572+ if b.Cells[id] != Empty {573+ continue574+ }575+ exs = append(exs, ex{id, [2]Mask{b.excludes(id, 0, mask), b.excludes(id, 1, mask)}})576+ }577+ for _, a := range exs {578+ if a.e[0] != 0 && a.e[1] != 0 {579+ return steps, false580+ }581+ if a.e[0] == 0 && a.e[1] == 0 {582+ continue583+ }584+ v, why := Cell(0), a.e[1]585+ if a.e[0] != 0 {586+ v, why = 1, a.e[0]587+ }588+ if b.Cells[a.id] != Empty {589+ continue590+ }591+ b.Cells[a.id] = v592+ steps = append(steps, Step{X: a.id % b.W, Y: a.id / b.W, V: v, Rules: why.Names()})593+ }594+ return steps, true595+}596+597+// Solutions enumerates up to limit complete assignments consistent with the598+// active rules, by propagation plus branching on the most constrained cell.599+// The search is bounded by DefaultBudget nodes; see SolutionsBudget.600+func (b *Board) Solutions(mask Mask, limit int) [][]Cell {601+ out, _ := b.SolutionsBudget(mask, limit, DefaultBudget)602+ return out603+}604+605+// DefaultBudget is the node budget for Solutions: past it the enumeration606+// stops and reports exhausted=false. This solver models technique, not607+// search; the sat package answers counting questions definitively.608+const DefaultBudget = 200000609+610+// SolutionsBudget is Solutions with an explicit node budget. exhausted is611+// true when the search space was fully explored (or limit was reached).612+func (b *Board) SolutionsBudget(mask Mask, limit int, budget int) (sols [][]Cell, exhausted bool) {613+ var out [][]Cell614+ nodes := 0615+ over := false616+ var rec func(t *Board)617+ rec = func(t *Board) {618+ if len(out) >= limit || over {619+ return620+ }621+ nodes++622+ if nodes > budget {623+ over = true624+ return625+ }626+ if _, ok := t.Propagate(mask, 0); !ok {627+ return628+ }629+ if t.Complete() {630+ if t.Validate(mask) == nil {631+ c := make([]Cell, len(t.Cells))632+ copy(c, t.Cells)633+ out = append(out, c)634+ }635+ return636+ }637+ id := t.pickBranch()638+ for v := Cell(0); v <= 1; v++ {639+ u := t.Clone()640+ u.Cells[id] = v641+ rec(u)642+ if len(out) >= limit || over {643+ return644+ }645+ }646+ }647+ rec(b.Clone())648+ return out, !over649+}650+651+// pickBranch chooses an empty cell whose lines are the most filled.652+func (b *Board) pickBranch() int {653+ g := b.Geometry()654+ filled := make([]int, len(g.lines))655+ for li, ln := range g.lines {656+ for _, id := range ln.Cells {657+ if b.Cells[id] != Empty {658+ filled[li]++659+ }660+ }661+ }662+ best, bestScore := -1, -1663+ for _, id := range g.cells {664+ if b.Cells[id] != Empty {665+ continue666+ }667+ s := 0668+ for _, li := range g.linesAt[id] {669+ s += filled[li]670+ }671+ if s > bestScore {672+ best, bestScore = id, s673+ }674+ }675+ return best676+}677+678+// Rect is a 2x2 flip rectangle in shape-local coordinates: cells679+// (C1,R1),(C2,R1),(C1,R2),(C2,R2) with S[R1][C1]=S[R2][C2] != S[R1][C2]=S[R2][C1].680+type Rect struct{ R1, C1, R2, C2 int }681+682+func (r Rect) Cells() [4][2]int {683+ return [4][2]int{{r.C1, r.R1}, {r.C2, r.R1}, {r.C1, r.R2}, {r.C2, r.R2}}684+}685+686+// FindFlips lists every rectangle of a complete shape (s is H rows of W687+// local cells, Empty outside the shape) whose four corners lie on two688+// shared row lines and two shared column lines and can be flipped (0<->1)689+// leaving the shape valid under mask.690+func FindFlips(sh Shape, s [][]Cell, mask Mask) []Rect {691+ W, H := sh.W, sh.H692+ m := sh.Mask()693+ // line id per cell per orientation, for the "same line" test694+ rowOf := make([]int, W*H)695+ colOf := make([]int, W*H)696+ for i := range rowOf {697+ rowOf[i], colOf[i] = -1, -1698+ }699+ for li, ln := range sh.Lines() {700+ row := len(ln) == 1 || ln[1] == ln[0]+1701+ for _, c := range ln {702+ if row {703+ rowOf[c] = li704+ } else {705+ colOf[c] = li706+ }707+ }708+ }709+ var out []Rect710+ for r1 := 0; r1 < H; r1++ {711+ for r2 := r1 + 1; r2 < H; r2++ {712+ for c1 := 0; c1 < W; c1++ {713+ for c2 := c1 + 1; c2 < W; c2++ {714+ a, bb, c, d := r1*W+c1, r1*W+c2, r2*W+c1, r2*W+c2715+ if !m[a] || !m[bb] || !m[c] || !m[d] {716+ continue717+ }718+ if rowOf[a] != rowOf[bb] || rowOf[c] != rowOf[d] || colOf[a] != colOf[c] || colOf[bb] != colOf[d] {719+ continue720+ }721+ if s[r1][c1] != s[r2][c2] || s[r1][c2] != s[r2][c1] || s[r1][c1] == s[r1][c2] {722+ continue723+ }724+ r := Rect{r1, c1, r2, c2}725+ t := FlipGrid(s, r)726+ cells := make([]Cell, W*H)727+ for y := 0; y < H; y++ {728+ copy(cells[y*W:(y+1)*W], t[y])729+ }730+ if Single(sh, cells).Validate(mask) == nil {731+ out = append(out, r)732+ }733+ }734+ }735+ }736+ }737+ return out738+}739+740+// FlipGrid returns a copy of s with the rectangle's corners inverted.741+func FlipGrid(s [][]Cell, r Rect) [][]Cell {742+ t := make([][]Cell, len(s))743+ for i := range s {744+ t[i] = append([]Cell(nil), s[i]...)745+ }746+ for _, c := range r.Cells() {747+ t[c[1]][c[0]] = 1 - t[c[1]][c[0]]748+ }749+ return t750+}751+752+// TileSolutions is the solution set of one shape alone, as flat local W*H753+// slices (Empty outside the shape).754+type TileSolutions [][]Cell755+756+// CoupledSolutionsGrid counts coupled solutions for an X-by-X grid of757+// n-squares on a pitch of n-1 (the phase-1 layout).758+func CoupledSolutionsGrid(X, n int, sols []TileSolutions, limit int) (int, [][]int) {759+ ws := make([]Shape, 0, X*X)760+ for ty := 0; ty < X; ty++ {761+ for tx := 0; tx < X; tx++ {762+ ws = append(ws, Square(tx*(n-1), ty*(n-1), n))763+ }764+ }765+ return CoupledSolutions(ws, sols, limit)766+}767+768+// CoupledSolutions counts (up to limit) the choices of one solution per769+// shape such that every pair of shapes agrees on every shared cell.770+func CoupledSolutions(ws []Shape, sols []TileSolutions, limit int) (int, [][]int) {771+ type pair struct{ a, b int }772+ masks := make([][]bool, len(ws))773+ for i, s := range ws {774+ masks[i] = s.Mask()775+ }776+ overlap := func(a, b int) [][2]int {777+ wa, wb := ws[a], ws[b]778+ var cells [][2]int // local index in a, local index in b779+ x0, x1 := max(wa.X0, wb.X0), min(wa.X0+wa.W, wb.X0+wb.W)780+ y0, y1 := max(wa.Y0, wb.Y0), min(wa.Y0+wa.H, wb.Y0+wb.H)781+ for gy := y0; gy < y1; gy++ {782+ for gx := x0; gx < x1; gx++ {783+ la := (gy-wa.Y0)*wa.W + gx - wa.X0784+ lb := (gy-wb.Y0)*wb.W + gx - wb.X0785+ if masks[a][la] && masks[b][lb] {786+ cells = append(cells, [2]int{la, lb})787+ }788+ }789+ }790+ return cells791+ }792+ compat := map[pair][][]bool{}793+ neighbours := make([][]int, len(ws))794+ for a := range ws {795+ for b := a + 1; b < len(ws); b++ {796+ cells := overlap(a, b)797+ if len(cells) == 0 {798+ continue799+ }800+ neighbours[a] = append(neighbours[a], b)801+ neighbours[b] = append(neighbours[b], a)802+ tbl := make([][]bool, len(sols[a]))803+ for i, sa := range sols[a] {804+ tbl[i] = make([]bool, len(sols[b]))805+ for j, sb := range sols[b] {806+ ok := true807+ for _, c := range cells {808+ if sa[c[0]] != sb[c[1]] {809+ ok = false810+ break811+ }812+ }813+ tbl[i][j] = ok814+ }815+ }816+ compat[pair{a, b}] = tbl817+ }818+ }819+ ok := func(a, i, b, j int) bool {820+ if a < b {821+ return compat[pair{a, b}][i][j]822+ }823+ return compat[pair{b, a}][j][i]824+ }825+ choice := make([]int, len(ws))826+ for i := range choice {827+ choice[i] = -1828+ }829+ var found [][]int830+ var rec func(t int)831+ rec = func(t int) {832+ if len(found) >= limit {833+ return834+ }835+ if t == len(ws) {836+ found = append(found, append([]int(nil), choice...))837+ return838+ }839+ for i := range sols[t] {840+ good := true841+ for _, nb := range neighbours[t] {842+ if choice[nb] >= 0 && !ok(t, i, nb, choice[nb]) {843+ good = false844+ break845+ }846+ }847+ if !good {848+ continue849+ }850+ choice[t] = i851+ rec(t + 1)852+ choice[t] = -1853+ }854+ }855+ rec(0)856+ return len(found), found857+}858+859+// Diff lists the flat indices where two equal-length cell slices differ.860+func Diff(a, b []Cell) []int {861+ var out []int862+ for i := range a {863+ if a[i] != b[i] {864+ out = append(out, i)865+ }866+ }867+ sort.Ints(out)868+ return out869+}870+871+// Rating is the technique ladder's verdict on a puzzle: which techniques872+// the ladder solver had to use. The ladder is the one the difficulty873+// literature uses: run+balance propagation first, the uniqueness rule only874+// when that stalls, and a depth-1 bifurcation only when all three stall.875+type Rating struct {876+ UsedUnique bool877+ UsedBifurcation bool878+ Complete bool879+ Bifurcations int880+}881+882+// Ladder solves b (mutating it) with the technique ladder and reports what883+// it needed. maxBifurcations bounds the search; when exceeded Complete is884+// false and UsedBifurcation is true.885+func (b *Board) Ladder(maxBifurcations int) Rating {886+ var r Rating887+ for {888+ if _, ok := b.Propagate(Run|Balance, 0); !ok {889+ return r890+ }891+ if b.Complete() {892+ r.Complete = true893+ return r894+ }895+ st, ok := b.propagateOnce(All)896+ if !ok {897+ return r898+ }899+ for _, s := range st {900+ for _, name := range s.Rules {901+ if name == "unique" {902+ r.UsedUnique = true903+ }904+ }905+ }906+ if len(st) > 0 {907+ continue908+ }909+ if b.Complete() {910+ r.Complete = true911+ return r912+ }913+ r.UsedBifurcation = true914+ if r.Bifurcations >= maxBifurcations {915+ return r916+ }917+ r.Bifurcations++918+ found, ok := b.bifurcateOnce(All)919+ if !ok {920+ return r921+ }922+ if !found {923+ return r924+ }925+ }926+}927+928+// bifurcateOnce fixes the first cell whose one value propagates (depth 0,929+// mask) to a contradiction. Returns found=false when no cell is decidable930+// this way, ok=false when both values contradict.931+func (b *Board) bifurcateOnce(mask Mask) (found bool, ok bool) {932+ for _, id := range b.Geometry().cells {933+ if b.Cells[id] != Empty {934+ continue935+ }936+ var bad [2]bool937+ for v := Cell(0); v <= 1; v++ {938+ t := b.Clone()939+ t.Cells[id] = v940+ if _, ok := t.Propagate(mask, 0); !ok {941+ bad[v] = true942+ }943+ }944+ if bad[0] && bad[1] {945+ return false, false946+ }947+ if bad[0] || bad[1] {948+ v := Cell(0)949+ if bad[0] {950+ v = 1951+ }952+ b.Cells[id] = v953+ return true, true954+ }955+ }956+ return false, true957+}@@ -0,0 +1,382 @@
1+package rules2+3+import (4+ "strings"5+ "testing"6+)7+8+func parse(t *testing.T, rows ...string) *Board {9+ t.Helper()10+ n := len(rows)11+ b := NewBoard(n, n)12+ b.Shapes = []Shape{Square(0, 0, n)}13+ for y, r := range rows {14+ if len(r) != n {15+ t.Fatalf("row %d has %d cells, want %d", y, len(r), n)16+ }17+ for x, ch := range r {18+ switch ch {19+ case '0':20+ b.Set(x, y, 0)21+ case '1':22+ b.Set(x, y, 1)23+ }24+ }25+ }26+ return b27+}28+29+func TestExcludesEachRuleIndependently(t *testing.T) {30+ // row 0: "00...." -> placing 0 at (2,0) makes a run; balance needs 3 of each31+ b := parse(t,32+ "00....",33+ "......",34+ "......",35+ "......",36+ "......",37+ "......")38+ if ex := b.excludes(b.Idx(2, 0), 0, All); ex&Run == 0 || ex&Balance != 0 {39+ t.Fatalf("want run only, got %v", ex.Names())40+ }41+ // balance: row 1 already has three 1s42+ b = parse(t,43+ "......",44+ "1.1.1.",45+ "......",46+ "......",47+ "......",48+ "......")49+ if ex := b.excludes(b.Idx(1, 1), 1, All); ex&Balance == 0 {50+ t.Fatalf("want balance, got %v", ex.Names())51+ }52+ // unique: completing row 1 as 010101 would equal row 053+ b = parse(t,54+ "010101",55+ "0.0101",56+ "......",57+ "......",58+ "......",59+ "......")60+ if ex := b.excludes(b.Idx(1, 1), 1, All); ex&Unique == 0 {61+ t.Fatalf("want unique, got %v", ex.Names())62+ }63+ if ex := b.excludes(b.Idx(1, 1), 1, Run|Balance); ex != 0 {64+ t.Fatalf("unique must not fire when masked out, got %v", ex.Names())65+ }66+}67+68+func TestPropagateRecoversRemovedCluesWithAttribution(t *testing.T) {69+ e := NewBoard(6, 6)70+ e.Shapes = []Shape{Square(0, 0, 6)}71+ sol := e.Solutions(All, 1)[0]72+ // blank a cell only when propagation gets it back: the puzzle stays73+ // propagation-solvable and every step must carry a rule name.74+ b := &Board{W: 6, H: 6, Cells: append([]Cell(nil), sol...), Shapes: e.Shapes}75+ blanked := 076+ for i := range sol {77+ b.Cells[i] = Empty78+ t2 := b.Clone()79+ t2.Propagate(All, 0)80+ if t2.Cells[i] != sol[i] {81+ b.Cells[i] = sol[i]82+ continue83+ }84+ blanked++85+ }86+ if blanked < 10 {87+ t.Fatalf("only %d cells blanked", blanked)88+ }89+ steps, ok := b.Propagate(All, 0)90+ if !ok || !b.Complete() {91+ t.Fatalf("ok=%v complete=%v\n%s", ok, b.Complete(), dump(b))92+ }93+ for i := range sol {94+ if b.Cells[i] != sol[i] {95+ t.Fatalf("cell %d differs from the solution", i)96+ }97+ }98+ if len(steps) != blanked {99+ t.Fatalf("%d steps for %d blanks", len(steps), blanked)100+ }101+ for _, s := range steps {102+ if len(s.Rules) == 0 {103+ t.Fatalf("step %v has no rule attribution", s)104+ }105+ }106+}107+108+func TestSolutionsCountsAndMask(t *testing.T) {109+ // an empty 4x4 has 72 valid grids under run+balance, fewer with uniqueness110+ e := NewBoard(4, 4)111+ e.Shapes = []Shape{Square(0, 0, 4)}112+ all := len(e.Solutions(All, 1000))113+ noUnique := len(e.Solutions(Run|Balance, 1000))114+ if noUnique <= all || all == 0 {115+ t.Fatalf("all=%d noUnique=%d", all, noUnique)116+ }117+ for _, s := range e.Solutions(All, 1000) {118+ c := &Board{W: 4, H: 4, Cells: s, Shapes: e.Shapes}119+ if err := c.Validate(All); err != nil {120+ t.Fatal(err)121+ }122+ }123+}124+125+func TestSeamCouplesTwoShapes(t *testing.T) {126+ // two 4x4 squares overlapping by one column (pitch 3) on a 7x4 board127+ b := NewBoard(7, 4)128+ b.Shapes = []Shape{Square(0, 0, 4), Square(3, 0, 4)}129+ sols := b.Solutions(All, 100000)130+ single := NewBoard(4, 4)131+ single.Shapes = []Shape{Square(0, 0, 4)}132+ one := len(single.Solutions(All, 1000))133+ if len(sols) >= one*one {134+ t.Fatalf("seam did not constrain: %d coupled vs %d*%d", len(sols), one, one)135+ }136+}137+138+func TestFindFlipsProducesValidAlternatives(t *testing.T) {139+ s := [][]Cell{140+ {0, 1, 0, 1, 1, 0},141+ {1, 0, 1, 0, 0, 1},142+ {0, 1, 1, 0, 1, 0},143+ {1, 0, 0, 1, 0, 1},144+ {0, 1, 0, 1, 1, 0},145+ {1, 0, 1, 0, 0, 1},146+ }147+ // rows 0 and 4 are equal: not a valid Takuzu, so fix row 4/5 to be distinct148+ s[4] = []Cell{1, 1, 0, 0, 1, 0}149+ s[5] = []Cell{0, 0, 1, 1, 0, 1}150+ sq := Square(0, 0, 6)151+ b := &Board{W: 6, H: 6, Shapes: []Shape{sq}}152+ for _, r := range s {153+ b.Cells = append(b.Cells, r...)154+ }155+ if err := b.Validate(All); err != nil {156+ t.Skip("fixture invalid: " + err.Error())157+ }158+ flips := FindFlips(sq, s, All)159+ for _, r := range flips {160+ f := FlipGrid(s, r)161+ c := &Board{W: 6, H: 6, Shapes: b.Shapes}162+ for _, row := range f {163+ c.Cells = append(c.Cells, row...)164+ }165+ if err := c.Validate(All); err != nil {166+ t.Fatalf("flip %v invalid: %v", r, err)167+ }168+ if len(Diff(b.Cells, c.Cells)) != 4 {169+ t.Fatalf("flip %v changed %d cells", r, len(Diff(b.Cells, c.Cells)))170+ }171+ }172+}173+174+func TestCoupledSolutionsAgreesOnSharedCells(t *testing.T) {175+ // a real 2x2 mosaic of 4x4 tiles (7x7 board); each tile's solution set is176+ // its true window plus the windows of other coupled mosaics, so the CSP177+ // must find the true assignment and reject any seam mismatch.178+ n, X := 4, 2179+ b := NewBoard(7, 7)180+ b.Shapes = []Shape{Square(0, 0, n), Square(3, 0, n), Square(0, 3, n), Square(3, 3, n)}181+ all := b.Solutions(All, 6)182+ if len(all) < 2 {183+ t.Fatalf("want several mosaics, got %d", len(all))184+ }185+ sols := make([]TileSolutions, X*X)186+ for ti, sh := range b.Shapes {187+ for _, mosaic := range all {188+ sols[ti] = append(sols[ti], sh.Local(mosaic, 7))189+ }190+ }191+ count, found := CoupledSolutionsGrid(X, n, sols, 100)192+ if count < len(all) {193+ t.Fatalf("count %d < %d true mosaics", count, len(all))194+ }195+ for _, ch := range found {196+ s0, s1 := sols[0][ch[0]], sols[1][ch[1]]197+ for y := 0; y < n; y++ {198+ if s0[y*n+3] != s1[y*n] {199+ t.Fatalf("seam mismatch in %v", ch)200+ }201+ }202+ }203+}204+205+// tee is a T: an 8-wide, 6-tall crossbar over a 4-wide, 2-tall stem206+// (bounding box 8x8, 56 cells). Lines: rows of 8 (6 of them), rows of 4207+// (2, the stem), columns of 8 (4, through the stem), columns of 6 (4,208+// crossbar only). Two parallel 4-lines is within the pigeonhole bound209+// (at most DistinctLines(4)/2 = 3).210+func tee() Shape {211+ return Shape{W: 8, H: 8, Rects: [][4]int{{0, 0, 8, 6}, {2, 6, 4, 2}}}212+}213+214+func TestShapeLinesAndValid(t *testing.T) {215+ sh := tee()216+ if sh.Cells() != 56 {217+ t.Fatalf("cells %d", sh.Cells())218+ }219+ lines := sh.Lines()220+ if len(lines) != 16 {221+ t.Fatalf("%d lines, want 16", len(lines))222+ }223+ lens := map[int]int{}224+ for _, ln := range lines {225+ lens[len(ln)]++226+ }227+ if lens[8] != 10 || lens[4] != 2 || lens[6] != 4 {228+ t.Fatalf("line lengths %v", lens)229+ }230+ if err := sh.Valid(); err != nil {231+ t.Fatal(err)232+ }233+ // odd stem width -> odd lines234+ bad := Shape{W: 8, H: 8, Rects: [][4]int{{0, 0, 8, 6}, {2, 6, 3, 2}}}235+ if bad.Valid() == nil {236+ t.Fatal("odd line accepted")237+ }238+ // a 2-wide stem makes 2-long rows239+ short := Shape{W: 8, H: 8, Rects: [][4]int{{0, 0, 8, 6}, {3, 6, 2, 2}}}240+ if short.Valid() == nil {241+ t.Fatal("2-long line accepted")242+ }243+ // disconnected244+ two := Shape{W: 10, H: 4, Rects: [][4]int{{0, 0, 4, 4}, {6, 0, 4, 4}}}245+ if two.Valid() == nil {246+ t.Fatal("disconnected shape accepted")247+ }248+ // loose bounding box249+ loose := Shape{W: 6, H: 4, Rects: [][4]int{{0, 0, 4, 4}}}250+ if loose.Valid() == nil {251+ t.Fatal("loose bounding box accepted")252+ }253+ if !sh.Contains(3, 6) || sh.Contains(0, 6) || sh.Contains(8, 0) {254+ t.Fatal("Contains wrong")255+ }256+ // pigeonhole: at most DistinctLines(L)/2 parallel lines of length L.257+ // A 4x12 has 12 parallel 4-lines (6 distinct exist, 3 allowed); even a258+ // 4x4 square has 4 > 3; a 6x6 has 6 parallel 6-lines (14 exist, 7259+ // allowed) and is the smallest square260+ thin := Shape{W: 4, H: 12, Rects: [][4]int{{0, 0, 4, 12}}}261+ if thin.Valid() == nil {262+ t.Fatal("4x12 accepted despite the uniqueness pigeonhole")263+ }264+ if Square(0, 0, 4).Valid() == nil {265+ t.Fatal("4x4 accepted: 4 parallel 4-lines, 3 allowed")266+ }267+ if Square(0, 0, 6).Valid() != nil || Square(0, 0, 16).Valid() != nil {268+ t.Fatal("6x6 or 16x16 rejected")269+ }270+ if (Shape{W: 12, H: 6, Rects: [][4]int{{0, 0, 12, 6}}}).Valid() == nil {271+ t.Fatal("12x6 accepted: 12 parallel 6-lines, 7 allowed")272+ }273+ if (Shape{W: 12, H: 8, Rects: [][4]int{{0, 0, 12, 8}}}).Valid() != nil {274+ t.Fatal("12x8 rejected: 12 parallel 8-lines, 17 allowed")275+ }276+ want := map[int]int{4: 6, 6: 14, 8: 34, 10: 84, 12: 208, 14: 518, 16: 1296}277+ for L, n := range want {278+ if DistinctLines(L) != n {279+ t.Fatalf("DistinctLines(%d) = %d, want %d", L, DistinctLines(L), n)280+ }281+ }282+}283+284+func TestShapeRulesOnATee(t *testing.T) {285+ sh := tee()286+ b := NewBoard(8, 8)287+ b.Shapes = []Shape{sh}288+ // the stem's row at y=6 spans x=2..5: two 0s at x=2,3 exclude 0 at x=4 (run)289+ b.Set(2, 6, 0)290+ b.Set(3, 6, 0)291+ if ex := b.excludes(b.Idx(4, 6), 0, All); ex&Run == 0 {292+ t.Fatalf("run along a 4-line: %v", ex.Names())293+ }294+ // balance on the 4-line: two 0s already -> a third 0 at x=5 is excluded295+ if ex := b.excludes(b.Idx(5, 6), 0, All); ex&Balance == 0 {296+ t.Fatalf("balance along a 4-line: %v", ex.Names())297+ }298+ // cells outside the shape are never touched by propagation299+ steps, ok := b.Propagate(All, 0)300+ if !ok {301+ t.Fatal("contradiction on a legal partial")302+ }303+ for _, s := range steps {304+ if !sh.Contains(s.X, s.Y) {305+ t.Fatalf("step outside the shape at (%d,%d)", s.X, s.Y)306+ }307+ }308+ if b.At(0, 6) != Empty {309+ t.Fatal("hole cell was written")310+ }311+ // a full solution exists, validates, and the ladder can solve a312+ // propagation-friendly puzzle over it313+ e := NewBoard(8, 8)314+ e.Shapes = []Shape{sh}315+ sols := e.Solutions(All, 3)316+ if len(sols) == 0 {317+ t.Fatal("no solution for a T")318+ }319+ full := &Board{W: 8, H: 8, Cells: sols[0], Shapes: e.Shapes}320+ if err := full.Validate(All); err != nil {321+ t.Fatal(err)322+ }323+ for _, id := range full.Geometry().cells {324+ if full.Cells[id] == Empty {325+ t.Fatal("incomplete solution")326+ }327+ }328+ if !full.Complete() {329+ t.Fatal("Complete false on a full T")330+ }331+ puzzle := full.Clone()332+ for i := range puzzle.Cells {333+ if sh.Contains(i%8, i/8) && i%3 == 0 {334+ puzzle.Cells[i] = Empty335+ }336+ }337+ r := puzzle.Ladder(4)338+ if !r.Complete && !r.UsedBifurcation {339+ t.Fatalf("ladder neither completed nor bifurcated: %+v", r)340+ }341+ // uniqueness only compares lines of equal length and orientation: the342+ // crossbar's 8-rows never collide with the stem's 4-rows343+ loc := sh.Local(full.Cells, 8)344+ rows := [][]Cell{}345+ for y := 0; y < 8; y++ {346+ rows = append(rows, loc[y*8:(y+1)*8])347+ }348+ for _, r := range FindFlips(sh, rows, All) {349+ for _, c := range r.Cells() {350+ if !sh.Contains(c[0], c[1]) {351+ t.Fatalf("flip %v uses a cell outside the shape", r)352+ }353+ }354+ // both rows of the rectangle must be one line each: a crossbar row355+ // and a stem row share x=2..5, and a rectangle across them is fine356+ // only if all four cells are on shared lines, which FindFlips checks357+ f := FlipGrid(rows, r)358+ cells := make([]Cell, 64)359+ for y := 0; y < 8; y++ {360+ copy(cells[y*8:(y+1)*8], f[y])361+ }362+ if err := Single(sh, cells).Validate(All); err != nil {363+ t.Fatalf("flip %v invalid: %v", r, err)364+ }365+ }366+}367+368+func dump(b *Board) string {369+ var sb strings.Builder370+ for y := 0; y < b.H; y++ {371+ for x := 0; x < b.W; x++ {372+ switch b.At(x, y) {373+ case Empty:374+ sb.WriteByte('.')375+ default:376+ sb.WriteByte(byte('0' + b.At(x, y)))377+ }378+ }379+ sb.WriteByte('\n')380+ }381+ return sb.String()382+}@@ -0,0 +1,432 @@
1+// Package sat answers the generator's questions about one Takuzu shape2+// with a CDCL SAT solver (gophersat) rather than a hand-rolled backtracker:3+// complete a partial shape (randomised), decide whether a partial shape has4+// any completion, and enumerate solutions up to a limit. Binary puzzles are5+// flat for SAT at every size in play (the literature's 0.3 s at 14x14 is6+// the slow end; a shape with fixed edges is milliseconds), where MRV7+// backtracking without propagation can spend seconds failing to refute an8+// infeasible prefill or to complete a tile with four fixed sides.9+//10+// Encoding, per shape with rule mask m, over the shape's lines (every11+// maximal horizontal or vertical run of its cells):12+//13+// x(cell) one variable per cell, true = 114+// run for every three consecutive cells of a line,15+// (a | b | c) and (!a | !b | !c)16+// balance every line has exactly len/2 true literals17+// (a pair of cardinality constraints)18+// unique for every pair of lines of one orientation and equal19+// length an auxiliary d(k) <-> x(i,k) xor x(j,k) per20+// position, and a clause d(1) | ... | d(len)21+// fixed cells unit clauses22+//23+// The rules package keeps the propagation solver: that one models the24+// human technique ladder (pairs, sandwiches, balance, uniqueness,25+// bifurcation) and is what forced/guess attribution and difficulty rating26+// mean. This package is for questions where only the answer matters.27+package sat28+29+import (30+ "math/rand/v2"31+ "strings"32+ "sync"33+34+ "github.com/crillab/gophersat/solver"35+36+ "mosaic-engine/rules"37+)38+39+// problem is the encoding of one shape under a rule mask, without the40+// fixed cells, so it can be built once per (shape, mask) and reused.41+// Variables: local index + 1 for cells (absent cells are simply unused),42+// auxiliaries above W*H.43+type problem struct {44+ W, H int45+ cells []int // local indexes of the shape's cells46+ nbVars int47+ constrs []solver.PBConstr48+}49+50+// lineConstraints appends the rules for one set of lines, with x mapping a51+// line position to a variable id; next is the first free auxiliary id.52+func lineConstraints(lines [][]int, x func(local int) int, mask rules.Mask, next int, cs []solver.PBConstr) (int, []solver.PBConstr) {53+ if mask&rules.Run != 0 {54+ for _, ln := range lines {55+ for k := 0; k+2 < len(ln); k++ {56+ cs = append(cs, solver.PropClause(x(ln[k]), x(ln[k+1]), x(ln[k+2])))57+ cs = append(cs, solver.PropClause(-x(ln[k]), -x(ln[k+1]), -x(ln[k+2])))58+ }59+ }60+ }61+ if mask&rules.Balance != 0 {62+ for _, ln := range lines {63+ lits := make([]int, len(ln))64+ for k, c := range ln {65+ lits[k] = x(c)66+ }67+ cs = append(cs, solver.AtLeast(append([]int(nil), lits...), len(ln)/2), solver.AtMost(lits, len(ln)/2))68+ }69+ }70+ if mask&rules.Unique != 0 {71+ // orientation: consecutive local indexes differ by 1 in a row72+ row := func(ln []int) bool { return len(ln) == 1 || ln[1] == ln[0]+1 }73+ for i := 0; i < len(lines); i++ {74+ for j := i + 1; j < len(lines); j++ {75+ a, b := lines[i], lines[j]76+ if len(a) != len(b) || row(a) != row(b) {77+ continue78+ }79+ ds := make([]int, len(a))80+ for k := range a {81+ d := next82+ next++83+ ds[k] = d84+ u, v := x(a[k]), x(b[k])85+ cs = append(cs,86+ solver.PropClause(-d, u, v),87+ solver.PropClause(-d, -u, -v),88+ solver.PropClause(d, -u, v),89+ solver.PropClause(d, u, -v),90+ )91+ }92+ cs = append(cs, solver.PropClause(ds...))93+ }94+ }95+ }96+ return next, cs97+}98+99+func encode(sh rules.Shape, mask rules.Mask) *problem {100+ p := &problem{W: sh.W, H: sh.H}101+ for i, ok := range sh.Mask() {102+ if ok {103+ p.cells = append(p.cells, i)104+ }105+ }106+ x := func(local int) int { return local + 1 }107+ next := sh.W*sh.H + 1108+ next, p.constrs = lineConstraints(sh.Lines(), x, mask, next, nil)109+ p.nbVars = next - 1110+ return p111+}112+113+// solverFor builds a solver for the shape with the given cells fixed and114+// extra constraints (blocking clauses), optionally relabelling the shape's115+// cell variables (perm maps a local index to the local index whose116+// variable it uses) and shuffling the constraint order.117+func (p *problem) solverFor(cells []rules.Cell, extra []solver.PBConstr, perm map[int]int, shuffle *rand.Rand) *solver.Solver {118+ cs := make([]solver.PBConstr, 0, len(p.constrs)+len(cells)+len(extra))119+ // every constraint is copied: gophersat takes ownership of the slices120+ // it is given and may reorder them, and the cached encoding is shared121+ // by concurrent callers122+ relabel := func(c solver.PBConstr) solver.PBConstr {123+ lits := make([]int, len(c.Lits))124+ for i, l := range c.Lits {125+ v := l126+ if v < 0 {127+ v = -v128+ }129+ if perm != nil {130+ if r, ok := perm[v-1]; ok {131+ v = r + 1132+ }133+ }134+ if l < 0 {135+ v = -v136+ }137+ lits[i] = v138+ }139+ var weights []int140+ if c.Weights != nil {141+ weights = append([]int(nil), c.Weights...)142+ }143+ return solver.PBConstr{Lits: lits, Weights: weights, AtLeast: c.AtLeast}144+ }145+ for _, i := range p.cells {146+ v := cells[i]147+ if v == rules.Empty {148+ continue149+ }150+ lit := i + 1151+ if v == 0 {152+ lit = -lit153+ }154+ cs = append(cs, relabel(solver.PropClause(lit)))155+ }156+ for _, c := range p.constrs {157+ cs = append(cs, relabel(c))158+ }159+ for _, c := range extra {160+ cs = append(cs, relabel(c))161+ }162+ if shuffle != nil {163+ // shuffling the constraint order changes the solver's first164+ // decisions too165+ shuffle.Shuffle(len(cs), func(a, b int) { cs[a], cs[b] = cs[b], cs[a] })166+ }167+ return solver.New(solver.ParsePBConstrs(cs))168+}169+170+// model reads the shape's cells back (Empty outside the shape).171+func (p *problem) model(s *solver.Solver, perm map[int]int) []rules.Cell {172+ m := s.Model()173+ out := make([]rules.Cell, p.W*p.H)174+ for i := range out {175+ out[i] = rules.Empty176+ }177+ for _, i := range p.cells {178+ v := i179+ if perm != nil {180+ if r, ok := perm[i]; ok {181+ v = r182+ }183+ }184+ out[i] = 0185+ if v < len(m) && m[v] {186+ out[i] = 1187+ }188+ }189+ return out190+}191+192+type key struct {193+ W, H int194+ mask string195+ rule rules.Mask196+}197+198+func keyFor(sh rules.Shape, mask rules.Mask) key {199+ var sb strings.Builder200+ for _, b := range sh.Mask() {201+ if b {202+ sb.WriteByte('1')203+ } else {204+ sb.WriteByte('0')205+ }206+ }207+ return key{sh.W, sh.H, sb.String(), mask}208+}209+210+var (211+ cacheMu sync.Mutex212+ cache = map[key]*problem{}213+ // gophersat keeps a package-level buffer for clause learning214+ // (solver/learn.go: bufLits), so two solvers must never run at once.215+ // Calls are milliseconds; serialising them costs less than the216+ // generator's parallel waves would gain.217+ solveMu sync.Mutex218+)219+220+func solve(s *solver.Solver) solver.Status {221+ solveMu.Lock()222+ defer solveMu.Unlock()223+ return s.Solve()224+}225+226+// problemFor returns the encoding for (shape, mask), built once. Safe for227+// concurrent use: the generator builds givens in parallel waves.228+func problemFor(sh rules.Shape, mask rules.Mask) *problem {229+ k := keyFor(sh, mask)230+ cacheMu.Lock()231+ defer cacheMu.Unlock()232+ if p, ok := cache[k]; ok {233+ return p234+ }235+ p := encode(sh, mask)236+ cache[k] = p237+ return p238+}239+240+// Feasible reports whether the partial shape (local W*H cells, Empty241+// marks blanks) has a completion under the mask. The answer is definitive.242+func Feasible(cells []rules.Cell, sh rules.Shape, mask rules.Mask) bool {243+ p := problemFor(sh, mask)244+ return solve(p.solverFor(cells, nil, nil, nil)) == solver.Sat245+}246+247+// Complete returns one completion of the partial shape under all rules,248+// or ok=false when none exists. rng varies the result: the cell variables249+// are relabelled by a random permutation of the shape's cells and the250+// constraints shuffled, so the solver's first decisions differ per draw;251+// on top of that a few blank cells are fixed at random values first and252+// dropped again if that makes the shape infeasible.253+func Complete(cells []rules.Cell, sh rules.Shape, rng *rand.Rand) (sol []rules.Cell, ok bool) {254+ p := problemFor(sh, rules.All)255+ order := rng.Perm(len(p.cells))256+ perm := make(map[int]int, len(p.cells))257+ for i, c := range p.cells {258+ perm[c] = p.cells[order[i]]259+ }260+ var blanks []int261+ for _, i := range p.cells {262+ if cells[i] == rules.Empty {263+ blanks = append(blanks, i)264+ }265+ }266+ rng.Shuffle(len(blanks), func(a, b int) { blanks[a], blanks[b] = blanks[b], blanks[a] })267+ seeds := len(blanks) / 8268+ for ; seeds >= 0; seeds /= 2 {269+ trial := append([]rules.Cell(nil), cells...)270+ for _, i := range blanks[:seeds] {271+ trial[i] = rules.Cell(rng.IntN(2))272+ }273+ shuffle := rand.New(rand.NewPCG(rng.Uint64(), rng.Uint64()))274+ s := p.solverFor(trial, nil, perm, shuffle)275+ if solve(s) == solver.Sat {276+ return p.model(s, perm), true277+ }278+ if seeds == 0 {279+ return nil, false280+ }281+ }282+ return nil, false283+}284+285+// Enumerate returns up to limit solutions of the partial shape under the286+// mask, by blocking each model found. exhausted is true when fewer than287+// limit exist (every solution was returned).288+func Enumerate(cells []rules.Cell, sh rules.Shape, mask rules.Mask, limit int) (sols [][]rules.Cell, exhausted bool) {289+ p := problemFor(sh, mask)290+ var blocks []solver.PBConstr291+ for len(sols) < limit {292+ s := p.solverFor(cells, blocks, nil, nil)293+ if solve(s) != solver.Sat {294+ return sols, true295+ }296+ m := p.model(s, nil)297+ sols = append(sols, m)298+ lits := make([]int, 0, len(p.cells))299+ for _, i := range p.cells {300+ if cells[i] != rules.Empty {301+ continue302+ }303+ if m[i] == 1 {304+ lits = append(lits, -(i + 1))305+ } else {306+ lits = append(lits, i+1)307+ }308+ }309+ if len(lits) == 0 {310+ return sols, true311+ }312+ blocks = append(blocks, solver.PropClause(lits...))313+ }314+ return sols, false315+}316+317+// Count is Enumerate without keeping the models.318+func Count(cells []rules.Cell, sh rules.Shape, mask rules.Mask, limit int) (count int, exhausted bool) {319+ sols, ex := Enumerate(cells, sh, mask, limit)320+ return len(sols), ex321+}322+323+// CompleteRegion completes the target shape jointly with the other shapes324+// over one board (row-major, width W): every shape's rules hold at once on325+// the shared cells, so the target's completion is one that leaves its326+// neighbours a completion too (and its neighbours' completions compatible327+// with each other, which per-shape forward checking cannot see). Only the328+// target's local W*H cells are returned (Empty outside it); the neighbours329+// stay unassigned on the board. rng varies the target's completion as in330+// Complete.331+func CompleteRegion(board []rules.Cell, W int, others []rules.Shape, target rules.Shape, rng *rand.Rand) (sol []rules.Cell, ok bool) {332+ all := append([]rules.Shape{target}, others...)333+ var cs []solver.PBConstr334+ next := len(board) + 1335+ for _, sh := range all {336+ x := func(local int) int { return (sh.Y0+local/sh.W)*W + sh.X0 + local%sh.W + 1 }337+ next, cs = lineConstraints(sh.Lines(), x, rules.All, next, cs)338+ for i, ok := range sh.Mask() {339+ if !ok {340+ continue341+ }342+ if v := board[x(i)-1]; v != rules.Empty {343+ lit := x(i)344+ if v == 0 {345+ lit = -lit346+ }347+ cs = append(cs, solver.PropClause(lit))348+ }349+ }350+ }351+ // randomise the target: relabel its cell variables by a permutation and352+ // shuffle the constraints, then seed a few of its blanks353+ tx := func(local int) int { return (target.Y0+local/target.W)*W + target.X0 + local%target.W + 1 }354+ var tcells []int // local indexes of the target's cells355+ for i, ok := range target.Mask() {356+ if ok {357+ tcells = append(tcells, i)358+ }359+ }360+ order := rng.Perm(len(tcells))361+ relabel := map[int]int{}362+ for i, c := range tcells {363+ relabel[tx(c)] = tx(tcells[order[i]])364+ }365+ for ci := range cs {366+ for li, l := range cs[ci].Lits {367+ v := l368+ if v < 0 {369+ v = -v370+ }371+ if r, ok := relabel[v]; ok {372+ if l < 0 {373+ r = -r374+ }375+ cs[ci].Lits[li] = r376+ }377+ }378+ }379+ rng.Shuffle(len(cs), func(a, b int) { cs[a], cs[b] = cs[b], cs[a] })380+ var blanks []int381+ for _, c := range tcells {382+ if board[tx(c)-1] == rules.Empty {383+ blanks = append(blanks, c)384+ }385+ }386+ rng.Shuffle(len(blanks), func(a, b int) { blanks[a], blanks[b] = blanks[b], blanks[a] })387+ extract := func(s *solver.Solver) []rules.Cell {388+ m := s.Model()389+ out := make([]rules.Cell, target.W*target.H)390+ for i := range out {391+ out[i] = rules.Empty392+ }393+ for _, c := range tcells {394+ out[c] = 0395+ if v := relabel[tx(c)] - 1; v < len(m) && m[v] {396+ out[c] = 1397+ }398+ }399+ return out400+ }401+ seeds := len(blanks) / 8402+ for ; seeds >= 0; seeds /= 2 {403+ trial := make([]solver.PBConstr, 0, len(cs)+seeds)404+ trial = append(trial, cs...)405+ for _, c := range blanks[:seeds] {406+ lit := relabel[tx(c)]407+ if rng.IntN(2) == 0 {408+ lit = -lit409+ }410+ trial = append(trial, solver.PropClause(lit))411+ }412+ s := solver.New(solver.ParsePBConstrs(copyConstrs(trial)))413+ if solve(s) == solver.Sat {414+ return extract(s), true415+ }416+ if seeds == 0 {417+ return nil, false418+ }419+ }420+ return nil, false421+}422+423+func copyConstrs(cs []solver.PBConstr) []solver.PBConstr {424+ out := make([]solver.PBConstr, len(cs))425+ for i, c := range cs {426+ out[i] = solver.PBConstr{Lits: append([]int(nil), c.Lits...), AtLeast: c.AtLeast}427+ if c.Weights != nil {428+ out[i].Weights = append([]int(nil), c.Weights...)429+ }430+ }431+ return out432+}@@ -0,0 +1,239 @@
1+package sat2+3+import (4+ "math/rand/v2"5+ "testing"6+ "time"7+8+ "mosaic-engine/rules"9+)10+11+func 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+}18+19+func sq(n int) rules.Shape { return rules.Square(0, 0, n) }20+21+// tee is an 8-wide, 6-tall crossbar over a 4x2 stem (56 cells; valid22+// under the pigeonhole bound)23+func tee() rules.Shape {24+ return rules.Shape{W: 8, H: 8, Rects: [][4]int{{0, 0, 8, 6}, {2, 6, 4, 2}}}25+}26+27+func 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+}51+52+func 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+}84+85+func 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+}104+105+func 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+}139+140+func 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+}155+156+func 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+}189+190+func 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+}