From 65d3f961dbaa2b59074ce83c24ab54e69e8cda9b Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Mon, 10 Aug 2026 14:24:32 +0000 Subject: [PATCH] Let the boolean table solver be cancelled Towards #858. SolveBooleanTable and BuildTruthTable never consulted the cancellation token, so the escape hatch that works everywhere else in the library did not exist here. Measured before the change: a token cancelled after three seconds was still being ignored twenty seconds later. That matters because of what the shape of these methods costs. #864 made the search cheap, which leaves writing every model down as the wall, and how tall it is depends on the answer rather than the question: tautology, 18 variables 262 144 rows 575 ms 124 MB tautology, 20 variables 1 048 576 rows 1724 ms 544 MB tautology, 22 variables 4 194 304 rows 7979 ms 2368 MB A caller cannot know in advance which of those they asked for, and there is no pruning available for a formula every assignment satisfies. Being able to stop is the whole of the remedy available without changing the signature. MultithreadingFunctional.ExitIfCancelled is what PolynomialGcd, Simplificator, Minimiser and ExponentialSolver already use; this adds it at the branch nodes of the search, in the loop that writes out completions, and in the truth-table loop, which is all 2^n rows by definition and so has nothing but stopping to offer. It costs nothing measurable -- 22 variables went 7979 ms to 7943 ms, inside the noise -- because the check is one async-local read against a per-row allocation. Verified: cancelling now returns at the moment it is asked rather than not at all, 6087 C# tests and 130 F# tests pass. Co-Authored-By: Claude Opus 5 (1M context) --- .../Functions/Boolean/TableSolver.cs | 13 ++++ .../Tests/UnitTests/Discrete/BooleanSolver.cs | 77 +++++++++++++++++++ 2 files changed, 90 insertions(+) diff --git a/Sources/AngouriMath/Functions/Boolean/TableSolver.cs b/Sources/AngouriMath/Functions/Boolean/TableSolver.cs index e6782eb24..0e4539429 100644 --- a/Sources/AngouriMath/Functions/Boolean/TableSolver.cs +++ b/Sources/AngouriMath/Functions/Boolean/TableSolver.cs @@ -6,6 +6,7 @@ // using AngouriMath.Core.Exceptions; +using AngouriMath.Core.Multithreading; using System; using static AngouriMath.Entity; @@ -91,6 +92,7 @@ private enum Verdict { False, True, Unknown } static void Search(Entity expr, Variable[] variables, Dictionary index, int[] assignment, int depth, MatrixBuilder tb) { + MultithreadingFunctional.ExitIfCancelled(); switch (Evaluate(expr, index, assignment)) { case Verdict.False: @@ -121,12 +123,20 @@ static void Search(Entity expr, Variable[] variables, Dictionary /// Writes out every way of filling in the variables from on, /// in counting order. Called where the expression is already true whatever they are. /// + /// + /// This is where the cost of the method's shape lands. The search is cheap, but every + /// model has to be written down, and a formula that most assignments satisfy has a + /// great many: a tautology over 22 variables is four million rows and 2.4 GB. So this + /// is the loop that most needs to be interruptible — the caller cannot know in advance + /// that the answer will not fit. + /// 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++) { + MultithreadingFunctional.ExitIfCancelled(); var row = new Entity[assignment.Length]; for (var i = 0; i < depth; i++) row[i] = assignment[i] == 1; @@ -241,6 +251,9 @@ static Verdict Evaluate(Entity expr, Dictionary index, int[] assi var variablesStorage = new Dictionary(); do { + // A truth table is all 2^n rows by definition, so there is no pruning to be + // had here and the only mercy available is being able to stop. + MultithreadingFunctional.ExitIfCancelled(); for (int i = 0; i < count; i++) variablesStorage[variables[i]] = states[i]; tb.Add(states.Select(s => (Entity)s).Append(expr.Substitute(variablesStorage).EvalBoolean())); diff --git a/Sources/Tests/UnitTests/Discrete/BooleanSolver.cs b/Sources/Tests/UnitTests/Discrete/BooleanSolver.cs index 97ab3f65e..0fb3fde06 100644 --- a/Sources/Tests/UnitTests/Discrete/BooleanSolver.cs +++ b/Sources/Tests/UnitTests/Discrete/BooleanSolver.cs @@ -6,8 +6,10 @@ // using AngouriMath; +using System; using System.Collections.Generic; using System.Linq; +using System.Threading; using Xunit; namespace AngouriMath.Tests.Discrete @@ -152,6 +154,81 @@ public void RowsKeepTruthTableOrder() } } + /// + /// A tautology over n variables has 2^n models and every one has to be written down, + /// so the answer can be far larger than the caller could know in advance — 22 + /// variables is four million rows and some gigabytes. Pruning cannot help, since + /// there is nothing to prune, which leaves stopping as the only recourse. It was not + /// available: the token that aborts was not consulted here + /// at all. + /// + static Entity Tautology(int count) + { + Entity all = (Entity)"p_0" | !(Entity)"p_0"; + for (var i = 1; i < count; i++) + all &= (Entity)$"p_{i}" | !(Entity)$"p_{i}"; + return all; + } + + [Fact] + public void AnAlreadyCancelledTokenStopsTheSolverAtOnce() + { + using var source = new CancellationTokenSource(); + source.Cancel(); + MathS.Multithreading.SetLocalCancellationToken(source.Token); + try + { + Assert.Throws( + () => MathS.SolveBooleanTable(Tautology(24), Vars(24))); + } + finally + { + MathS.Multithreading.SetLocalCancellationToken(default); + } + } + + [Fact] + public void CancellingPartwayThroughStopsTheSolver() + { + using var source = new CancellationTokenSource(); + using var started = new ManualResetEventSlim(); + + var worker = new Thread(() => + { + MathS.Multithreading.SetLocalCancellationToken(source.Token); + started.Set(); + try { MathS.SolveBooleanTable(Tautology(24), Vars(24)); } + catch (OperationCanceledException) { cancelled = true; } + }); + worker.Start(); + started.Wait(); + Thread.Sleep(200); + source.Cancel(); + + Assert.True(worker.Join(TimeSpan.FromSeconds(20)), "the solver ignored the cancellation"); + Assert.True(cancelled, "the solver stopped without reporting cancellation"); + } + + private volatile bool cancelled; + + /// The truth table is all 2^n rows by definition, and must stop too. + [Fact] + public void AnAlreadyCancelledTokenStopsTheTruthTableAtOnce() + { + using var source = new CancellationTokenSource(); + source.Cancel(); + MathS.Multithreading.SetLocalCancellationToken(source.Token); + try + { + Assert.Throws( + () => MathS.Boolean.BuildTruthTable(Tautology(24), Vars(24))); + } + finally + { + MathS.Multithreading.SetLocalCancellationToken(default); + } + } + [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 }")]