Prune the boolean search instead of walking the whole truth table

Sources/AngouriMath/Functions/Boolean/TableSolver.cs

@@ -38,31 +38,196 @@ internal static bool Next(in Span<bool> states)
             return true;
         }
 
+        /// <summary>What a partial assignment already settles about a subexpression.</summary>
+        private enum Verdict { False, True, Unknown }
+
+        private const int Unassigned = -1;
+
         /// <summary>
         /// Returns a tensor of solutions over <paramref name="variables"/> 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.
         /// </summary>
+        /// <remarks>
+        /// <para>
+        /// 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
+        /// <c>2^n</c> 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.
+        /// </para>
+        /// <para>
+        /// 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.
+        /// </para>
+        /// <para>
+        /// 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.
+        /// </para>
+        /// </remarks>
         /// <exception cref="WrongNumberOfArgumentsException"/>
         internal static Matrix? SolveTable(Entity expr, Variable[] variables)
         {
             var count = expr.Vars.Count;
             // 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<Variable, int>(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<Variable, Entity>();
-            do
+            Search(expr, variables, index, assignment, 0, tb);
+            return tb.ToMatrix();
+        }
+
+        static void Search(Entity expr, Variable[] variables, Dictionary<Variable, int> 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;
+        }
+
+        /// <summary>
+        /// Writes out every way of filling in the variables from <paramref name="depth"/> on,
+        /// in counting order. Called where the expression is already true whatever they are.
+        /// </summary>
+        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<Variable, Entity>(variables.Length);
+            for (var i = 0; i < variables.Length; i++)
+                storage[variables[i]] = assignment[i] == 1;
+            return expr.Substitute(storage).EvalBoolean();
+        }
+
+        /// <summary>
+        /// Reads the expression under a partial assignment. Anything it does not recognise is
+        /// <see cref="Verdict.Unknown"/>, which costs pruning and never costs correctness --
+        /// the caller falls back to a real evaluation once everything is assigned.
+        /// </summary>
+        static Verdict Evaluate(Entity expr, Dictionary<Variable, int> 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)

Sources/Tests/UnitTests/Discrete/BooleanSolver.cs

@@ -58,6 +58,100 @@
             }
         }
 
+        static Variable[] Vars(int count) =>
+            Enumerable.Range(0, count).Select(i => (Variable)$"p_{i}").ToArray();
+
+        /// <summary>
+        /// 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.
+        /// </summary>
+        [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());
+        }
+
+        /// <summary>Forty variables, forty solutions, out of 2^40 assignments.</summary>
+        [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);
+            }
+        }
+
+        /// <summary>
+        /// An unsatisfiable expression has no rows, and the contract for that is a null
+        /// rather than an empty matrix.
+        /// </summary>
+        [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));
+        }
+
+        /// <summary>
+        /// 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.
+        /// </summary>
+        [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<int>();
+            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 }")]