LogicalOptimizer
A .NET toolkit and CLI for parsing, optimizing, and transforming Boolean expressions, with no third-party runtime dependency — with provable minimization and mandatory equivalence verification of every result.
LogicalOptimizer covers exact Quine–McCluskey minimization with an explicit proof status, a built-in CDCL SAT solver, an ROBDD engine, d-DNNF knowledge compilation, Tseitin/Plaisted–Greenbaum CNF, cardinality/pseudo-Boolean/MaxSAT encodings, and DIMACS/BLIF/Verilog/LaTeX exporters — in one managed package set with no third-party runtime dependency. How that scope compares against Z3, LogicNG, SymPy and PyEDA, measured on a pinned corpus with pinned competitor versions: comparison results.
Note
Two guarantees the library never trades away: no third-party runtime dependency in any shipped package, and explainability plus mandatory verification — every returned result is checked equivalent to the input (by truth table up to 12 variables, by SAT miter beyond). Both terms are defined, and linked to the test or CI check that backs them, in CLAIMS.md.
Get started
# Library (facade pulls in the four core engine packages; add .Dnnf separately)
dotnet add package LogicalOptimizer
# CLI as a global dotnet tool -> command: logical-optimizer
dotnet tool install -g LogicalOptimizer.Cli
logical-optimizer "a & b | a & c"
# Optimized: a & (b | c)
Documentation map
| Section | What it covers |
|---|---|
| Introduction / Getting Started | What the library is, install, first example |
| Formula construction & the AST | FormulaFactory, n-ary AST, AstFormatter, AstMetrics |
| Optimizer & options | BooleanExpressionOptimizer, OptimizationOptions, AIG rewriting (v3.0 default), quality analysis |
| Operation contracts & statuses | MinimizationStatus, ComputationStatus, what "provably minimal" means |
| Resource budgets & the zone model | ResourceBudget, PerformanceValidator, variable-count routing |
| Diagnostic trace | --trace / IncludeTrace: which engine ran and why, budgets, candidate costs, adoption and fallback |
| Normal forms & transformations | CNF / DNF / ANF, Transformations, equisatisfiable Tseitin CNF, TruthTable |
| Two-level minimization | TruthTableMinimizer, don't-cares, CSV parsing, multi-output tables |
| SAT solving, cardinality, PB & MaxSAT | SatSolver, assumptions, unsat cores, DRAT, CardinalityEncoder, PseudoBooleanEncoder, MaxSatSolver |
| Binary decision diagrams | BinaryDecisionDiagram: model counting, enumeration, ordering |
| Knowledge compilation & model counting | KnowledgeCompilation / DnnfCircuit: exact/weighted #SAT |
| Equivalence & backbones | FormulaAnalysis, EquivalenceChecker, CheckWithProof, pluggable checkers |
| Export formats | DIMACS / BLIF / Verilog / LaTeX / CSV / C# code generation |
| Packages & architecture | The 7-package split, layering, FormulaFactory, canonical n-ary AST |
| CLI usage | Every flag with verified example outputs, plus the solve / maxsat / solve-pb / count standard-format verbs |
| Migration to v2.0 | Breaking changes and how to adapt |
| Benchmarks & comparison | Result size and timing against SymPy and PyEDA on a pinned corpus, and the BenchmarkDotNet suite |
| Choosing a tool | Scenario by scenario against Z3, ABC, LogicNG, SymPy and PyEDA — including where this project is weakest |
| Case studies | Measured end-to-end examples |
| Testing overview | The structured functional suite and the ten techniques layered on it |
| API Reference | Generated from the XML doc comments of the seven library packages |
Every code example across these articles is mirrored by an executed, asserted test in
LogicalOptimizer.Tests/Documentation/DocExamplesTests.cs — the outputs shown are real.
Where it fits
LogicalOptimizer is a propositional Boolean reasoning toolkit for .NET. It is not a replacement for Z3 (full SMT), ABC (logic synthesis), CUDD (industrial BDD), or a complete Espresso. What it offers instead is a specific combination: everything in-house and pure managed, and every optimization result verified equivalent to the input with an explicit minimality status. Whether that combination fits your case — and where the alternatives are the better choice — is worked through in Choosing a tool.