Let the boolean table solver be cancelled - #870
Merged
Conversation
Towards #858. SolveBooleanTable and BuildTruthTable never consulted the cancellation token, so the escape hatch that works everywhere else in the library did not exist here. Measured before the change: a token cancelled after three seconds was still being ignored twenty seconds later. That matters because of what the shape of these methods costs. #864 made the search cheap, which leaves writing every model down as the wall, and how tall it is depends on the answer rather than the question: tautology, 18 variables 262 144 rows 575 ms 124 MB tautology, 20 variables 1 048 576 rows 1724 ms 544 MB tautology, 22 variables 4 194 304 rows 7979 ms 2368 MB A caller cannot know in advance which of those they asked for, and there is no pruning available for a formula every assignment satisfies. Being able to stop is the whole of the remedy available without changing the signature. MultithreadingFunctional.ExitIfCancelled is what PolynomialGcd, Simplificator, Minimiser and ExponentialSolver already use; this adds it at the branch nodes of the search, in the loop that writes out completions, and in the truth-table loop, which is all 2^n rows by definition and so has nothing but stopping to offer. It costs nothing measurable -- 22 variables went 7979 ms to 7943 ms, inside the noise -- because the check is one async-local read against a per-row allocation. Verified: cancelling now returns at the moment it is asked rather than not at all, 6087 C# tests and 130 F# tests pass. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Towards #858, and it removes most of the reason that issue needed a decision.
SolveBooleanTableandBuildTruthTablenever consulted the cancellation token, so the escape hatch that works everywhere else in the library did not exist here. Measured before changing anything: a token cancelled after three seconds was still being ignored twenty seconds later.That matters because of where the cost of these methods now sits. #864 made the search cheap, which leaves writing every model down as the wall — and how tall it is depends on the answer, not the question:
A caller cannot know in advance which of those they asked for, and a formula every assignment satisfies offers nothing to prune. Being able to stop is the whole of the remedy available without changing the signature — which is why this is worth doing regardless of how #858 is settled.
What changed
MultithreadingFunctional.ExitIfCancelled()— the same helperPolynomialGcd,Simplificator,MinimiserandExponentialSolveralready use — at three places:It costs nothing measurable. 22 variables went from 7979 ms to 7943 ms — inside the noise — because the check is one async-local read set against a per-row allocation.
On #858's remaining question
Worth recording what this leaves. The genuinely useful additions — asking whether a formula is satisfiable, asking for one model, capping the count — are all additive, so they do not need the 2.0 window and can be designed at leisure in 2.1. The only thing that would need the window is changing
SolveBooleanTable's existing return type, and there is a decent argument against: a method named for returning the table of solutions returning exactly that is coherent, and the bounded and lazy needs are better served by new members than by mutating this one.So #858 is no longer a deadline, which is the useful part.
Verification
No behavioural change for anyone who does not set a token, and no signature change, so nothing for
BREAKING-CHANGES.md.🤖 Generated with Claude Code