Column-to-row coefficient access#

Status: Open lead. Owner: unassigned.

Investigate how a walk over a tableau column should obtain the coefficients it needs. Measurement, design selection, implementation, and evaluation remain open. This continues the occurrence-index work of original lead 3b, which implemented only the row-to-column half of a cross-linked matrix.

Current representation#

The LRA chapter describes the layout. A row is a vector of RowEntry {var, coeff, occ_slot} sorted by variable ID. The column occurs_in_[j] is an unordered vector of basic variables. It records neither the coefficient \(a_{ij}\) nor the position of variable \(j\) inside row \(i\). The links are therefore asymmetric:

row -> column:  occurs_in_[e.var][e.occ_slot] == b   for each entry e of rows_[b]
column -> row:  none; a_ij must be found inside rows_[i]

A column walk yields the rows containing \(j\). Any consumer that also needs \(a_{ij}\) must then search row \(i\) for it. These consumers do:

Consumer

Needs \(a_{ij}\) for

Lookup in row \(i\)

update

\(\beta(x_i) \mathrel{+}= a_{ij}\,\Delta\) whenever a nonbasic assignment changes, including after each check pivot, after a fixed-basic elimination pivot, on an SOI step without a pivot, when a new bound excludes the current value, and from set_nonbasic_value

linear scan, stops at \(j\)

soi_select, breakpoint collection

one breakpoint per row containing \(j\)

linear scan, stops at \(j\)

soi_select, breakpoint crossing

the same coefficient again, for each crossed breakpoint

linear scan, stops at \(j\)

freedom_interval_impl

the bound on \(x_j\) implied by each \(x_i\)’s bounds

linear find_if, stops at \(j\)

diversify_shared_model, apply lambda

scratch copy of update

linear scan of the whole row, no early exit

pivot

the entering variable’s coefficient in each affected row

std::lower_bound

unlink_occurrence

the row entry of the swapped column element, to repair its occ_slot

std::lower_bound

Four of the five linear lookups cost the position of \(j\) in row \(i\); the apply lambda costs the whole row. Sorted rows make an \(O(\log |row_i|)\) binary search possible, but only pivot and unlink_occurrence use one. Lead 7’s closing note describes coefficient lookup as lower_bound, following Griggio §2.5.2; that holds only for those two sites. unlink_occurrence has three callers: pivot’s two removal sites and set_soi_direction, which relinks the SOI objective row.

The other column walks need row membership only. They are the row-propagation scans in the online propagator and its component counterpart, and the online model-phase dirty marking and its component counterpart. A further linear lookup in check’s SOI path, which reads the leaving row’s coefficient for the entering variable, is not a column walk. It is in scope for design 1 below, but not for designs 2 and 3.

Candidate designs#

The candidates below share one obligation: the search must be unchanged. Each changes how the coefficient is located, not which coefficient is used or the order of occurs_in_. So the search counters :lra.pivots, :lra.pivot-term-ops, :sat.decisions and :sat.conflicts should be identical to the baseline. As in lead 3b, that makes every timing difference a constant factor rather than a different search trajectory.

  1. Binary search at the linear sites. Replace the linear lookups with std::lower_bound over the sorted row. In soi_select, carry the coefficient in the breakpoint record instead of looking it up twice. This needs no representation change, no extra memory, and no maintenance. On short rows, or when \(j\) sits near the front of the row, an early-exit scan may beat a binary search; step 3 below measures that. This does not help unlink_occurrence, which already searches by bisection.

  2. Coefficient in the column. Store (basic, coeff) in occurs_in_. Lookup becomes constant-time. During the merge, occ_slot locates the column entry of a changed or new term in constant time. Unchanged terms need no write. Costs: a column entry grows from 8 bytes to 8 bytes plus an inline Rational (24 bytes on the measured build, see compact rational storage); a large value deep-copies its GMP rational; and the merge performs an extra coefficient copy per changed term. Rational copies were 1.1% of lead 7’s tropical profile, but the pivot source comment records 465M copy constructions on scrambled228965, the largest single source being per-row copies that pivot no longer makes. The coefficient is duplicated, so every producer of a row must keep both copies equal, including pop, set_soi_direction and rebuild_occurs_in_index. This does not help unlink_occurrence.

  3. Row slot in the column. Store (basic, row_slot). Lookup and the unlink_occurrence repair both become constant-time. The maintenance cost is the scattered refresh described above, paid inside pivot’s hottest loop. Without a measurement this is the least promising option.

  4. King’s doubly linked matrix (King §2.2.7). Lead 3b did not adopt it: it gives up sorted contiguous rows and the two-way merge, and needs a dense scratch map for row addition. It was not prototyped.

Evidence so far#

No measurement isolates the cost of the coefficient lookups. Existing profiles bound it only loosely:

  • Lead 7’s gprof profile puts LraTableau::update at 2.1% self time, against 74.1% for pivot. The register places that profile on tropical constraint-199552, a long-column instance. The Rational operators are out-of-line and attributed separately, so the 2.1% excludes the rational arithmetic itself. It does not bound the cost on long-row instances.

  • A QF_LIA profile of ten medium-hard instances (2026-08-21, after occ_slot landed) puts LraTableau::unlink_occurrence at 5.0% self time, against 5.7% for pivot. That figure includes the swap-pop and is not split by caller, but it is the mechanism design 3 targets. The same profile attributes 8.0% of all Rational::operator* calls to update. Those calls are the \(a_{ij}\Delta\) products, not the lookup itself.

The volume of lookup work is roughly the column entries walked times the position of \(j\) in each row. Long rows, as in the latendresse/ecoli family (691 terms on ecoliFBAyicesTest-500, three of the seven regressions in lead 3b’s >0.2 s band), raise the second factor. Long columns raise the first: the register reports tropical rows of about 102 terms during search and columns averaging 679. Which family carries more lookup cost is a hypothesis for step 1, not a conclusion.

Investigation and rejection criteria#

  1. Add counters for column-walk lookups: lookups performed and row entries inspected, separately for update, both soi_select sites, freedom intervals and model mutation. Count unlink_occurrence repairs and their probes by caller. Profile ecoliFBAyicesTest-500, p6-zenonumeric_s5, tropical constraint-199552, and the QF_LRA stratified sample on SLURM.

  2. The lookups are inline loops, so a profile cannot attribute their time directly. Use the combined self time of the consuming functions (update, soi_select, freedom_interval_impl, diversify_shared_model) as an upper bound; check that all four appear as their own symbols, since an inlined consumer’s time would be charged to its caller. Close this lead and record the measurement here if that bound stays below a threshold fixed before the run (for example 2%) on each of the three named instances and on the stratified sample in aggregate. Otherwise continue.

  3. Implement design 1 first. Confirm that the search counters are bit-identical on solved files, and evaluate with paired per-file time ratios against the unchanged binary, as in lead 3b’s cost analysis, not with a PAR2 difference.

  4. Consider design 2 only if lookups remain above the threshold after design 1. Extend occurs_in_index_matches_full_rebuild to check that each column coefficient equals its row coefficient. Add a pop-then-pivot regression and measure memory alongside time. Consider design 3 only after lead 3b’s LraVarId narrowing experiment shows that the unlink_occurrence repair, not RowEntry size, is the remaining cost.

Any representation change (designs 2 and 3) touches the tableau invariant. It requires make asan-test and the QF_LRA model fuzz merge gate on SLURM. Design 1 also changes solver code, so it requires the merge gate as well, even though its search is expected to be unchanged. Reject any variant that changes a search counter or an answer, or produces an invalid model. Also reject one that regresses the >1 s band of commonly solved files without a corresponding gain on the instances where step 1 found the lookup cost.

Sources#

Source

Use here

Tim King, PhD thesis, NYU, 2014 [30], §2.2.7

Doubly linked sparse matrix with constant-time unlink; the structure whose column-to-row half Primo lacks. Not adopted.

Alberto Griggio, PhD thesis, 2009 [27], §2.5.2

Sorted contiguous coefficient arrays, whose layout Primo’s rows follow.

No paper mechanism is implemented by this lead. Designs 1–3 are implementation choices within Primo’s existing sorted-row representation.