Prune the boolean search instead of walking the whole truth table

[Rafael-SOWNet]

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 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

		was	now
p_0 & p_1 & ..., one solution	8 vars	12 ms	5 ms
	18 vars	3.1 s	0 ms
	22 vars	> 30 s	0 ms
	200 vars	—	7 ms
exactly one of k true	40 vars	2⁴⁰, hopeless	208 ms, 40 solutions
an xor chain — nothing prunable	20 vars	2²⁰ substitutions	943 ms, 524 288 solutions

Even 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

• Same rows, same order. Assigning false before true with the last variable moving fastest is exactly the order counting through the table produced. RowsKeepTruthTableOrder pins that against an independently computed expectation.
• Unrecognised nodes cost pruning, never correctness. Anything the three-valued reading does not know reads as Unknown, and once every variable is assigned the search falls through to precisely the old substitute-and-evaluate. A non-boolean expression therefore still throws exactly where it threw before.
• BuildTruthTable is untouched — a truth table is all 2ⁿ rows by definition, so there is nothing there to prune.

No BREAKING-CHANGES.md entry, 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, null per the existing contract)
• RowsKeepTruthTableOrder (order preservation)

Verification

• 6065 C# tests pass, 0 failed
• 130 F# wrapper tests pass
• the existing BooleanSolver.Test theory, which asserts exact solution counts and re-checks every returned row by substitution, is unchanged and green

🤖 Generated with Claude Code