optional · interactive figures

Explore: backjumping and completeness

The running example replayed frame by frame, the variable order and the termination measure on four instances, a jump rule that is only right when the search follows the input order, backjumping inside branch and bound, and restarts run by run.

optional: nothing in the unit depends on itback to the slides

19b · explore

The running example, frame by frame

Try: step CBJ to step 8, where it jumps from c straight back to a; then pick the chronological run, which enters the two b = 2 subtrees CBJ never does. Static versions: thrashing, the backjump rule.

What it shows. Top: the search tree of the running example that chronological search visits, one box per value tried; a box turns solid when this run touches it, red when a constraint rejects the value, grey when a backjump closes it. A dashed arrow is a jump. Bottom: the stack, one row per frame: the variable, its values (struck through when closed, outlined when current, red when this step closed it), and its conflict set. The deepest frame is shaded, red when every value is closed.

CBJ (17 steps): at step 7 the frame of d is exhausted with E = {a, c} and jumps to c; at step 8 the frame of c is exhausted with E = {a} and jumps to a, skipping b. It ends at step 17 with every value of a closed and E empty. The two b = 2 subtrees stay dashed.
Chronological (33 steps): the same until step 8, where it goes back to b; it then repeats the c, d failure under b = 2, for a = 1 and again for a = 2.

Data. slides/viz/traces/u19b.py, data()["cbj-replay"]: the reference engine solve() on running_example() with the static order, in modes "chrono" and "cbj", with a full stack snapshot after every step. The tree is the set of nodes the chronological run touches; the recording asserts that CBJ touches none outside it.

19b · explore

The variable at each depth, and the measure

Try: Mycielski with dom, past step 29, where depth 5 gets a new variable; watch the measure drop while the digits below a jump go back up. Static versions: the measure, the contract, ordering, measured.

What it shows. One recorded run, chosen by instance, variable order and search. Each row is a depth: the variable of its frame (blue and boxed when the order put a different variable there than the last time this depth was occupied), its digit of the measure (the values not yet closed, or the radix minus one when the depth has no frame), its values, and every variable that has sat at this depth so far. Below: the measure after each step, and how much each step lowered it on a log scale, since a jump high up lowers it by far more than a rejection deep down; jumps are the blue bars, and the stop has none. The figure opens on CBJ. Every bar is above zero: the measure falls at every step, whichever order chose the variables.

Under the static orders every depth keeps one variable. Under dom, dom/deg and dom/wdeg the variable at a depth changes between branches: on the Mycielski graph from step 29 (dom) or step 16 (dom/deg, dom/wdeg), on the random CSP from step 7 (dom) or 10, on the pigeons only under dom/wdeg, from step 82. The panel says when two choices give the same run step for step, as on the pigeons, where every CBJ jump goes to the frame just above, exactly as chronological search does.

Data. slides/viz/traces/u19b.py, data()["ordering"]: the reference engine on the four instances of the heuristic table, with each of the five orders, chronological and CBJ. Each run is stored as one token per step and replayed in the page into the stack; the recording checks the replay against the engine's snapshots and digits, and the page checks that it ends at the recorded stack and measure. Runs are cut at the first 120 steps (the panel says so); the full counts come from the same runs.

19b · explore

The jump-target pitfall, replayed

Try: step to step 10, where the two rules pick different frames, then to step 11, where the index rule answers UNSAT; the stack rule goes on to a solution at step 30. Static versions: the pitfall, the correction.

What it shows. Trial 291 of the pitfall generator, the first instance on which the index rule with silent dropping answers wrongly, solved twice with the same random dynamic order (seed 291). Left: the correct rule, jump to the deepest frame whose variable is in E. Right: the rule written for a search in the input order, jump to the variable of E with the largest input index. Up to step 9 no frame is exhausted and the runs are identical. At step 10 the frame of v1 is exhausted with E = {v0, v3}; the order placed v3 at depth 1 and v0 at depth 2. The index rule jumps to v3, discards v0's frame, and leaves v3's conflict set naming v0, which is no longer on the stack (marked red): the invariant is broken. At step 11 v3 is exhausted; dropping v0 empties E and the run answers UNSAT. The stack rule finds a solution at step 30.

Data. slides/viz/traces/u19b.py, data()["pitfall"]: the reference engine through pitfall_replay(291), with jump_rule="stack" and with jump_rule="index", drop=True, a full snapshot per step. The red marks are the invariant's breaches found in each recorded snapshot; the recording asserts that the stack rule has none, and that the first breach is the step where the traces diverge. The solution is checked against every constraint, and brute force agrees.

19b · explore

Optimization, frame by frame

Try: step CBJ to step 4, the first solution, and step 5, the jump back to a; in the chronological run, the bound rejects a value at steps 8 and 17. Static version: the example.

What it shows. The same figure as the running example, on the optimization example: a, b, c in {1, 2}, a ≠ c, minimise f = a + 2c, static order a, b, c. A green box is a solution; the panel shows U, the cost of the incumbent (∞ before the first one). A solution does not stop the search: it sets U and closes its value, with the other variable of f, a, as the reason. A red box is a value rejected by a constraint or, once U is set, by the bound f < U.

CBJ (11 steps): the first solution, a = 1, c = 2, cost 5, at step 4; c is then exhausted with E = {a} and the jump at step 5 skips b. Under a = 2 the solution at step 8 costs 4; step 11 ends with every value of a closed and E empty: cost 4 is optimal.
Chronological (21 steps): after step 4 it goes back to b and tries b = 2, where the bound rejects c = 2 (step 8); under a = 2 it rejects c = 1 the same way (step 17). Both runs find the same two incumbents.

Data. slides/viz/traces/u19b.py, data()["opt-replay"]: the reference engine solve() on opt_example(), in modes "chrono" and "cbj", with the invariant checked after every step. The printout of uv run python -m slides.viz.traces.u19b checks the optimum against brute force.

19b · explore

Restarts, run by run

Try: step through run 1 and watch it open b after a; then pick run 4, where the weights have moved c there, and run 7, the first with room to finish. Static version: restarts.

What it shows. The restarts slide's example, a triangle a, c, d plus a ≠ b and b ≠ e, all in {1, 2}, under CBJ with dom/wdeg, the weights kept from run to run, and Luby cutoffs of 4 steps per unit (4, 4, 8, 4, 4, 8, 16). Pick a run and step through it. Top: every node any of the seven runs touches, keyed by "variable = value", since the variable at a depth changes between runs. Solid: touched by this run so far; outlined: only an earlier run went there; dashed: no run up to this one did. Bottom: the stack, which every run builds from scratch. The panel shows the weights each run starts with.

Runs 1 to 3 open b right after a (every weight is 1, and ties go to the input order). Their rejections raise the weights of a ≠ b, a ≠ c and c ≠ d.
From run 4 the triangle's weights put c after a, and b is never opened again.
Run 7 has a cutoff of 16, and the search needs 15 steps in that order: it answers unsatisfiable.

Data. slides/viz/traces/u19b.py, data()["restart-replay"]: the reference engine on restart_example(), one traced run per restart, with the invariant checked after every step; the answer is checked against brute force.