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 }")]