clone

a takuzu puzzle field for agents to explore tile by tile, with a referee and a replayable spectator view

engine: per-phase and per-tile timers, SAT call counters

dami committed 7a4c6cc
MOSAIC_DEBUG=1 prints the table. Baseline, idle machine, G=60 scatter
seed a (45 tiles): 34.4 s wall = fill 0.14 s + givens 33.3 s (14 waves)
+ settle/CSP 1.0 s; 108,448 SAT calls (167.7 s inside solve incl. lock
wait, serialised by the mutex); removal loops sum 422 s over parallel
candidates; ladder 36 ms; the heaviest tile (168 cells) 12.2 s over 6
rounds / 60 trials / 5,849 SAT calls. The removal loop is the cost.
commit
7a4c6ccdfe55395bf9a01b8cb8f79770d87a9ab0
parent
1313f8508703d20590d85c178c1aa7305c333d9a
author
dami <gazey55@gmail.com>
2 files changed, +151 -0
Mengine/gen/gen.go133++++++++++++++++++++++++++++++
Mengine/sat/sat.go18++++
M engine/gen/gen.go +133 -0
@@ -179,6 +179,31 @@ type Stats struct {
179179 Regivens int `json:"regivens"`180180 Releases int `json:"releases"` // repairs that took back neighbours' seam clues181181 Waves int `json:"waves"`182+ // phase timings of the successful attempt (wall clock) and of the183+ // attempts wasted before it184+ FillMs int64 `json:"fill_ms"`185+ GivensMs int64 `json:"givens_ms"`186+ SettleMs int64 `json:"settle_ms"`187+ WastedMs int64 `json:"wasted_ms"`188+ Wasted int `json:"wasted"` // attempts that failed189+ SatCalls int64 `json:"sat_calls"`190+ SatMs int64 `json:"sat_ms"` // time inside the SAT solver (serialised)191+ LadderMs int64 `json:"ladder_ms"`192+ RemoveMs int64 `json:"remove_ms"` // clue removal loops, summed over tiles (parallel)193+ TileTimers []TileTimer `json:"tile_timers,omitempty"`194+}195+196+// TileTimer is what one tile cost in the successful attempt.197+type TileTimer struct {198+ ID int `json:"id"`199+ Cells int `json:"cells"`200+ FillMs int64 `json:"fill_ms"`201+ GivensMs int64 `json:"givens_ms"` // buildGivens wall, all rounds and refills202+ Rounds int `json:"rounds"` // makeGivens rounds203+ Trials int `json:"trials"` // removeClues candidates tried204+ SatCalls int `json:"sat_calls"` // counts by this tile's removal loops205+ LadderMs int64 `json:"ladder_ms"`206+ RemoveMs int64 `json:"remove_ms"`182207 }183208 184209 type Output struct {
@@ -278,18 +303,30 @@ func Generate(ctx context.Context, p Params) (*Output, error) {
278303 }279304 }280305 start := time.Now()306+ satCalls0, satNs0 := sat.Counters()281307 var last error308+ wasted := 0309+ var wastedMs int64282310 for attempt := 0; attempt < p.MaxAttempts; attempt++ {311+ t0 := time.Now()283312 out, err := generateAttempt(ctx, p, L, attempt)284313 if err == nil {285314 out.Stats.Attempts = attempt + 1286315 out.Stats.Ms = time.Since(start).Milliseconds()316+ out.Stats.Wasted, out.Stats.WastedMs = wasted, wastedMs317+ c, d := sat.Counters()318+ out.Stats.SatCalls, out.Stats.SatMs = c-satCalls0, (d - satNs0).Milliseconds()287319 out.Layout = L.Report320+ if Verbose {321+ printTimers(out)322+ }288323 return out, nil289324 }290325 if ctx.Err() != nil {291326 return nil, ctx.Err()292327 }328+ wasted++329+ wastedMs += time.Since(t0).Milliseconds()293330 last = err294331 if Verbose {295332 fmt.Fprintf(os.Stderr, "gen: attempt %d failed after %s: %v\n", attempt, time.Since(start).Round(time.Millisecond), err)
@@ -345,6 +382,13 @@ type mosaic struct {
345382 seamOwner map[int]int // which tile index added each seam given346383 used map[int]bool // cells of planted rectangles: never givens347384 mu sync.Mutex385+ timers []TileTimer // per tile index386+}387+388+func (m *mosaic) addTimer(i int, f func(t *TileTimer)) {389+ m.mu.Lock()390+ f(&m.timers[i])391+ m.mu.Unlock()348392 }349393 350394 func newMosaic(p Params, L *pack.Layout) *mosaic {
@@ -415,6 +459,10 @@ func newMosaic(p Params, L *pack.Layout) *mosaic {
415459 }416460 m.geom = append(m.geom, g)417461 }462+ m.timers = make([]TileTimer, len(m.geom))463+ for i, g := range m.geom {464+ m.timers[i] = TileTimer{ID: g.pubID, Cells: g.cells}465+ }418466 m.order = m.fillOrder()419467 for pos, id := range m.order {420468 m.geom[id].rank = pos
@@ -498,9 +546,12 @@ func generateAttempt(ctx context.Context, p Params, L *pack.Layout, attempt int)
498546 // Phase A: the solution, tile by tile in most-constrained-first order499547 // (fillOrder) with backjumping (fillSolution).500548 total := len(m.geom) // emitted tiles plus fixed context549+ tFill := time.Now()501550 if err := m.fillSolution(ctx, tag); err != nil {502551 return nil, err503552 }553+ m.stats.FillMs = time.Since(tFill).Milliseconds()554+ tGivens := time.Now()504555 // Phase B: givens, in waves over the fixed solution. A tile is ready when505556 // every earlier tile (fill order) it shares a cell with is done (seam506557 // givens flow from earlier tiles); tiles in one wave share no cell, so
@@ -563,6 +614,8 @@ func generateAttempt(ctx context.Context, p Params, L *pack.Layout, attempt int)
563614 if err := m.global.Validate(rules.All); err != nil {564615 return nil, fmt.Errorf("solution invalid: %w", err)565616 }617+ m.stats.GivensMs = time.Since(tGivens).Milliseconds()618+ tSettle := time.Now()566619 567620 // Later tiles may have added seam givens on earlier tiles' shared cells:568621 // settle every tile's final givens and solution set, then check the
@@ -665,6 +718,12 @@ func generateAttempt(ctx context.Context, p Params, L *pack.Layout, attempt int)
665718 }666719 }667720 721+ m.stats.SettleMs = time.Since(tSettle).Milliseconds()722+ for _, t := range m.timers[:m.n] {723+ m.stats.LadderMs += t.LadderMs724+ m.stats.RemoveMs += t.RemoveMs725+ }726+ m.stats.TileTimers = append([]TileTimer(nil), m.timers[:m.n]...)668727 if attemptHook != nil {669728 attemptHook(m, tiles)670729 }
@@ -721,6 +780,22 @@ func generateAttempt(ctx context.Context, p Params, L *pack.Layout, attempt int)
721780 return out, nil722781 }723782 783+// printTimers writes the timing table to stderr (MOSAIC_DEBUG=1).784+func printTimers(o *Output) {785+ st := o.Stats786+ fmt.Fprintf(os.Stderr, "gen: %d tiles in %d ms: fill %d ms, givens %d ms (waves %d, remove sum %d ms, ladder sum %d ms), settle+csp %d ms, sat %d calls / %d ms, attempts %d (wasted %d, %d ms), regivens %d, releases %d, backjumps %d\n",787+ len(o.Manifest.Tiles), st.Ms, st.FillMs, st.GivensMs, st.Waves, st.RemoveMs, st.LadderMs, st.SettleMs, st.SatCalls, st.SatMs, st.Attempts, st.Wasted, st.WastedMs, st.Regivens, st.Releases, st.Backjumps)788+ rows := append([]TileTimer(nil), st.TileTimers...)789+ sort.Slice(rows, func(a, b int) bool { return rows[a].GivensMs > rows[b].GivensMs })790+ if len(rows) > 12 {791+ rows = rows[:12]792+ }793+ fmt.Fprintf(os.Stderr, "gen: %6s %5s %7s %8s %6s %6s %6s %8s %8s\n", "tile", "cells", "fill", "givens", "rounds", "trials", "sat", "remove", "ladder")794+ for _, r := range rows {795+ fmt.Fprintf(os.Stderr, "gen: %6d %5d %7d %8d %6d %6d %6d %8d %8d\n", r.ID, r.Cells, r.FillMs, r.GivensMs, r.Rounds, r.Trials, r.SatCalls, r.RemoveMs, r.LadderMs)796+ }797+}798+724799 func generatorHash() string {725800 h := sha256.Sum256([]byte("mosaic-engine/" + Version))726801 return hex.EncodeToString(h[:8])
@@ -743,7 +818,9 @@ func (m *mosaic) fillSolution(ctx context.Context, tag string) error {
743818 return ctx.Err()744819 }745820 i := m.order[pos]821+ t0 := time.Now()746822 ok, err := m.fillTile(ctx, tag, i, tries[i])823+ m.addTimer(i, func(t *TileTimer) { t.FillMs += time.Since(t0).Milliseconds() })747824 if err != nil {748825 return err749826 }
@@ -799,6 +876,40 @@ func (m *mosaic) fillSolution(ctx context.Context, tag string) error {
799876 j := byRank[k]800877 if Verbose {801878 fmt.Fprintf(os.Stderr, "gen: tile %d (%d cells) has no completion; backjump to tile %d (dep %d of %d, try %d)\n", i, g.cells, j, k+1, len(byRank), tries[j])879+ if fails[i] == 20 {880+ // a tile refused twenty times: say what fixes the region881+ fmt.Fprintf(os.Stderr, "gen: diagnose tile %d (%dx%d at %d,%d rank %d): deps %v\n", i, g.W, g.H, g.sh.X0, g.sh.Y0, g.rank, g.deps)882+ report := func(t *tileGeom) {883+ owners := map[int]int{}884+ filled := 0885+ for li, ok := range t.mask {886+ if !ok {887+ continue888+ }889+ id := t.gid(m, li)890+ if m.global.Cells[id] != rules.Empty {891+ filled++892+ for _, o := range m.owners[id] {893+ if o != t.id {894+ owners[o]++895+ }896+ }897+ }898+ }899+ fmt.Fprintf(os.Stderr, "gen: tile %d (%dx%d at %d,%d rank %d fixed %v): %d/%d cells fixed, by owner %v, deps %v\n", t.id, t.W, t.H, t.sh.X0, t.sh.Y0, t.rank, t.fixed, filled, t.cells, owners, t.deps)900+ }901+ report(g)902+ for _, o := range m.geom {903+ if o.rank > g.rank {904+ for _, d := range o.deps {905+ if d == i {906+ report(o)907+ break908+ }909+ }910+ }911+ }912+ }802913 }803914 for p := pos; p >= m.geom[j].rank; p-- {804915 m.clearTile(m.order[p])
@@ -815,6 +926,8 @@ func (m *mosaic) fillSolution(ctx context.Context, tag string) error {
815926 // `fillTry` continues the per-tile fill counter across refills so each816927 // draw is distinct and deterministic.817928 func (m *mosaic) buildGivens(ctx context.Context, tag string, i int) (*tileWork, error) {929+ t0 := time.Now()930+ defer func() { m.addTimer(i, func(t *TileTimer) { t.GivensMs += time.Since(t0).Milliseconds() }) }()818931 var gerr error819932 fillTry := 1 // 0 was used by phase A820933 for refill := 0; refill < 6; refill++ {
@@ -1197,6 +1310,13 @@ func (m *mosaic) makeGivens(ctx context.Context, tag string, i int, round int) (
11971310 }(ci)11981311 }11991312 wg.Wait()1313+ m.addTimer(i, func(t *TileTimer) {1314+ t.Rounds++1315+ t.Trials += limit1316+ for _, r := range results {1317+ t.RemoveMs += r.ms1318+ }1319+ })12001320 var lastErr error12011321 for ci, res := range results {12021322 if Verbose {
@@ -1248,6 +1368,16 @@ func (m *mosaic) removeClues(ctx context.Context, rng *rand.Rand, ti int, S [][]
12481368 W := g.W12491369 M := g.m12501370 gid := func(lx, ly int) int { return g.gid(m, ly*W+lx) }1371+ satCalls := 01372+ defer func() { m.addTimer(ti, func(t *TileTimer) { t.SatCalls += satCalls }) }()1373+ countPT := func(puzzle []rules.Cell, sh rules.Shape, limit int) int {1374+ satCalls++1375+ return countPT(puzzle, sh, limit)1376+ }1377+ solutionsPT := func(puzzle []rules.Cell, sh rules.Shape, limit int) (rules.TileSolutions, bool) {1378+ satCalls++1379+ return solutionsPT(puzzle, sh, limit)1380+ }12511381 protect := map[int]bool{} // local indices never given: planted rectangles12521382 planted := r.R1 >= 012531383 if planted {
@@ -1434,8 +1564,11 @@ func (m *mosaic) removeClues(ctx context.Context, rng *rand.Rand, ti int, S [][]
14341564 pinned[i] = S[i/W][i%W]14351565 }14361566 }1567+ tLadder := time.Now()14371568 rating := rules.Single(g.sh, append([]rules.Cell(nil), pinned...)).Ladder(12)1569+ m.addTimer(ti, func(t *TileTimer) { t.LadderMs += time.Since(tLadder).Milliseconds() })14381570 needsBif := rating.UsedBifurcation1571+ satCalls++14391572 noUnique, _ := sat.Count(pinned, g.sh, rules.Run|rules.Balance, 2)14401573 needsUnique := noUnique >= 214411574 if pol.NeedsBifurcation && !needsBif {
M engine/sat/sat.go +18 -0