Prune the boolean search instead of walking the whole truth table - #864
Merged
Conversation
Closes #858. SolveTable enumerated all 2^n assignments and, for each, did a full symbolic Substitute followed by EvalBoolean. Twenty-two variables did not finish in 30s, which put a hard ceiling on the public API at around twenty. It now assigns variables one at a time and asks after each what the expression already is, under a three-valued reading. A prefix that makes it false rules out every completion of itself at once; a prefix that makes it true admits all of them and they are written out directly. Only a prefix that settles nothing gets branched on. Enumerating the whole table is what happens when no prefix ever settles anything, so it went from being the algorithm to being the worst case. p_0 & p_1 & ... , one solution was 8 vars 12 ms 18 vars 3.1 s 22 vars >30 s now 22 vars 0 ms 200 vars 7 ms exactly one of k true now 40 vars 208 ms (40 solutions of 2^40) an xor chain, nothing prunable now 20 vars 943 ms (524288 solutions) Even the adversarial case is faster: the old per-row cost was a symbolic substitution into the tree, and the new one is a walk that stops early plus a row written straight out. What remains exponential is the output -- a tautology over n variables has 2^n solutions and they all have to be written down. That is the contract, not the search, and changing it would change the signature. No behavioural change. The same rows come back in the same order: assigning false before true with the last variable moving fastest is the order counting through the table produced, and RowsKeepTruthTableOrder pins it. An expression the three-valued reading does not recognise falls through to exactly the old substitute-and-evaluate once everything is assigned, so unhandled node shapes cost pruning and never correctness. BuildTruthTable is untouched, since a truth table is all 2^n rows by definition. The three new tests cannot pass by enumeration: 60 variables is 2^60. Verified: 6065 C# tests and 130 F# tests pass. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Rafael-SOWNet
added a commit
that referenced
this pull request
Aug 10, 2026
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
1 participant
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.
Closes #858.
SolveTableenumerated all2^nassignments and, for each, did a full symbolicSubstitutefollowed byEvalBoolean. Twenty-two variables did not finish in 30 s, which put a hard ceiling on the public API at around twenty.It now assigns variables one at a time and asks after each what the expression already is, under a three-valued reading. A prefix that makes it false rules out every completion of itself at once; a prefix that makes it true admits all of them, and they are written out directly rather than tested. Only a prefix that settles nothing gets branched on.
Walking the whole table is what happens when no prefix ever settles anything — so it went from being the algorithm to being the worst case.
Measured
p_0 & p_1 & ..., one solutionEven the adversarial case is faster. The old per-row cost was a symbolic substitution into the tree; the new one is a walk that stops early plus a row written straight out.
What stays exponential is the output. A tautology over n variables has 2ⁿ solutions and they all have to be written down. That is the method's contract — it enumerates models, not satisfiability — and changing it would change the signature, which is the separate question raised in #858 and worth settling while 2.0 is in preview. This PR does not touch it.
No behavioural change
RowsKeepTruthTableOrderpins that against an independently computed expectation.BuildTruthTableis untouched — a truth table is all 2ⁿ rows by definition, so there is nothing there to prune.No
BREAKING-CHANGES.mdentry, because nothing observable changed.Tests
Three of the new tests cannot pass by enumeration — 60 variables is 2⁶⁰:
AConjunctionIsSolvedWithoutEnumeratingTheTable(60 vars, 1 solution)ExactlyOneTrueIsFoundWithoutEnumeratingTheTable(40 vars, 40 solutions)AContradictionHasNoSolutions(30 vars,nullper the existing contract)RowsKeepTruthTableOrder(order preservation)Verification
BooleanSolver.Testtheory, which asserts exact solution counts and re-checks every returned row by substitution, is unchanged and green🤖 Generated with Claude Code