MathS.SolveBooleanTable enumerates every assignment. TableSolver.SolveTable walks all 2^n rows and, for each, does a full symbolic Substitute followed by EvalBoolean — no unit propagation, no early exit, no clause learning:
do
{
for (int i = 0; i < count; i++)
variablesStorage[variables[i]] = states[i];
if (expr.Substitute(variablesStorage).EvalBoolean())
tb.Add(states.Select(s => (Entity)s));
}
while (Next(states));Measured on the current build, with a formula having exactly one satisfying assignment:
| variables |
time |
| 8 |
12 ms |
| 18 |
3.1 s |
| 22 |
> 30 s |
Each variable doubles the work, and the per-row cost is a tree substitution rather than a bit operation, so the constant factor is large on top of the exponential.
That puts a hard ceiling on the public API at roughly 20 variables. A one-hot encoding of anything combinatorial passes it immediately — a 4×4 Latin square needs 64 booleans, a 9×9 Sudoku needs 729.
Suggested fix
DPLL with unit propagation and pure-literal elimination, over a compiled clause representation rather than repeated Entity.Substitute. Watched literals and conflict-driven learning are the usual next steps but are not needed to make this vastly better than exhaustive enumeration.
Purely internal — no signature change, so it does not need the 2.0 window.
One thing that does want the 2.0 window
The method returns Matrix? holding every satisfying assignment, materialised. For a formula with many models that is inherently exponential in output size no matter how good the solver is, and callers who want "is this satisfiable" or "give me one model" have no way to say so.
If the signature should grow a budget/cancellation parameter, or return solutions lazily instead of a whole Matrix, that is a breaking change and wants deciding before 2.0 leaves preview. The internals can improve at any time; the shape cannot.
Entity.SolveBoolean(Variable) is a separate, symbolic, single-variable path and is not affected.
MathS.SolveBooleanTableenumerates every assignment.TableSolver.SolveTablewalks all2^nrows and, for each, does a full symbolicSubstitutefollowed byEvalBoolean— no unit propagation, no early exit, no clause learning:Measured on the current build, with a formula having exactly one satisfying assignment:
Each variable doubles the work, and the per-row cost is a tree substitution rather than a bit operation, so the constant factor is large on top of the exponential.
That puts a hard ceiling on the public API at roughly 20 variables. A one-hot encoding of anything combinatorial passes it immediately — a 4×4 Latin square needs 64 booleans, a 9×9 Sudoku needs 729.
Suggested fix
DPLL with unit propagation and pure-literal elimination, over a compiled clause representation rather than repeated
Entity.Substitute. Watched literals and conflict-driven learning are the usual next steps but are not needed to make this vastly better than exhaustive enumeration.Purely internal — no signature change, so it does not need the 2.0 window.
One thing that does want the 2.0 window
The method returns
Matrix?holding every satisfying assignment, materialised. For a formula with many models that is inherently exponential in output size no matter how good the solver is, and callers who want "is this satisfiable" or "give me one model" have no way to say so.If the signature should grow a budget/cancellation parameter, or return solutions lazily instead of a whole
Matrix, that is a breaking change and wants deciding before 2.0 leaves preview. The internals can improve at any time; the shape cannot.Entity.SolveBoolean(Variable)is a separate, symbolic, single-variable path and is not affected.