The nine wasted G=200 attempts fell into four classes; each now has a local escalation: a fill that thrashes on backjumps is redrawn with a new salt inside the attempt (cap 3*tiles, up to 4 redraws) and the joint completion looks two hops out; a repair whose givens fail over every draw redraws the tile's interior before giving up; the technique policy keys on a tile's free cells (a 160-cell tile with 60 shared cells is a 100-cell puzzle), so heavily shared tiles are not asked for a bifurcation they cannot have; and layout-class failures (no pinning flip on a tiny overlap, shared cells that leave nothing ambiguous) re-pack with a salted layout instead of re-attempting the same one. The assertion checker derives free cells from the manifest geometry.
- commit
- ae9363b17fb829e1983bea5c234b754c9cec2a9f
- parent
- 2e2f8d4786e02b1b653eb8721311383aac527333
- author
- dami <gazey55@gmail.com>
| M | engine/ | 188 | +++++++++++++++++++++++++----- |
| M | engine/ | 15 | ++ |
| M | engine/ | 13 | +- |
@@ -18,6 +18,7 @@ import (
1818 "os"1919 "runtime"2020 "sort"21+ "strings"2122 "sync"2223 "time"2324 @@ -171,6 +172,25 @@ type Ladder struct {
171172 Complete bool `json:"complete"`172173 }173174 175+// errBackjumps: the fill phase thrashed; the attempt redraws it with a new176+// salt (maxFillRetries times) before giving up.177+var errBackjumps = errors.New("too many backjumps")178+179+const maxFillRetries = 4180+181+// errLayout: the failure is a property of the layout; Generate re-packs182+// with a new salt instead of attempting the same layout again.183+var errLayout = errors.New("layout")184+185+func isLayoutClass(err error) bool {186+ msg := err.Error()187+ return strings.Contains(msg, "differs inside no overlap region") ||188+ strings.Contains(msg, "falls to propagation alone") ||189+ strings.Contains(msg, "shared cells stay ambiguous")190+}191+192+const maxPackSalts = 3193+174194 // maxRepairRounds bounds the coupled-uniqueness repair loop; each round175195 // costs a makeGivens, so 3*tiles at G=200 was effectively unbounded.176196 const maxRepairRounds = 60@@ -185,6 +205,7 @@ type Stats struct {
185205 Waves int `json:"waves"`186206 WaveRetries int `json:"wave_retries"` // tiles whose givens needed a fresh draw within the attempt187207 Redraws int `json:"redraws"` // stuck tiles whose interior solution was redrawn in repair208+ FillRetries int `json:"fill_retries"` // fill phases redrawn after thrashing on backjumps188209 // phase timings of the successful attempt (wall clock) and of the189210 // attempts wasted before it190211 FillMs int64 `json:"fill_ms"`@@ -296,33 +317,45 @@ func Generate(ctx context.Context, p Params) (*Output, error) {
296317 return sat.Feasible(sh.Local(ctxBoard, p.G), sh, rules.All)297318 }298319 }299- L, err := pack.Pack(pp)300- if err != nil {301- return nil, err302- }303- // every tile must be able to carry the rules on its own before any304- // search starts (an infeasible shape costs SAT seconds to refute)305- for _, t := range L.All() {306- sh := rules.Shape{X0: t.X0, Y0: t.Y0, W: t.W, H: t.H, Rects: t.Rects}307- if err := sh.Valid(); err != nil {308- return nil, fmt.Errorf("layout tile %d (%dx%d at %d,%d): %w", t.ID, t.W, t.H, t.X0, t.Y0, err)309- }310- }311- // and every new tile must have a neighbour able to pin it: an overlap312- // of at least MinLine cells. Without one, "an alternative differs313- // inside an overlap region" is unsatisfiable and every attempt would314- // fail; better to refuse the layout now than after twenty attempts.315- for i, t := range L.Tiles {316- pinnable := false317- for _, o := range L.Overlaps[i] {318- if o.Cells >= pack.MinLine {319- pinnable = true320- break320+ packLayout := func(salt int) (*pack.Layout, error) {321+ pp.Salt = ""322+ if salt > 0 {323+ pp.Salt = fmt.Sprint("gen-salt", salt)324+ }325+ L, err := pack.Pack(pp)326+ if err != nil {327+ return nil, err328+ }329+ // every tile must be able to carry the rules on its own before any330+ // search starts (an infeasible shape costs SAT seconds to refute)331+ for _, t := range L.All() {332+ sh := rules.Shape{X0: t.X0, Y0: t.Y0, W: t.W, H: t.H, Rects: t.Rects}333+ if err := sh.Valid(); err != nil {334+ return nil, fmt.Errorf("layout tile %d (%dx%d at %d,%d): %w", t.ID, t.W, t.H, t.X0, t.Y0, err)321335 }322336 }323- if !pinnable {324- return nil, fmt.Errorf("layout tile %d (%dx%d at %d,%d): no overlap of at least %d cells, no neighbour can pin it", t.ID, t.W, t.H, t.X0, t.Y0, pack.MinLine)337+ // and every new tile must have a neighbour able to pin it: an338+ // overlap of at least MinLine cells. Without one, "an alternative339+ // differs inside an overlap region" is unsatisfiable and every340+ // attempt would fail; better to refuse the layout now341+ for i, t := range L.Tiles {342+ pinnable := false343+ for _, o := range L.Overlaps[i] {344+ if o.Cells >= pack.MinLine {345+ pinnable = true346+ break347+ }348+ }349+ if !pinnable {350+ return nil, fmt.Errorf("layout tile %d (%dx%d at %d,%d): no overlap of at least %d cells, no neighbour can pin it", t.ID, t.W, t.H, t.X0, t.Y0, pack.MinLine)351+ }325352 }353+ return L, nil354+ }355+ packSalt := 0356+ L, err := packLayout(packSalt)357+ if err != nil {358+ return nil, err326359 }327360 start := time.Now()328361 satCalls0, satNs0 := sat.Counters()@@ -357,6 +390,18 @@ func Generate(ctx context.Context, p Params) (*Output, error) {
357390 // the layout, not the draw, is at fault: attempts cannot help358391 return nil, fmt.Errorf("layout against the fixed context: %w", err)359392 }393+ if errors.Is(err, errLayout) {394+ if packSalt >= maxPackSalts {395+ return nil, fmt.Errorf("no layout after %d packings: %w", packSalt+1, err)396+ }397+ packSalt++398+ if Verbose {399+ fmt.Fprintf(os.Stderr, "gen: layout-class failure; re-packing with salt %d\n", packSalt)400+ }401+ if L, err = packLayout(packSalt); err != nil {402+ return nil, err403+ }404+ }360405 }361406 return nil, fmt.Errorf("no mosaic after %d attempts: %w", p.MaxAttempts, last)362407 }@@ -569,9 +614,26 @@ func generateAttempt(ctx context.Context, p Params, L *pack.Layout, attempt int)
569614 // (fillOrder) with backjumping (fillSolution).570615 total := len(m.geom) // emitted tiles plus fixed context571616 tFill := time.Now()572- if err := m.fillSolution(ctx, tag); err != nil {573- return nil, err617+ // a fill that thrashes on backjumps is redrawn with a new salt inside618+ // the attempt: the fill is seconds when it works, and nothing of the619+ // attempt exists yet to lose620+ fillRetries := 0621+ for {622+ err := m.fillSolution(ctx, tag)623+ if err == nil {624+ break625+ }626+ if !errors.Is(err, errBackjumps) || fillRetries >= maxFillRetries || ctx.Err() != nil {627+ return nil, err628+ }629+ fillRetries++630+ tag = fmt.Sprintf("%s|f%d", tag, fillRetries)631+ if Verbose {632+ fmt.Fprintf(os.Stderr, "gen: fill thrashed; redrawing with salt %d\n", fillRetries)633+ }634+ m = newMosaic(p, L)574635 }636+ m.stats.FillRetries = fillRetries575637 m.stats.FillMs = time.Since(tFill).Milliseconds()576638 tGivens := time.Now()577639 // Phase B: givens, in waves over the fixed solution. A tile is ready when@@ -638,7 +700,15 @@ func generateAttempt(ctx context.Context, p Params, L *pack.Layout, attempt int)
638700 for k, i := range idx {639701 if errs[k] != nil {640702 g := m.geom[i]641- return nil, fmt.Errorf("tile %d (%dx%d, %d cells at %d,%d): %w", g.pubID, g.W, g.H, g.cells, g.sh.X0, g.sh.Y0, errs[k])703+ err := errs[k]704+ if isLayoutClass(err) {705+ // every refill and retry failed on a property of the706+ // tile's geometry (its overlaps admit no pinning flip,707+ // or its shared cells leave nothing to bifurcate on):708+ // another draw of the same layout cannot help709+ err = fmt.Errorf("%w: %v", errLayout, err)710+ }711+ return nil, fmt.Errorf("tile %d (%dx%d, %d cells at %d,%d): %w", g.pubID, g.W, g.H, g.cells, g.sh.X0, g.sh.Y0, err)642712 }643713 tiles[i] = results[k]644714 m.commitGivens(results[k])@@ -678,6 +748,23 @@ func generateAttempt(ctx context.Context, p Params, L *pack.Layout, attempt int)
678748 break679749 }680750 }751+ if err != nil && ctx.Err() == nil {752+ // no choice of givens over this solution works: redraw the753+ // tile's interior (neighbours keep their shared cells) and try754+ // the givens again over the new solution755+ m.clearInterior(bad)756+ if ok, ferr := m.fillTile(ctx, fmt.Sprintf("%s|rr%d", tag, round), bad, 300+round); ferr != nil {757+ return ferr758+ } else if ok {759+ m.stats.Redraws++760+ for wr := 0; wr < waveRetries; wr++ {761+ tw, err = m.makeGivens(ctx, fmt.Sprintf("%s|rr%d|%d", tag, round, wr), bad, 100+round)762+ if err == nil || ctx.Err() != nil {763+ break764+ }765+ }766+ }767+ }681768 if err != nil {682769 return fmt.Errorf("repair tile %d: %w", m.geom[bad].pubID, err)683770 }@@ -918,8 +1005,8 @@ func (m *mosaic) fillSolution(ctx context.Context, tag string) error {
9181005 }9191006 backjumps++9201007 m.bump(&m.stats.Backjumps)921- if backjumps > 6*total {922- return errors.New("too many backjumps")1008+ if backjumps > 3*total {1009+ return errBackjumps9231010 }9241011 g := m.geom[i]9251012 // the conflict set: every redrawable earlier tile that fixes a cell@@ -1081,6 +1168,17 @@ func (m *mosaic) clearTile(i int) {
10811168 }10821169 }10831170 1171+// free counts the tile's cells no other tile shares.1172+func (g *tileGeom) free() int {1173+ n := 01174+ for li, ok := range g.mask {1175+ if ok && !g.shared[li] {1176+ n++1177+ }1178+ }1179+ return n1180+}1181+10841182 // clearInterior blanks only the cells no other tile owns. Used once every10851183 // tile has a solution (phase B): a redraw must not touch a shared cell,10861184 // because the tiles across it are already filled and may be building their@@ -1108,17 +1206,41 @@ func (m *mosaic) clearInterior(i int) {
11081206 // joint completion exists: a definitive NOFIT, and the caller backjumps.11091207 func (m *mosaic) fillTile(ctx context.Context, tag string, i, refill int) (bool, error) {11101208 g := m.geom[i]1209+ // the joint region: every unfilled neighbour, and every unfilled tile1210+ // that shares a cell with one of them (two hops). One hop keeps the1211+ // neighbours completable; the second keeps the neighbours completable1212+ // together, which is what a later NOFIT usually turns out to be about1213+ inRegion := map[int]bool{}11111214 var later []rules.Shape1215+ add := func(j int) {1216+ if j != i && !inRegion[j] && m.geom[j].rank > g.rank {1217+ inRegion[j] = true1218+ later = append(later, m.geom[j].sh)1219+ }1220+ }1221+ var hop1 []int11121222 for _, o := range m.geom {11131223 if o.rank > g.rank {11141224 for _, d := range o.deps {11151225 if d == i {1116- later = append(later, o.sh)1226+ hop1 = append(hop1, o.id)1227+ add(o.id)11171228 break11181229 }11191230 }11201231 }11211232 }1233+ for _, j := range hop1 {1234+ gj := m.geom[j]1235+ for li, ok := range gj.mask {1236+ if !ok {1237+ continue1238+ }1239+ for _, o := range m.owners[gj.gid(m, li)] {1240+ add(o)1241+ }1242+ }1243+ }11221244 const tries = 16 // only band collisions need a second draw11231245 var collided []rules.Cell11241246 for t := 0; t < tries; t++ {@@ -1599,6 +1721,12 @@ func (m *mosaic) removeClues(ctx context.Context, rng *rand.Rand, ti int, S [][]
15991721 count := func(lim int) int { return countPT(puzzle, g.sh, lim) }16001722 rng.Shuffle(len(removable), func(a, b int) { removable[a], removable[b] = removable[b], removable[a] })16011723 pol := PolicyFor(g.cells)1724+ // the technique checks (needs a bifurcation, needs uniqueness) are1725+ // about the work left inside the tile once its neighbours have fixed1726+ // the shared cells, so they key on the free cells, not the total: a1727+ // 160-cell tile with 60 shared cells is a 100-cell puzzle1728+ tech := PolicyFor(g.free())1729+ pol.NeedsUnique, pol.NeedsBifurcation = tech.NeedsUnique, tech.NeedsBifurcation16021730 target := int(pol.BlankMax * float64(g.cells))16031731 for _, i := range removable {16041732 if blanks >= target {@@ -163,6 +163,21 @@ func checkAssertions(t *testing.T, o *Output) {
163163 cells[(gy-tp.Y0)*tp.W+gx-tp.X0] = rules.Cell(g[1])164164 }165165 pol := PolicyFor(tp.Cells)166+ // the technique checks key on the tile's free cells (no other167+ // owner), recomputed here from the manifest's geometry168+ free := 0169+ for ly := 0; ly < tp.H; ly++ {170+ for lx := 0; lx < tp.W; lx++ {171+ if !sh.Contains(tp.X0+lx, tp.Y0+ly) {172+ continue173+ }174+ if len(owners[(tp.Y0+ly)*G+tp.X0+lx]) == 1 {175+ free++176+ }177+ }178+ }179+ tech := PolicyFor(free)180+ pol.NeedsUnique, pol.NeedsBifurcation = tech.NeedsUnique, tech.NeedsBifurcation166181 blank := 1 - float64(len(priv.Givens))/float64(tp.Cells)167182 if blank < pol.BlankMin {168183 t.Fatalf("tile %d (%d cells): %.0f%% blank", i, tp.Cells, blank*100)@@ -45,8 +45,9 @@ func MByN(n int) int { return MFor(n * n) }
4545 4646 type Params struct {4747 Seed string `json:"seed"`48- G int `json:"G"` // cells per side of the field49- Kind string `json:"kind"` // scatter | grid | big-first | bands48+ Salt string `json:"salt,omitempty"` // extra rng salt (gen re-packs a layout that cannot be given)49+ G int `json:"G"` // cells per side of the field50+ Kind string `json:"kind"` // scatter | grid | big-first | bands5051 // grid: every tile the same size5152 N int `json:"n,omitempty"`5253 // big-first: fraction of pitch-space area to cover with large squares@@ -582,7 +583,11 @@ func Pack(p Params) (*Layout, error) {
582583 if p.G < MinN {583584 return nil, fmt.Errorf("G must be at least %d", MinN)584585 }585- rng := rngFor("pack", p.Seed, p.Kind, fmt.Sprint(p.G))586+ parts := []string{"pack", p.Seed, p.Kind, fmt.Sprint(p.G)}587+ if p.Salt != "" {588+ parts = append(parts, p.Salt)589+ }590+ rng := rngFor(parts...)586591 L := &Layout{G: p.G, Kind: p.Kind, Region: p.Region, Fixed: p.Fixed, IDBase: p.IDBase}587592 if p.Kind != "scatter" && (p.Region != [4]int{} || len(p.Fixed) > 0 || p.IDBase != 0) {588593 return nil, fmt.Errorf("chunk mode (region, fixed, id_base) is scatter only")@@ -595,7 +600,7 @@ func Pack(p Params) (*Layout, error) {
595600 for salt := 0; salt < 8; salt++ {596601 r := rng597602 if salt > 0 {598- r = rngFor("pack", p.Seed, p.Kind, fmt.Sprint(p.G), fmt.Sprint("salt", salt))603+ r = rngFor(append(append([]string(nil), parts...), fmt.Sprint("salt", salt))...)599604 }600605 L = &Layout{G: p.G, Kind: p.Kind, Region: p.Region, Fixed: p.Fixed, IDBase: p.IDBase}601606 if err = scatter(L, p, r); err == nil {