Introduction / Getting Started

What LogicalOptimizer is

LogicalOptimizer is a lightweight .NET library and CLI for parsing, optimizing, and transforming Boolean expressions. Everything is in-house — no native and no third-party runtime dependency — and every result it returns is verified equivalent to the input before you get it.

Two properties define the project and are never traded away:

  • No third-party runtime dependency — a shipped package references other LogicalOptimizer packages and nothing else. Audited on every pull request and enforced as a gate before publishing.
  • Explainability + mandatory verification — minimality is reported with an explicit status (never a silent downgrade), and equivalence is checked on every optimization (truth table up to 12 variables, built-in CDCL SAT miter proof beyond).

Both terms are defined precisely, with the test or CI check that backs each one and the limits of each, in CLAIMS.md.

What it is not: a replacement for Z3 (full SMT), ABC (logic synthesis), CUDD (industrial BDD), or a complete Espresso. It covers propositional Boolean reasoning, not parity-across-the-board — see Choosing a tool for where an alternative is the better answer.

Requirements

  • Library packages: .NET 8.0 or higher (single net8.0 asset, consumable from any newer runtime).
  • CLI tool / building from source: .NET 10 SDK.
  • OS: Windows, Linux, or macOS.

Installation

Add the library as a NuGet package — since v4.0 there is exactly one:

# The whole toolkit (all seven assemblies) in one package.
dotnet add package LogicalOptimizer

Upgrading from pre-4.0? The former per-layer packages (.Core / .Sat / .Bdd / .Dnnf / .Formats / .Minimization / .Full) remain installable as deprecated forwarding shells that depend on LogicalOptimizer, so existing references keep compiling — see Packages & Architecture.

Install the CLI as a global .NET tool (the command is logical-optimizer):

dotnet tool install -g LogicalOptimizer.Cli

Your first optimize

From the CLI:

logical-optimizer "a & b | a & c"

Which prints (running from source with dotnet run --project LogicalOptimizer.Cli -c Release -- "a & b | a & c" gives the same):

Original: a & b | a & c
Optimized: a & (b | c)
Equivalent: proven
Minimality: proven
Cost: 4 -> 3 literals
CNF: a & (b | c)
DNF: a & b | a & c
Variables: [a, b, c]

Truth Table:
| a | b | c | Result |
| - | - | - | ------ |
| 0 | 0 | 0 | 0      |
| 0 | 0 | 1 | 0      |
| 0 | 1 | 0 | 0      |
| 0 | 1 | 1 | 0      |
| 1 | 0 | 0 | 0      |
| 1 | 0 | 1 | 1      |
| 1 | 1 | 0 | 1      |
| 1 | 1 | 1 | 1      |

(A truth table is printed for expressions with ≤ 6 variables; an Advanced: line is printed only when a pattern such as XOR / implication / equivalence is recognized.)

Your first optimize (library)

using LogicalOptimizer;

var optimizer = new BooleanExpressionOptimizer();
var result = optimizer.OptimizeExpression("a & b | a & c", includeMetrics: true);

Console.WriteLine(result.Original);   // a & b | a & c
Console.WriteLine(result.Optimized);  // a & (b | c)
Console.WriteLine(result.CNF);        // a & (b | c)
Console.WriteLine(result.DNF);        // a & b | a & c
Console.WriteLine(string.Join(", ", result.Variables));  // a, b, c

// The minimality provenance is explicit:
Console.WriteLine(result.MinimizationStatus);  // MinimalProven (≤10 vars)

// Every result is verified equivalent to the input before return:
Console.WriteLine(result.IsEquivalent());      // True

Building formulas programmatically always goes through FormulaFactory, the single construction entry point (results are canonical and interned):

var f = new FormulaFactory();
var parsed = f.Parse("c & a & b");
Console.WriteLine(parsed);                          // a & b & c  (canonical order)

var built = f.And(f.Variable("a"), f.Variable("b"), f.Variable("c"));
Console.WriteLine(ReferenceEquals(parsed, built));  // True (interning)

Next steps

Every code example across these articles is mirrored by an executed, asserted test in LogicalOptimizer.Tests/Documentation/DocExamplesTests.cs, so the outputs shown are real.

Edit this page