What CP-SAT and HiGHS actually do in the whole route

The whole route (awx/whole_route.py, run on a real board by the bus step awx/route_bus.py, on bus622-take5) plans every lane's complete path between two ball grid arrays before it routes anything. That plan is built by two solvers with different jobs. CP-SAT settles discrete questions: who crosses whom, and on which layer. HiGHS then solves a continuous question: how far sideways each lane sits at every point along the way. Between them sits the frame, which turns the board into one road per lane, so both solvers can work along a single coordinate. Most sections below have an interactive toy. The toys use the same ideas and constraint shapes as the code, at toy scale.

The words you will meet

lane

one net's planned path through the bus, from the source BGA to the destination BGA. A differential pair is one lane.

tooth / berth

where a lane escapes at the source (tooth) and arrives at the destination (berth): the end of its escape stub, just outside the array. A surface stub fixes the layer the lane starts or ends on. A stub that ends in a via (a via end) leaves the layer to the solve.

trunk

a straight line from the source array's pad box through the destination's. Lanes that arrive on the destination's facing side end on it.

ring

a road round the destination, outside its pads and the parts hugging it. A lane whose berth is on another side of the destination leaves the trunk and rides a ring to it.

cut

(two meanings) the point where an array's outline is unrolled into one order: the destination's, away from its facing side, where its two rings meet and which decides which way round each lane goes, and the source's, on its far face (the frame); and a "not this combination" rule sent back to CP-SAT after a later stage found a plan that cannot be drawn (the loop).

u

a lane's route coordinate: distance along the trunk from its tooth (or from the end of its lead-in, for a tooth on the source's far side), then along its ring to its berth. Every crossing and layer change is a position in u.

crossing

a pair of lanes whose order is swapped between source and destination. They must pass through each other, so at that point they sit on different layers.

via

a layer change. Vias are what the discrete plan tries to minimise. Every via is a through via.

convex

a region with no dents, holes or separate pieces: every point between two allowed points is allowed too. An LP's region always is, which is why the LP finds the best answer overall and not just the best nearby (section 2).

Watch a whole run

Two films of real runs of the whole route on a two-layer bench (a processor's BGA to a DDR3 memory), made by awx/whole_movie.py in September. Each walks the stages in order: the ends, the frame, the solve, the geometry, the polish, the snap, the audit and the route. The stages are the same today; what has been added since (more than two layers, the escape fanout, the winding cut) is described below. Beside the board the film draws what each solver decides:

• The solve (CP-SAT) is a braid under the board, sharing its x axis. Each strand is a lane, its height is the lane's order, and its colour is its layer. Two strands that cross differ in colour, and a white ring is a via. The search is replayed from the plans CP-SAT really found, in the order it found them, with the bound that proved the last one. On the board above, the lanes swap exactly where the solve put each crossing.
• The geometry (HiGHS LP) is drawn as forces on the board. Every rule that holds a lane where it is has a shadow price in the LP's dual, and the price is how hard it pushes: a neighbour on the same layer, a via's room, a pad, the board edge, a turn limit.

Neither solver is re-implemented for the film. Each is run again under the chain's own settings and watched, and the film is refused unless the re-run writes what the chain wrote, byte for byte.

0   The pipeline, and where the two solvers sit

Click a stage. Dashed arrows are the feedback that makes this a negotiation instead of a one-way pipe. whole_route.py repeats the fanout for up to 3 rounds (--rounds; the bus step in the routing chain runs 2), and within a round its loop repeats solve, geometry, polish and audit for up to 6 rounds (LOOP_ROUNDS).

0a   Ends and fanout: the ends decide the braid (fanout_from_plan.py, whole_ends.py)

Before any solver runs, the fanout decides where every lane leaves the source BGA (its tooth) and where it arrives at the destination (its berth), including which layer it is on at each end. Those choices fix the whole puzzle: the order of teeth around the source and of berths around the destination decides which pairs must cross, and the end layers decide what each crossing costs. That is why the fanout is not a separate chore. whole_ends scores candidate ends by the vias the resulting braid would need (an estimate from the ends alone), and the fanout lays the cheapest, then judges what it actually laid. Crowded ends found later by the audit come back here as feedback.

The ends are chosen from a menu of ways out of each ball. With the escape fanout (route_bus's escape mode) the menu is the human's: every netted ball of both arrays is first dog-boned (a short stub to a via on a diagonal gap point, dogbone_arrays.py), an outer ball with a clear way out is left on the surface, and a lane may then leave its ball's via on any routing layer: half a pitch onto a ball line, a sidestep to a line beside it, or onto an empty street through the array (escape_plan.py). An array an earlier bus already routed through is planned whole each round with the new bus, its other nets and plane balls included (joint_escape.py). The bus step has two other modes. joint also fans out the arrays' other nets and plane balls: the bus is laid round a via site kept free in every other ball, and the rest are planned together round it in one CP-SAT model, plane balls sharing drop vias or strapped to a neighbour. plain fans out the bus alone.

0b   How the ends are searched: exchange moves and random kicks

The real menu is far too big to try every combination, so whole_ends uses a local search. One move changes one lane's tooth or berth to another option. If that option is already taken by one other lane, that lane is ejected to its best free option, and the two changes are scored together (an exchange). A move is taken as soon as it lowers the objective, and it sweeps until no single move helps. That reaches a local optimum, which is not always the best. So it is iterated: a few lanes are kicked to random options, searched again, and the result kept only if better. The kicks use a fixed seed, so every machine gets the same answer.

Why a local search here, when the rest of the pipeline uses CP-SAT and an LP. The search starts from the fanout's own greedy choice of berths (every berth clear of the others), from CP-SAT's joint ends on an escape fanout (below), or on a re-plan from the previous round's, and improves it by the moves above. CP-SAT is still used, but as the final judge rather than the search: the best few ends the search reaches are re-ranked on the exact route (best_exact). The ends are hard to put in one exact model, for three reasons:

• Scoring one choice of ends is itself a solve. What a set of ends really costs is the via count of the route they force, and that is the whole CP-SAT solve of section 1: seconds to tens of seconds for each candidate. A model that chose the ends and the route together would be that solve with every lane's menu of exits added to it. So the search steers by an estimate that takes milliseconds and is exact in its parts: on each layer, the crossings a lane must leave the layer for are a permutation graph, whose least cover is found exactly by a chain.
• Much of what the fanout can lay is a check, not an equation: two exits that conflict, another net's copper between a pair's tips, a move the fanout refused. A search simply skips such a move, where a model would need each one written as a constraint.
• Some terms are not linear: congestion is priced by the square of the overload, and whether a lane's one layer change can serve all of its crossings depends on the order it meets them in.

What it gives up is a proof. CP-SAT proves the fewest vias for the ends it is given, and the LP the best geometry for that plan, but nothing proves the ends themselves are the best. The search stops at a local optimum. The kicks and the exact re-ranking make a poor one less likely, but do not rule it out.

Where CP-SAT does choose the ends. On the escape fanout, before any local search, one CP-SAT model picks every lane's tooth and berth together from the same menus (the joint ends): one choice per lane and end, the same conflicts, and two lanes whose orders differ round the boxes crossing on different layers. It counts the fanout's vias and ten vias a crossing, so it puts crossings first: the local search's objective prices a crossing at a hundredth of a via, and on a dense bus it bought stacks back with crossings the solve could then not place. Whichever ends are chosen are then put to the solve's check: the bench they would make is built in memory and the whole solve (section 1) is run on it under its strict rules. If it finds no plan, the crowded lanes are priced and the ends are searched again (up to four times). The ends model also chooses the cut on the destination's far side, which is where the frame takes over.

0c   The frame: one road per lane, both arrays unrolled (whole_frame.py)

The ends are points round two arrays, but both solvers want each lane to be one road with one coordinate. The frame builds those roads from the board alone.

One lane, worked through. Take a lane whose berth is on the destination's far side, facing away from the source. It leaves its tooth and runs along the trunk, the straight line from the source's pad box to the destination's. In front of the destination it reaches the arrival line (H0). There it leaves the trunk onto the north ring, a road round the destination outside its pads, follows it round the corner and down the far side, and drops into its berth (lane D in the figure below). Its route coordinate u is how far it has come: 32 mm along the trunk, then 23.7 mm along the ring, so u runs from 0 to 55.7. A lane whose berth faces the source never leaves the trunk at all. Every crossing and every via the solve places is a position in u.

Which way round is decided by the cut, one point on the destination's outline away from the facing side. Berths on one side of the cut go round the north, the others round the south. Now unroll the destination: cut its outline there and straighten it into a line. The berths stand in one order, north to south. Two lanes cross exactly when that order and the teeth's disagree.

The source is unrolled too, from a cut on its own far face, but it has no rings. A tooth on its facing face starts on the trunk. A tooth on its north or south face runs along that face and joins the trunk past the corner, and its u counts that run. A tooth on its far face cannot be carried by the trunk at all (the trunk's columns stand across that stretch), so it goes straight out of the face and round the corner on a lead-in: north of the source's cut round the north, south of it round the south, then on as a side face's lane. On each side the lane launched first rides outermost. So the teeth stand in one order too, north to south, and the source's cut decides which way a far-face tooth goes round. Everything the solve needs to know about who crosses whom is in those two lists: moving either cut changes the crossings, and with them the vias. It also changes how far each lane rides round.

Default cuts puts them where the code does without the ends model's say: the destination's at the middle of the widest gap between its far side's berths, the source's at the gap between its far-face teeth with the fewest crossings. In the real run the ends model chooses the destination's cut: it scores the ends at each candidate cut and keeps the best (0a). Crossings are cheap only when the two lanes can be on different layers there, so fewer crossings usually means fewer vias, and a cut that winds lanes round the far side can win even though they ride further. A lane winding round the destination to arrive from the far side is what a human layout often does too.

1   CP-SAT: the discrete plan (whole_solve.py)

Bus lanes leave the source BGA in one order (the launch order: the teeth, unrolled) and must arrive at the destination in another (the berth order: the destination unrolled from the cut, 0c). Every pair that is inverted between the two has to cross, once, at a position in u both lanes share. Two copper lanes cannot cross on the same layer, so at each crossing they are on different layers: on two layers one is on F.Cu and the other on B.Cu. Each layer change costs a via. A lane whose stub ends on the surface starts (or ends) on that layer; a lane whose stub ends in a via may leave it on any layer its run fits on.

The CP-SAT model is exactly that puzzle, for every lane at once: booleans for "which lane is on which layer at this crossing", integers for "where along u the crossing happens" and "where each lane changes layer" (up to three changes a lane), and constraints tying them together. It minimises vias and proves the minimum. Below, an instance of that puzzle with the numbers shrunk to 5 lanes on two layers.

1a   The layer puzzle, and how a solver searches it

1b   Where along u: time-window constraints

Booleans decide who crosses. Integers decide where. Each crossing gets an integer position t in u (on a grid of a fifth of a lane pitch), limited to a window: the stretch where both lanes exist, clear of a pair's end connector, and for two lanes on the same ring short of the earlier one's berth. A lane's crossings along it must be at least a lane pitch apart (less for a lane sweeping steeply across the others). That is the AddNoOverlap constraint on optional intervals in whole_solve.py. Layer changes are positions in u too, with rooms of their own:

• a change keeps a via's room from its own lane's crossings, and a single lane's change keeps a change's room from both its ends (a pair's, its dive room);
• no change in a band along the source's facing side, where the teeth stand and the lanes have not spread yet (on two layers, no crossing there either; a lane allowed to change at its own tooth is not held by it);
• a lane leaving the surface may change layer right at its stub's end only where a via there is measured clear of every other net's copper on every layer;
• two neighbouring lanes' changes are staggered along u, so their vias clear the via-to-via rule;
• no change where the lane's reference passes within a via's reach of another part's pad (the built-in via cuts, on the rings too).

Inside its window, nothing in the objective prices where a crossing or a change stands: every place costs the same once the vias are minimal. So CP-SAT tends to leave them where its search first put them, often at the window's start, just past the teeth, and the geometry and the audits then judge whether there is room there.

1c   What "best" means: a lexicographic objective

The objective is one sum, in vias: W_V·(vias + 5·(each via a net carries past two) + (each run on a plane's layer)) + (history congestion). A net with three vias on the board costs eight, so the solve spreads changes across nets, but this is a price, not a cap. A run on an inner layer that carries a power or ground pour costs one via more, so a lane takes a plane's layer only where it saves a via. The weights are chosen so that each term dominates the next. Fewer vias always beats less congestion, and congestion only breaks ties between plans with equal vias. The congestion term is PathFinder-style history: places where earlier audits found trouble get a price, so the solver steers around them. Last of all, between plans of equal cost, each run's layer is chosen again by the plane it would split (a ground plane's dearer than a power plane's), so a plan and its mirror on the inner layers always come out the same way.

1d   More than two layers (route_layers.py, relayer.py)

ROUTE_LAYERS names the layers the lanes may run on: F.Cu and B.Cu, then any inner layers (F.Cu,B.Cu,In1.Cu,In2.Cu), planes' layers included. On two layers a lane's layer is one bit, flipped by each change. On more, each run between two changes is an integer, its layer, and a change goes to any other layer. Two crossing lanes must be on different layers, which now leaves the solve a choice of which two.

• Via ends. An end whose stub carries a via (a dog-bone, or a via in its pad) can leave on any layer its run from the via to the array's edge fits on, and the solve chooses which. Another net's copper within the rule of the run bans a layer, and two runs within the rule of each other must end on different layers. Before the geometry, the relayer moves each such run onto the layer the solve chose.
• Passive regions. Decoupling caps and other small parts with pads on some layers only, close together, make a region. A lane passing near one pays two vias on each of the region's layers, so the solve puts it on a free layer, and the lanes it keeps there take at most half the room the layer has.
• Part gates. A part whose pads stand on one face is a gate on that layer: the lanes the solve puts on that layer beside it must fit the width left there.
• Cuts on a layer: a lane found against a part, a track of an earlier bus, or a keep-out area on one layer is held off that layer there from the next solve on (section 3).

2   HiGHS: the continuous geometry (whole_geo.py)

CP-SAT has fixed the topology: the order of lanes at every column, where each pair crosses, and each lane's layer, so where along its route each via sits. What is still unknown is real numbers: how far off its frame's spine each lane sits at each column (one column every 4 router grid steps, along the trunk and along both rings). That question is a linear program, one for the whole bus.

The unknown is one number per (lane, column): its sideways offset o[lane][col]. The rows are:

• Pitch (hard): neighbours on the same layer are at least P_MIN apart, plus half a pair's pitch for diff pairs. The real code adds tangent cuts of sqrt(1+k²) so slope is priced correctly.
• Static copper (hard): a lane passes each part (an island) on one side, with clearance, each column measured where its own offset line meets the part's pads. The split below is that choice. Other nets' vias in the field round the arrays (an earlier bus's) are islands too, round discs at the router's ring, and the gap between two of them holds only the lanes that fit it as the board measures it.
• Via rooms, board edge, 45° turn limit a column, slope cap (hard). A pair runs straight for the pair router's straight run either side of each dive.
• Length, bends, and pitch short of comfortable (soft): the price of sideways moves, kinks, and squeezing lanes closer than the comfortable pitch (a track more than the bar), four times as steeply below halfway to the bar.
• Trunk to ring: a ring lane's trunk piece ends on its ring's side of the ring's start, and its ring piece starts at the same offset. Which side of a part a lane passes is decided once on the board, not once per frame, so the trunk and a ring never send one lane round a part on opposite sides.

Every "hard" row is really elastic: it carries a slack variable priced at W_HARD=10⁴. So the LP is always feasible, and if the plan cannot be drawn, the LP does not fail. It pays, and the rows it paid on are reported. Those become cuts for CP-SAT. The LP runs twice: the second pass holds each lane to one side of every island near it, and solves the many tangent rows lazily (only those near binding, then any its answer breaks, until it breaks none).

2b   How an LP is solved: walking the corners, or cutting through the middle

Picture an LP with only two unknowns (x, y) so it fits on a screen. Every row is a straight wall, and together the walls fence in a polygon of allowed answers. The polygon is convex, with no dents, because straight walls cannot make one. The cost is a slope: the polygon is shaded from expensive to cheap. The best answer is always at a corner (or along a whole side, if the slope happens to line up with it). The real LP is the same picture with tens of thousands of unknowns. HiGHS has two ways to find that corner:

• Simplex (highs-ds) starts at a corner and hops to a cheaper neighbouring corner, again and again, until no neighbour is cheaper. Because the polygon is convex, a corner with no cheaper neighbour is the cheapest corner of all. In a region with a dent, it could be a dead end.
• Interior point (highs-ipm) starts in the middle of the polygon. The walls push it back with a force that grows as it gets close (a "barrier"). That push is slowly weakened, so the point drifts toward the cheap corner without ever touching a wall.

whole_geo.lp_by_dual has one further trick: it solves the dual LP. This LP has many more rows than columns, so its dual has a row per column and every slack is a plain inequality. HiGHS's interior point runs it about 6× faster (on a 51-net bench's second pass: 31 s instead of 188 s). The lane offsets come back in the same answer: HiGHS returns a multiplier for every balance equation of the dual, and those multipliers are the offsets. The interior point is capped at 500 iterations (it once ran 2329 on an 18-net bench); past that the dual simplex solves it, and lands on the same point. What that dual is: its prices are the forces that hold each lane where it is, and a rule that pushes must be touching, which is how the forces place the lanes. See Shadow prices as forces.

3   The two solvers negotiate

CP-SAT proves a plan is optimal in vias, but it knows nothing about millimetres. The LP knows the millimetres but can't change topology. When the LP has to pay on a hard row, it says which lane and which place. That becomes a cut (a boolean disjunction) added to the CP-SAT model, and CP-SAT solves again. Audits after the polish and snap do the same and also feed the congestion history. The loop (whole_route.py) runs up to 6 rounds.

• What comes back. From the geometry: an island a lane could not be kept off, a change it could not give its room, a pair's dive it could not lay straight. From the polish: side flips, a lane sent round the other side of a part (back to the geometry, not the solve). From the audits: every finding's place, as history, so a round with no cut still solves again. A lane found against a part on one layer gets a layer cut: held on another layer across that part. Each cut is held to the stretch of the lane's own laid route that met what cut it.
• Soft and firm. A cut is soft, priced at three vias, so a plan breaks it only when holding it would cost more. A cut from another net's track (an earlier bus) or a keep-out area is firm, a hundred vias, because a lane planned across another net's track is a lane that cannot be laid. A firm track cut holds for every lane whose path passes that place, not just the one found there.
• When it stops. Not converging: two rounds in a row that do not beat the best so far (a round with new side flips to try is not counted). Ends crowded: a finding at the ends that stands two rounds running, which only the fanout can move (4c).

4   After the plan: polish, snap, audit, route

The solvers give a plan that is correct on paper. The remaining stages make it something the router can lay, and check it against the router's own rules before a single track is routed.

4a   Polish: meet the audit's numbers exactly (whole_polish.py)

The geometry LP measures in its own frames and linearises slopes, so its lanes come out a few micrometres short of the audit's bars in dozens of places. The polish works on the lanes' real board polylines. Every near-violation becomes a linear constraint on small vertex moves, a small LP finds the least movement that meets them all, and it repeats (re-linearised) until the audit's measures hold. Each bar is the snap's plus a grid step, so every gap the snap later splits holds a grid row. The toy below uses a simple push in place of that LP, but shows the same behaviour: tiny targeted moves, a few rounds, ends pinned.

• No rule broken unseen. A rule is in the LP while it stands within twice the round's move limit of its bar, since two vertices each moving the limit close a gap by twice as much.
• Every round has an answer. A turn already past 90 degrees that cannot be straightened is opened as far as the round allows and the rest paid, so a round never stops dead.
• The best state is kept: the one with the fewest short rules and shape faults any round reached, not the last round's.
• Out of a pad. A lane inside a pad has no nearest edge to be pushed off, so it is pushed out across its own line on the side with less of the way out, its neighbours moving ahead of it. A via inside a pad goes out along its lane or across it.
• Flips. A lane that cannot be held on its side of a part is flipped to the other side, and the geometry runs again before anything is snapped.

4b   Snap: land the line on the router's grid (whole_snap.py)

The router draws only on its grid, in 0°, 45° and 90° segments. The snap takes each lane's smooth line and finds an octilinear path on grid points in a band around it, one lane at a time, with hard clearance to everything already placed. The cost is length + bends + distance from the smooth line. Because the polish left every lane a grid step of room, the snap of one lane never steals the room the next needs.

• The pairs go first, alone, moving as the pair router does: 45-degree turns, a straight run after each, a via only on a straight run. Each pair's end is two short legs from its pads to a pose on the grid where the pair router takes over. A pair whose legs must swap sides (P on one side at its tooth, the other at its berth) swaps them at its first dive with a crossover. The pairs are then held while the polish fits the singles round them.
• Then the singles, each keeping a share of every gap for the lanes not yet placed, so the lanes laid first cannot take the room the later ones need. Two sweeps then lay every lane again against the others' real copper.
• A lane the snap cannot lay is named with where its search got stuck, and the loop sends that place to the solve. Both searches run in the router's Rust core.

4c   Audit, gate and feedback (whole_audit.py, whole_gate.py, whole_lint.py, whole_feedback.py)

The plan is installed in the whole route's own lanes exactly as the router will get it, and the audit runs every one of the router's own checks on it: pitch, dive room, clearance to static copper as KiCad draws the pads, a pair's end connectors and crossover as exact copper, shape, and that every lane's band joins its tooth to its berth. A shortfall of a quarter of the router's grid step or less is a near miss, not a finding: the grid snap moves a lane that near off its bar. The gate passes a plan only when every lane is laid and every check is clean, with nothing waived, and writes every finding's position. The lint checks what the snap promises: grid points, 0/45/90 pieces, a via at every layer change. Where a finding is decides who can fix it:

• Between the arrays: the solve's problem. The place becomes history (a price on the next solve) and a cut.
• At the ends (beside or in front of an array): the solve cannot move it, because it comes from where the teeth and berths stand. whole_feedback names the pair of ends not to choose together again, and the fanout re-chooses. If the same finding stands in two rounds, the loop stops instead of paying for another solve.

Feedback reaches the fanout by four channels: crowded ends from the audits; the nets an unproved plan left over two vias; a fanout that was refused (a pair it split); and, after a round is laid, every net it left open, named at the end where it fails. A named end is priced by place (in full where the lane stands on its layer, half on the other layer, fading over 0.76 mm around it), and its price doubles each later round it is named again. A fanout that lays the same ends again has its feedback raised and runs again.

4d   Route all lanes, each in its band (route_lanes.py)

Finally the production router lays every lane from the audited plan (--plan): pairs first, then the singles, each in the berths' order round the destination, each confined to its own band around the plan and routed against every earlier lane's copper. A pair's end connectors and crossover are laid as planned and the pair router runs between them. A pair refused in its band is tried in a wider one, and free of the plan only last, after every lane has had its band. Then check_connected and check_drc grade the board (a lane reported "routed" is not proof its net connects). The plan is what makes the order unimportant: it already decided which lanes pass which side of an obstacle.

4e   Rounds, and the board handed on (whole_route.py, route_bus.py)

A run hands back the best board it laid, and lays something whenever a plan for some of the lanes exists:

• A loop that does not pass is laid all the same, from the plan it held (its snapped plan, else its best smooth plan snapped with no gate). A lane that cannot be laid stays open. If that lay is not clean, the round lays one other loop round's plan too (the fewest findings first) and keeps the better: DRC first, then open nets, vias and copper.
• The rounds stop at the first clean lay. A round whose plan lays connected and DRC-clean ends the run, whether or not its loop passed or its solve was proved. A later round could only move the ends its audits named, which the lay already went round.
• Otherwise a round that leaves nets open feeds the next fanout (4c), up to the round limit. Every round is graded, and the best (fewest open nets, then fewest vias) is the run's board. When no round laid anything, a last resort plans only part of the lanes, the ones the rounds named left out.

On a real board the bus step (route_bus.py) wraps this. It finds the buses between pairs of ball arrays (or takes them from --bus SRC:DEST[:MODE[:LAYERS]], each with its own fanout mode, joint, escape or plain, and its own routing layers), strips the bus's old copper, fans out, turns the board into the flow frame, runs the whole route and turns the copper back. It then grades the board where it is written: every bus net connected, no DRC violation on a bus net, the whole board no worse than it came. The board's length and skew rules are named but not counted, because the bus is laid untuned. A net left open, or named in a violation, goes back as it came, for the rest of the routing chain. The nets handed on are protected in the board's project and their tracks and vias locked, so the later routing steps route round them and never rip them up. Several buses are routed in turn, each on the board the one before handed on.

5   Side by side

Where else these solvers appear (older braid chain and instruments)

• HiGHS MILP: schedule.exact_pages assigns each net to a page (binary x[i,p], with x[i,p]+x[j,p] ≤ 1 for inverted pairs, minimising swimmers, then page vias). joint_floor.py and synth_bus.cap_floor put a binary layer at each crossing (y_a+y_b=1) and count layer changes. That is the same puzzle as 1a, and an infeasible model there means an odd parity cycle. braid._prime_highs_threads pins it to one thread for determinism.
• CP-SAT: pages_first.py picks each net's destination move, source move and page in one model (a "swimmer" is priced at 100 vias), and synth_bus.cap_sat_feasible / escape_move_floor check feasibility. whole_ends.py uses it on one worker to rank end states exactly, and to choose the joint ends on an escape fanout. joint_escape.py plans a whole array's escapes, straps and plane drops in one model. solve_memo.py caches a solve by hashing the model text plus parameters, and replays a hit by fixing every variable to its stored value. That works because the solve is deterministic.