The last pathological chunk (ring 3 of the daily, 20 min to the cap, deterministically) was a layout that admits no joint completion against its context: pairwise acceptance cannot see three-tile interactions, and the tile-by-tile fill thrashed on it. Boards of at most 48 new tiles are now filled by sat.CompleteAll (every tile at once over the fixed cells, randomised as CompleteRegion), so a NOFIT is a 150 ms verdict on the layout; and a chunk's layout is checked with the same call when packed, re-drawn with a salt (bounded) until it is jointly feasible. The chunk: 20 min -> 1 s. gen.Version is gen-v6 (small boards' solutions change); the 2x2 fixture is regenerated and reproduces.
- commit
- bfa50b5785352a338370c444723d05bb3d95ef43
- parent
- cf97a70a7af112fde2c99b7b761c7c8fbb58d14e
- author
- dami <gazey55@gmail.com>
| M | engine/ | 59 | +++++++++++++++++++- |
| M | engine/ | 90 | ++++++++++++++++++++++++++++++ |
| M | engine/ | 37 | ++++++++++++ |
| M | engine/ | 2 | +- |
@@ -61,7 +61,7 @@ func PolicyFor(cells int) Policy {
6161 var Verbose = os.Getenv("MOSAIC_DEBUG") != ""6262 6363 // Version changes whenever the generator's output for a seed could change.64-const Version = "gen-v5" // v5: manifest v3, shapes and overlap regions64+const Version = "gen-v6" // v6: chunks filled by one joint SAT completion (v5: manifest v3, shapes and overlap regions)6565 6666 type Params struct {6767 Seed string `json:"seed"`@@ -182,6 +182,10 @@ var errBackjumps = errors.New("too many backjumps")
182182 183183 const maxFillRetries = 4184184 185+// jointFillMax: boards with at most this many new tiles are filled by one186+// joint SAT completion (fillSolution); larger ones tile by tile.187+const jointFillMax = 48188+185189 // errLayout: the failure is a property of the layout; Generate re-packs186190 // with a new salt instead of attempting the same layout again.187191 var errLayout = errors.New("layout")@@ -195,6 +199,10 @@ func isLayoutClass(err error) bool {
195199 196200 const maxPackSalts = 3197201 202+// maxLayoutSalts bounds the re-draws of a chunk layout that admits no joint203+// completion against its context (a SAT verdict each, milliseconds).204+const maxLayoutSalts = 12205+198206 // maxRepairRounds bounds the coupled-uniqueness repair loop; each round199207 // costs a makeGivens, so 3*tiles at G=200 was effectively unbounded.200208 const maxRepairRounds = 60@@ -366,11 +374,12 @@ func generate(ctx context.Context, p Params) (*Output, error) {
366374 }367375 pp := pack.Params{Seed: p.Seed + "|" + p.Nonce, G: p.G, Kind: p.Kind, N: p.N, BigArea: p.BigArea, Coverage: p.Coverage, Compound: p.Compound,368376 Region: p.Region, Fixed: fixed, IDBase: p.IDBase}377+ var ctxBoard []rules.Cell369378 if len(fixed) > 0 {370379 // a candidate touching the context must be completable over the371380 // context's cells (a whole line of it can lie inside a fixed tile,372381 // where nothing made that segment balanced); the packer asks373- ctxBoard := make([]rules.Cell, p.G*p.G)382+ ctxBoard = make([]rules.Cell, p.G*p.G)374383 for i := range ctxBoard {375384 ctxBoard[i] = rules.Empty376385 }@@ -439,6 +448,35 @@ func generate(ctx context.Context, p Params) (*Output, error) {
439448 if err != nil {440449 return nil, err441450 }451+ if len(p.Fixed) > 0 && len(L.Tiles) > 0 && len(L.Tiles) <= jointFillMax {452+ // a chunk's layout must admit a joint completion against its453+ // context; pairwise checks at drop time do not guarantee that, and454+ // finding out in the fill costs a whole attempt. One SAT call per455+ // salted re-draw, bounded.456+ feasible := func(L *pack.Layout) bool {457+ shapes := make([]rules.Shape, 0, len(L.Tiles))458+ for _, t := range L.Tiles {459+ shapes = append(shapes, rules.Shape{X0: t.X0, Y0: t.Y0, W: t.W, H: t.H, Rects: t.Rects})460+ }461+ _, ok := sat.CompleteAll(ctxBoard, p.G, shapes, rngFor(p.Seed, p.Nonce, "layout-check"))462+ return ok463+ }464+ for !feasible(L) {465+ if packSalt >= maxLayoutSalts {466+ return nil, fmt.Errorf("no layout with a joint completion against the context after %d packings: %w", packSalt+1, errFixedNoFit)467+ }468+ packSalt++469+ if Verbose {470+ fmt.Fprintf(os.Stderr, "gen: layout admits no joint completion against the context; re-packing with salt %d\n", packSalt)471+ }472+ if L, err = packLayout(packSalt); err != nil {473+ return nil, err474+ }475+ if len(L.Tiles) == 0 {476+ break477+ }478+ }479+ }442480 if len(L.Tiles) == 0 {443481 // a chunk region the context already covers: nothing to generate444482 commit := sha256.Sum256([]byte(p.Seed + "|" + p.Nonce))@@ -1076,6 +1114,23 @@ func generatorHash() string {
10761114 // looping on a refill that cannot help.10771115 func (m *mosaic) fillSolution(ctx context.Context, tag string) error {10781116 total := len(m.geom)1117+ if m.n <= jointFillMax {1118+ // a chunk: one joint completion of every new tile over the context,1119+ // no backjumping. A NOFIT is definitive: the layout admits no1120+ // solution against its context, and the caller re-packs.1121+ shapes := make([]rules.Shape, 0, m.n)1122+ for i := 0; i < m.n; i++ {1123+ shapes = append(shapes, m.geom[i].sh)1124+ }1125+ assign, ok := sat.CompleteAll(m.global.Cells, m.G, shapes, rngFor(tag, "fill-all"))1126+ if !ok {1127+ return fmt.Errorf("layout admits no joint completion: %w", errFixedNoFit)1128+ }1129+ for id, v := range assign {1130+ m.global.Cells[id] = v1131+ }1132+ return nil1133+ }10791134 tries := make([]int, total) // by tile id10801135 fails := make([]int, total) // consecutive NOFITs by tile id10811136 backjumps := 0@@ -443,3 +443,93 @@ func copyConstrs(cs []solver.PBConstr) []solver.PBConstr {
443443 }444444 return out445445 }446+447+// CompleteAll completes every shape at once over the board's fixed cells:448+// one SAT instance over all of them, randomised like CompleteRegion but449+// over every blank cell of every shape. It returns the values of the blank450+// cells (by global id) or ok=false when no joint completion exists, which451+// is definitive: the layout cannot be filled against its context. For a452+// chunk of a few dozen tiles this replaces tile-by-tile filling with453+// backjumping, which can thrash when a late tile's only redrawable454+// neighbours cannot help.455+func CompleteAll(board []rules.Cell, W int, shapes []rules.Shape, rng *rand.Rand) (assign map[int]rules.Cell, ok bool) {456+ var cs []solver.PBConstr457+ next := len(board) + 1458+ var blanks []int // global ids of blank shape cells, deduplicated459+ seen := map[int]bool{}460+ for _, sh := range shapes {461+ x := func(local int) int { return (sh.Y0+local/sh.W)*W + sh.X0 + local%sh.W + 1 }462+ next, cs = lineConstraints(sh.Lines(), x, rules.All, next, cs)463+ for i, ok := range sh.Mask() {464+ if !ok {465+ continue466+ }467+ id := x(i) - 1468+ if v := board[id]; v != rules.Empty {469+ lit := x(i)470+ if v == 0 {471+ lit = -lit472+ }473+ cs = append(cs, solver.PropClause(lit))474+ } else if !seen[id] {475+ seen[id] = true476+ blanks = append(blanks, id)477+ }478+ }479+ }480+ if len(blanks) == 0 {481+ return map[int]rules.Cell{}, true482+ }483+ // relabel the blank cells' variables by a permutation, shuffle the484+ // constraints, seed a few blanks485+ order := rng.Perm(len(blanks))486+ relabel := map[int]int{}487+ for i, id := range blanks {488+ relabel[id+1] = blanks[order[i]] + 1489+ }490+ for ci := range cs {491+ for li, l := range cs[ci].Lits {492+ v := l493+ if v < 0 {494+ v = -v495+ }496+ if r, ok := relabel[v]; ok {497+ if l < 0 {498+ r = -r499+ }500+ cs[ci].Lits[li] = r501+ }502+ }503+ }504+ rng.Shuffle(len(cs), func(a, b int) { cs[a], cs[b] = cs[b], cs[a] })505+ shuffled := append([]int(nil), blanks...)506+ rng.Shuffle(len(shuffled), func(a, b int) { shuffled[a], shuffled[b] = shuffled[b], shuffled[a] })507+ seeds := len(blanks) / 8508+ for ; seeds >= 0; seeds /= 2 {509+ trial := make([]solver.PBConstr, 0, len(cs)+seeds)510+ trial = append(trial, cs...)511+ for _, id := range shuffled[:seeds] {512+ lit := relabel[id+1]513+ if rng.IntN(2) == 0 {514+ lit = -lit515+ }516+ trial = append(trial, solver.PropClause(lit))517+ }518+ s := solver.New(solver.ParsePBConstrs(copyConstrs(trial)))519+ if solve(s) == solver.Sat {520+ m := s.Model()521+ out := make(map[int]rules.Cell, len(blanks))522+ for _, id := range blanks {523+ out[id] = 0524+ if v := relabel[id+1] - 1; v < len(m) && m[v] {525+ out[id] = 1526+ }527+ }528+ return out, true529+ }530+ if seeds == 0 {531+ return nil, false532+ }533+ }534+ return nil, false535+}@@ -349,3 +349,40 @@ func TestCoupledMatchesBacktracking(t *testing.T) {
349349 }350350 }351351 }352+353+// TestCompleteAll: a 2x2 grid of squares completed jointly is a valid354+// coupled board, deterministic per rng, and refuses an impossible context.355+func 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+}@@ -1 +1 @@
1-{"manifest":{"version":3,"id":"3e47144edce6e1c6d8f489a30b2327fd04f0d32e4053e125d6e734cfbdadff75","seed_commit":"3e47144edce6e1c6d8f489a30b2327fd04f0d32e4053e125d6e734cfbdadff75","G":27,"packer":{"kind":"grid","params":{"big_area":0,"compound":0,"coverage":0,"n":14}},"m_by_n":{"10":3,"12":3,"14":3,"16":4,"6":2,"8":2},"rules":{"overlaps":true,"cross_tile":false,"seam_clues":false,"band_unique":false},"seed_tile":0,"tiles":[{"id":0,"x0":0,"y0":0,"w":14,"h":14,"rects":[[0,0,14,14]],"cells":196,"hash":"278721a54ac3ec4df562ecd5f3b7e9cc7c915bb688781fca4632364a65bff742","m":3,"overlaps":[{"with":1,"cells":14},{"with":2,"cells":14},{"with":3,"cells":1}],"pins":[1]},{"id":1,"x0":13,"y0":0,"w":14,"h":14,"rects":[[0,0,14,14]],"cells":196,"hash":"6b9eda012e81d3e638faa3cc001a322b213d20bcd904ad4217f0a25092cbf434","m":3,"overlaps":[{"with":0,"cells":14},{"with":2,"cells":1},{"with":3,"cells":14}],"pins":[0,2]},{"id":2,"x0":0,"y0":13,"w":14,"h":14,"rects":[[0,0,14,14]],"cells":196,"hash":"170acaaf99604d402a410822ba61176423e72f007291c5e443afb1e4b1808727","m":2,"overlaps":[{"with":0,"cells":14},{"with":1,"cells":1},{"with":3,"cells":14}],"pins":[0]},{"id":3,"x0":13,"y0":13,"w":14,"h":14,"rects":[[0,0,14,14]],"cells":196,"hash":"4691921906b455fc8c72c56224d42e1038819ab23f38918d92fb949891e5f5f1","m":3,"overlaps":[{"with":0,"cells":1},{"with":1,"cells":14},{"with":2,"cells":14}],"pins":[2]}],"k":"unmeasured","generator":"feb831a53261e6bc","library":null},"solution":["100101101010010100110110100","011010100100110011001100101","100101011001101011001001011","101011001011001100110011010","010100110100110010110100101","010011010110010101001011001","101100101011001011010101010","100110011001101100101010101","011001100110010011011001010","010011001100110100100110110","101100110011001011001100101","010100110011011010010011010","011011001100100100110110110","101010010101101101101001001","010101100110010100100110110","100100101010110011011001100","101011010101001010010110011","010101001010110101101001100","011010110101001101010110100","100100110110101010011010011","011001001010110110100101100","100110011001011001001010011","011001100101101011010101100","011010011010010100101001011","100110101010010010110110100","100101100101101001001101011","011011011001000110110010011"],"tiles":[{"id":0,"givens":[[1,0],[2,0],[4,0],[6,1],[9,0],[11,0],[12,0],[27,0],[32,0],[54,1],[57,1],[60,0],[61,1],[65,1],[85,1],[86,1],[89,1],[90,0],[91,1],[92,1],[108,0],[110,0],[147,0],[162,1],[164,1],[165,1],[168,1],[172,1],[173,1],[195,0],[196,1],[216,0],[219,0],[224,0],[227,0],[250,0],[253,0],[254,0],[272,1],[274,0],[276,1],[282,0],[297,0],[301,0],[303,1],[304,1],[324,0],[334,0],[335,0]],"blank":0.75,"needs_unique":true,"needs_bifurcation":true,"flip":[62,63,359,360],"ladder":{"used_unique":false,"used_bifurcation":true,"bifurcations":2,"complete":false}},{"id":1,"givens":[[16,0],[21,1],[23,0],[26,0],[41,0],[42,0],[45,0],[47,1],[50,0],[71,1],[79,1],[97,0],[98,0],[107,0],[122,0],[126,1],[149,0],[150,1],[154,0],[156,0],[160,0],[185,1],[188,0],[203,1],[204,1],[206,0],[233,1],[236,1],[237,0],[242,0],[262,0],[265,1],[268,1],[269,0],[286,1],[288,0],[290,1],[293,0],[311,1],[313,1],[319,1],[322,1],[343,1],[345,1],[346,1],[347,0],[348,1],[349,1],[350,0]],"blank":0.75,"needs_unique":true,"needs_bifurcation":true,"flip":[13,14,67,68],"ladder":{"used_unique":false,"used_bifurcation":true,"bifurcations":1,"complete":false}},{"id":2,"givens":[[379,1],[380,0],[382,0],[388,1],[390,0],[409,0],[413,1],[415,1],[416,0],[417,1],[433,0],[437,1],[442,0],[459,0],[460,1],[465,0],[470,0],[487,1],[490,1],[493,1],[494,0],[515,0],[520,1],[521,0],[523,1],[525,1],[550,1],[552,1],[574,1],[576,0],[594,0],[597,0],[605,1],[621,0],[624,0],[625,1],[626,0],[627,0],[629,1],[656,1],[658,1],[660,0],[679,0],[682,0],[686,1],[703,1],[704,1],[711,0],[713,1]],"blank":0.75,"needs_unique":true,"needs_bifurcation":true,"flip":[357,358,384,385],"ladder":{"used_unique":false,"used_bifurcation":true,"bifurcations":2,"complete":false}},{"id":3,"givens":[[392,0],[394,0],[395,0],[398,0],[404,0],[419,0],[422,1],[424,1],[431,0],[448,1],[451,1],[453,1],[454,1],[482,1],[483,1],[485,0],[500,1],[503,1],[505,1],[507,1],[511,0],[512,0],[527,1],[528,0],[531,0],[536,0],[555,1],[556,1],[564,1],[584,1],[585,0],[586,0],[609,0],[610,1],[611,1],[617,1],[618,1],[635,0],[636,1],[643,0],[646,1],[665,0],[669,1],[693,0],[694,0],[696,1],[700,1],[717,1],[719,0]],"blank":0.75,"needs_unique":true,"needs_bifurcation":true,"flip":[499,501,580,582],"ladder":{"used_unique":true,"used_bifurcation":true,"bifurcations":1,"complete":false}}],"stats":{"ms":9757,"attempts":1,"refills":0,"backjumps":0,"regivens":0,"waves":4},"layout":{"tiles":4,"coverage":1,"holes":0,"hole_cells":0,"mean_hole":0,"by_cells":{"129-256":4},"overlaps":6,"mean_overlap":9.666666666666666,"compound":0}}1+{"manifest":{"version":3,"id":"3e47144edce6e1c6d8f489a30b2327fd04f0d32e4053e125d6e734cfbdadff75","seed_commit":"3e47144edce6e1c6d8f489a30b2327fd04f0d32e4053e125d6e734cfbdadff75","G":27,"packer":{"kind":"grid","params":{"big_area":0,"compound":0,"coverage":0,"n":14}},"m_by_n":{"10":3,"12":3,"14":3,"16":4,"6":2,"8":2},"rules":{"overlaps":true,"cross_tile":false,"seam_clues":true,"band_unique":false},"seed_tile":0,"tiles":[{"id":0,"x0":0,"y0":0,"w":14,"h":14,"rects":[[0,0,14,14]],"cells":196,"hash":"eac3d2f1ac703f689faf383270dad4bd58607c27518650b7527ce73f7a4e22b8","m":3,"overlaps":[{"with":1,"cells":14},{"with":2,"cells":14},{"with":3,"cells":1}],"pins":[0,1]},{"id":1,"x0":13,"y0":0,"w":14,"h":14,"rects":[[0,0,14,14]],"cells":196,"hash":"67d62e2ece0609f61b0bf26a0899fbc49d10705bd4f7db5082e0b01b0c5b27c7","m":3,"overlaps":[{"with":0,"cells":14},{"with":2,"cells":1},{"with":3,"cells":14}],"pins":[0]},{"id":2,"x0":0,"y0":13,"w":14,"h":14,"rects":[[0,0,14,14]],"cells":196,"hash":"ce70dbf666d311c9697dae8fdc0389a54ea74ae71b09f97b297ae60c88bbd5ad","m":3,"overlaps":[{"with":0,"cells":14},{"with":1,"cells":1},{"with":3,"cells":14}],"pins":[0,2]},{"id":3,"x0":13,"y0":13,"w":14,"h":14,"rects":[[0,0,14,14]],"cells":196,"hash":"99251ff6252a0206bd86779530fca78835d0c8b8fcd0bad6217e25eadc5dcce9","m":3,"overlaps":[{"with":0,"cells":1},{"with":1,"cells":14},{"with":2,"cells":14}],"pins":[1,2]}],"k":"unmeasured","generator":"73797f83aaaef481","library":null},"solution":["001101101010101101010010011","100100110101010110100110010","011011001001101001101001101","010110011010011010011010010","101101100101000101100101011","110010010110101101001100101","010011011001010010011011010","101100100110010100110100101","011001010110101011001101100","100110101001101100110011010","011010010110010011001010101","101001001011011010100100110","100101101001100101011011001","010010110100110010110101100","101010011010010100100110011","001101101001101011001001011","010010010110110110110010100","110101101001001101101100100","101011011001001001011001011","010100100110110110010110100","001001010110111010101010010","110110101001001001010101101","001010110100110110110100100","101101001011000101001011011","110101100101001001100101011","001010010110110110011010100","110101001011001001001011011"],"tiles":[{"id":0,"givens":[[0,0],[1,0],[3,1],[6,1],[8,1],[12,1],[28,0],[33,1],[38,1],[54,0],[60,0],[65,1],[81,0],[82,1],[86,0],[87,0],[92,0],[93,0],[114,1],[116,0],[118,0],[144,1],[162,0],[164,0],[166,1],[168,0],[170,1],[172,0],[175,1],[194,0],[217,1],[226,1],[249,1],[251,1],[252,0],[255,1],[272,1],[277,1],[297,1],[299,1],[302,1],[304,0],[307,1],[308,1],[325,0],[328,0],[331,0],[333,0],[335,1],[336,1]],"blank":0.7448979591836735,"needs_unique":true,"needs_bifurcation":true,"flip":[201,202,228,229],"ladder":{"used_unique":false,"used_bifurcation":true,"bifurcations":3,"complete":false}},{"id":1,"givens":[[14,1],[15,1],[25,1],[26,1],[46,0],[48,1],[50,0],[52,1],[68,1],[70,0],[72,1],[80,1],[95,1],[97,1],[100,1],[104,0],[105,0],[127,0],[132,0],[134,1],[150,1],[152,1],[155,1],[157,0],[159,1],[160,0],[161,1],[175,1],[182,1],[205,0],[211,0],[214,0],[230,1],[239,1],[257,1],[260,0],[263,0],[266,1],[268,1],[285,0],[292,1],[293,0],[313,1],[316,0],[317,0],[321,1],[338,0],[346,1],[349,0]],"blank":0.75,"needs_unique":true,"needs_bifurcation":true,"flip":[94,98,121,125],"ladder":{"used_unique":false,"used_bifurcation":true,"bifurcations":1,"complete":false}},{"id":2,"givens":[[380,1],[383,0],[385,1],[386,1],[387,0],[389,0],[410,1],[417,1],[433,1],[438,0],[459,1],[460,1],[464,1],[468,0],[470,1],[486,1],[493,1],[517,0],[518,0],[522,1],[523,1],[540,0],[548,0],[570,1],[572,0],[573,1],[605,0],[621,1],[623,1],[624,1],[626,1],[631,1],[633,0],[648,1],[650,0],[651,1],[656,0],[679,1],[680,0],[681,0],[683,0],[685,1],[702,1],[703,1],[706,0],[707,1],[712,1],[713,1],[714,0]],"blank":0.75,"needs_unique":true,"needs_bifurcation":true,"flip":[362,363,659,660],"ladder":{"used_unique":true,"used_bifurcation":true,"bifurcations":4,"complete":false}},{"id":3,"givens":[[395,0],[400,1],[402,0],[419,1],[420,0],[421,1],[430,1],[447,1],[453,0],[458,0],[473,1],[474,1],[478,0],[479,1],[485,0],[502,0],[505,1],[511,1],[512,1],[528,1],[532,1],[533,0],[535,1],[538,0],[539,0],[556,1],[562,1],[563,0],[564,0],[565,1],[566,0],[586,1],[587,0],[592,0],[609,1],[613,1],[618,1],[619,0],[636,1],[639,0],[643,1],[647,1],[671,1],[673,1],[691,1],[693,0],[701,0],[716,1],[720,0]],"blank":0.75,"needs_unique":true,"needs_bifurcation":true,"flip":[607,617,634,644],"ladder":{"used_unique":false,"used_bifurcation":true,"bifurcations":1,"complete":false}}],"stats":{"ms":1064,"attempts":1,"refills":0,"backjumps":0,"regivens":0,"releases":0,"waves":4,"wave_retries":0,"redraws":0,"fill_retries":0,"fill_ms":29,"givens_ms":995,"settle_ms":39,"wasted_ms":0,"wasted":0,"sat_calls":2917,"sat_ms":554,"ladder_ms":129,"remove_ms":8504,"tile_timers":[{"id":0,"cells":196,"fill_ms":0,"givens_ms":245,"rounds":1,"trials":10,"sat_calls":547,"ladder_ms":37,"remove_ms":2130},{"id":1,"cells":196,"fill_ms":0,"givens_ms":238,"rounds":1,"trials":10,"sat_calls":953,"ladder_ms":40,"remove_ms":2034},{"id":2,"cells":196,"fill_ms":0,"givens_ms":257,"rounds":1,"trials":10,"sat_calls":649,"ladder_ms":33,"remove_ms":2221},{"id":3,"cells":196,"fill_ms":0,"givens_ms":253,"rounds":1,"trials":10,"sat_calls":658,"ladder_ms":19,"remove_ms":2119}]},"layout":{"tiles":4,"coverage":1,"holes":0,"hole_cells":0,"mean_hole":0,"by_cells":{"129-256":4},"overlaps":6,"mean_overlap":9.666666666666666,"compound":0}}