From b9f5e53da4acf1448d266983c54cb42d9ae67eef Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Sun, 9 Aug 2026 21:08:03 +0000 Subject: [PATCH] Prune the boolean search instead of walking the whole truth table 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) --- .../Functions/Boolean/TableSolver.cs | 187 ++++++++++++++++-- .../Tests/UnitTests/Discrete/BooleanSolver.cs | 94 +++++++++ 2 files changed, 270 insertions(+), 11 deletions(-) diff --git a/Sources/AngouriMath/Functions/Boolean/TableSolver.cs b/Sources/AngouriMath/Functions/Boolean/TableSolver.cs index 5ef389845..e6782eb24 100644 --- a/Sources/AngouriMath/Functions/Boolean/TableSolver.cs +++ b/Sources/AngouriMath/Functions/Boolean/TableSolver.cs @@ -38,11 +38,35 @@ internal static bool Next(in Span states) return true; } + /// What a partial assignment already settles about a subexpression. + private enum Verdict { False, True, Unknown } + + private const int Unassigned = -1; + /// /// Returns a tensor of solutions over so that - /// the expression turns into a True when evaled. Computes the roots by - /// compiling the truth table + /// the expression turns into a True when evaled. /// + /// + /// + /// Assigns the variables one at a time and asks after each what the expression + /// already is. A prefix that makes it false rules out every completion of itself at + /// once, and a prefix that makes it true admits all of them, so neither has to be + /// walked. Only a prefix that settles nothing is branched on. Enumerating all + /// 2^n rows and testing each — which is what this did — is the case where no + /// prefix ever settles anything, and is now the worst case rather than the only one. + /// + /// + /// The order of the rows is unchanged: assigning false before true, with the last + /// variable moving fastest, is the same order counting through the table produced. + /// + /// + /// This enumerates models, not satisfiability, so the result can still be + /// exponentially large — a tautology over n variables has 2^n solutions and they all + /// have to be written down. What is gone is paying that price for the search when the + /// answer is small. + /// + /// /// internal static Matrix? SolveTable(Entity expr, Variable[] variables) { @@ -50,19 +74,160 @@ internal static bool Next(in Span states) // TODO: we probably also should verify the uniqueness of the given variables if (count != variables.Length) throw new WrongNumberOfArgumentsException("Number of variables must equal number of variables in the expression"); - var states = new bool[variables.Length]; + + var index = new Dictionary(count); + for (var i = 0; i < variables.Length; i++) + index[variables[i]] = i; + + var assignment = new int[count]; + for (var i = 0; i < count; i++) + assignment[i] = Unassigned; + var tb = new MatrixBuilder(count); - var variablesStorage = new Dictionary(); - do + Search(expr, variables, index, assignment, 0, tb); + return tb.ToMatrix(); + } + + static void Search(Entity expr, Variable[] variables, Dictionary index, + int[] assignment, int depth, MatrixBuilder tb) + { + switch (Evaluate(expr, index, assignment)) { - for (int i = 0; i < count; i++) - variablesStorage[variables[i]] = states[i]; - if (expr.Substitute(variablesStorage).EvalBoolean()) - tb.Add(states.Select(s => (Entity)s)); + case Verdict.False: + return; + case Verdict.True: + EmitEveryCompletion(assignment, depth, tb); + return; } - while (Next(states)); - return tb.ToMatrix(); + if (depth == assignment.Length) + { + // Everything is assigned and the three-valued reading still cannot say. That + // is a node shape it does not know rather than a real undecidability, so fall + // back to substituting and evaluating for real. + if (Concretely(expr, variables, assignment)) + EmitEveryCompletion(assignment, depth, tb); + return; + } + + assignment[depth] = 0; + Search(expr, variables, index, assignment, depth + 1, tb); + assignment[depth] = 1; + Search(expr, variables, index, assignment, depth + 1, tb); + assignment[depth] = Unassigned; + } + + /// + /// Writes out every way of filling in the variables from on, + /// in counting order. Called where the expression is already true whatever they are. + /// + static void EmitEveryCompletion(int[] assignment, int depth, MatrixBuilder tb) + { + var free = assignment.Length - depth; + var total = 1L << free; + for (long combination = 0; combination < total; combination++) + { + var row = new Entity[assignment.Length]; + for (var i = 0; i < depth; i++) + row[i] = assignment[i] == 1; + for (var j = 0; j < free; j++) + row[depth + j] = ((combination >> (free - 1 - j)) & 1) == 1; + tb.Add(row); + } + } + + static bool Concretely(Entity expr, Variable[] variables, int[] assignment) + { + var storage = new Dictionary(variables.Length); + for (var i = 0; i < variables.Length; i++) + storage[variables[i]] = assignment[i] == 1; + return expr.Substitute(storage).EvalBoolean(); + } + + /// + /// Reads the expression under a partial assignment. Anything it does not recognise is + /// , which costs pruning and never costs correctness -- + /// the caller falls back to a real evaluation once everything is assigned. + /// + static Verdict Evaluate(Entity expr, Dictionary index, int[] assignment) + { + switch (expr) + { + case Entity.Boolean b: + return b.Value ? Verdict.True : Verdict.False; + + case Variable v: + if (!index.TryGetValue(v, out var i)) + return Verdict.Unknown; + return assignment[i] switch + { + 0 => Verdict.False, + 1 => Verdict.True, + _ => Verdict.Unknown + }; + + case Notf not: + return Evaluate(not.Argument, index, assignment) switch + { + Verdict.True => Verdict.False, + Verdict.False => Verdict.True, + _ => Verdict.Unknown + }; + + case Andf and: + { + // One false settles it without reading the other side. + var left = Evaluate(and.Left, index, assignment); + if (left is Verdict.False) return Verdict.False; + var right = Evaluate(and.Right, index, assignment); + if (right is Verdict.False) return Verdict.False; + return left is Verdict.True && right is Verdict.True ? Verdict.True : Verdict.Unknown; + } + + case Orf or: + { + var left = Evaluate(or.Left, index, assignment); + if (left is Verdict.True) return Verdict.True; + var right = Evaluate(or.Right, index, assignment); + if (right is Verdict.True) return Verdict.True; + return left is Verdict.False && right is Verdict.False ? Verdict.False : Verdict.Unknown; + } + + case Xorf xor: + { + // Neither side alone settles an xor. + var left = Evaluate(xor.Left, index, assignment); + if (left is Verdict.Unknown) return Verdict.Unknown; + var right = Evaluate(xor.Right, index, assignment); + if (right is Verdict.Unknown) return Verdict.Unknown; + return left == right ? Verdict.False : Verdict.True; + } + + case Impliesf implies: + { + var assumption = Evaluate(implies.Assumption, index, assignment); + if (assumption is Verdict.False) return Verdict.True; + var conclusion = Evaluate(implies.Conclusion, index, assignment); + if (conclusion is Verdict.True) return Verdict.True; + return assumption is Verdict.True && conclusion is Verdict.False + ? Verdict.False + : Verdict.Unknown; + } + + case Equalsf equals: + { + // Only where both sides read as booleans; a comparison of anything else + // leaves its operands Unknown and falls out here as Unknown too. + var left = Evaluate(equals.Left, index, assignment); + if (left is Verdict.Unknown) return Verdict.Unknown; + var right = Evaluate(equals.Right, index, assignment); + if (right is Verdict.Unknown) return Verdict.Unknown; + return left == right ? Verdict.True : Verdict.False; + } + + default: + return Verdict.Unknown; + } } internal static Matrix? BuildTruthTable(Entity expr, Variable[] variables) diff --git a/Sources/Tests/UnitTests/Discrete/BooleanSolver.cs b/Sources/Tests/UnitTests/Discrete/BooleanSolver.cs index 4fd19e6a4..97ab3f65e 100644 --- a/Sources/Tests/UnitTests/Discrete/BooleanSolver.cs +++ b/Sources/Tests/UnitTests/Discrete/BooleanSolver.cs @@ -58,6 +58,100 @@ public void Test(int rootNumber, string exprString) } } + static Variable[] Vars(int count) => + Enumerable.Range(0, count).Select(i => (Variable)$"p_{i}").ToArray(); + + /// + /// Sixty variables is 2^60 assignments. Enumerating them was what this did, so this + /// test cannot pass by accident: it either prunes or it never returns. + /// + [Fact] + public void AConjunctionIsSolvedWithoutEnumeratingTheTable() + { + var vars = Vars(60); + Entity expr = vars[0]; + for (var i = 1; i < vars.Length; i++) + expr = expr & vars[i]; + + var solutions = MathS.SolveBooleanTable(expr, vars); + + Assert.NotNull(solutions); + Assert.Equal(1, solutions.RowCount); + for (var j = 0; j < vars.Length; j++) + Assert.True((bool)solutions[0, j].EvalBoolean()); + } + + /// Forty variables, forty solutions, out of 2^40 assignments. + [Fact] + public void ExactlyOneTrueIsFoundWithoutEnumeratingTheTable() + { + var vars = Vars(40); + Entity expr = vars[0]; + for (var i = 1; i < vars.Length; i++) + expr = expr | vars[i]; + for (var i = 0; i < vars.Length; i++) + for (var j = i + 1; j < vars.Length; j++) + expr = expr & !(vars[i] & vars[j]); + + var solutions = MathS.SolveBooleanTable(expr, vars); + + Assert.NotNull(solutions); + Assert.Equal(vars.Length, solutions.RowCount); + for (var row = 0; row < solutions.RowCount; row++) + { + var trues = 0; + for (var j = 0; j < vars.Length; j++) + if ((bool)solutions[row, j].EvalBoolean()) trues++; + Assert.Equal(1, trues); + } + } + + /// + /// An unsatisfiable expression has no rows, and the contract for that is a null + /// rather than an empty matrix. + /// + [Fact] + public void AContradictionHasNoSolutions() + { + var vars = Vars(30); + Entity expr = vars[0] & !vars[0]; + for (var i = 1; i < vars.Length; i++) + expr = expr & (vars[i] | !vars[i]); + + Assert.Null(MathS.SolveBooleanTable(expr, vars)); + } + + /// + /// Pruning must not reorder the answer. The rows are still the satisfying rows of the + /// truth table, in the order the table would have produced them. + /// + [Fact] + public void RowsKeepTruthTableOrder() + { + var vars = Vars(4); + Entity expr = (vars[0] | vars[1]) & (vars[2] | vars[3]); + + var solutions = MathS.SolveBooleanTable(expr, vars); + Assert.NotNull(solutions); + + var expected = new List(); + for (var assignment = 0; assignment < 16; assignment++) + { + var bits = Enumerable.Range(0, 4) + .Select(i => ((assignment >> (3 - i)) & 1) == 1).ToArray(); + if ((bits[0] || bits[1]) && (bits[2] || bits[3])) expected.Add(assignment); + } + + Assert.Equal(expected.Count, solutions.RowCount); + for (var row = 0; row < solutions.RowCount; row++) + { + var actual = 0; + for (var j = 0; j < 4; j++) + actual = (actual << 1) | ((bool)solutions[row, j].EvalBoolean() ? 1 : 0); + Assert.Equal(expected[row], actual); + } + } + [Theory] [InlineData("(x implies a) = b", "{ False provided a and b, True provided a and b, False provided not a and b, True provided not a and not b }")] [InlineData("(x and a) = b", "{ True provided b and a, False provided a and not b, True provided not a and not b, False provided not a and not b }")]