Skip to content

Build one candidate when the construction budget is already spent - #46

Merged
guyvdbroeck merged 2 commits into
mainfrom
portfolio-last-attempt
Sep 1, 2026
Merged

Build one candidate when the construction budget is already spent#46
guyvdbroeck merged 2 commits into
mainfrom
portfolio-last-attempt

Conversation

@guyvdbroeck

Copy link
Copy Markdown
Member

vtree_from_portfolio walks its catalog under a construction deadline and
skips every remaining entry once that deadline has passed. When the deadline is
already spent at the loop's first iteration, that skips the whole catalog: the
build returns with nothing and the caller gets a construction error reporting
every candidate as failed, on a formula nothing was ever tried on. It happens
when preprocessing used the budget up, and on multi-component formulas where
earlier components spent it.

The first catalog entry is an anytime cutter, so given any wall at all it
returns a decomposition. When the deadline is spent and nothing has been built
yet, the entry the walk stopped at — the first one, when the deadline was
already spent on arrival — now gets one attempt with a fixed one-second cap and
wall and with behind_schedule set, since finishing beats searching in that
regime. The candidates behind it are reported as never started, as they are
today. The wall is a fixed number rather than a share of what is left because
what is left is zero or less. A diag! line reports that the fallback fired and
which entry took it.

Whether anything has been built is read from both best.vtree and cands,
because which of the two a built candidate lands in depends on the mode: plain
selection adopts into best, projected selection collects into cands and
picks at the end.

On a 1,074-instance model-counting benchmark at a two-minute wall this removed
a construction-failure class: two instances that had reported every candidate
failed were solved, and nothing that solved before stopped solving. That is the
honest size of it, a robustness fix worth about two instances at that budget
rather than a scoring improvement.

The portfolio skipped every catalog entry when its deadline had passed
before the walk began, so the build returned nothing and the caller got a
construction error naming every candidate as failed. It happens when
preprocessing used the budget up, and on multi-component formulas where
earlier components spent it.

The entry the walk stops at now gets one attempt under a fixed one-second
wall when nothing has been built yet, and the entries behind it are
reported as never started. The wall is fixed rather than a share of what
is left because what is left is zero or less.
The deterministic-unit twin of the wall-clock case expected an error from
a one-unit budget, and the field and module docs stated the old rule: that
nothing stands between an exhausted budget and a construction error, and
that the wall an entry gets is always the time left.

The multi-component check now uses two differently sized components. Two
identical ones are served from the component cache, so only one of them is
constructed and the attempts cannot be counted.
@guyvdbroeck
guyvdbroeck merged commit 30f4911 into main Sep 1, 2026
2 checks passed
@guyvdbroeck
guyvdbroeck deleted the portfolio-last-attempt branch September 1, 2026 20:22
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant