Namespace LogicalOptimizer

Classes

AndNode: N-ary conjunction node. The constructors are low-level: no flattening, sorting, deduplication or folding is performed — build through And(params AstNode[]) to get canonical trees.

AstFormatter: Single precedence-based renderer for expression trees. Every node's ToString delegates here, so parenthesization rules live in exactly one place: a child is wrapped in parentheses only when its precedence is lower than its parent requires. N-ary connectives render flat (a & b & c), an OR under an AND is parenthesized, derived binary operators (XOR/NAND/NOR/ EQV/IMP) parenthesize any compound child because they have no precedence in the input grammar, and NOT renders as !x for atomic operands and !(...) for compound ones.

AstMetrics: Size and shape metrics over expression trees. Cost model: an n-ary And/Or node counts as ONE node (and one operator) regardless of its operand count — the flat list is a single connective, not a chain of binary ones.

AstNode

AstVisualizer: Renders an AST as a human-readable tree (box-drawing characters) for diagnostics.

BackboneResult: Result of a backbone query.

BddEquivalenceChecker: BDD backend: builds both sides in one manager and compares canonical roots. Returns Unknown when the node budget is exceeded (no counterexample extraction).

BinaryDecisionDiagram

Reduced Ordered Binary Decision Diagram over a variable order, with a shared unique table (hash-consing) and memoized ite. Because ROBDDs are canonical, two expressions are equivalent exactly when they build to the same node — ideal for repeated equivalence queries against one baseline. A node budget turns pathological orderings into a clean exception instead of memory blowup (callers can fall back to the SAT-based EquivalenceChecker).

The diagram uses CUDD-style complement edges: an "edge" is an int that packs a node index and a complement bit (the low bit); a function and its negation share the very same node, halving memory, and Negate(int) is an O(1) bit flip. There is a single terminal node (ONE); FALSE is the complemented edge to it. The canonical invariant is that the THEN (high) edge of every stored node is always regular (non-complemented); when a node would be built with a complemented then-edge, both children are complemented and a complemented edge to the normalized node is returned. That single rule keeps the representation canonical, so equivalence is still edge equality.

Variable position is decoupled from variable identity: the stored Variable field of a node is a stable variable id, and LogicalOptimizer.BinaryDecisionDiagram._varLevel maps each id to its current level (position, top to bottom). That indirection lets BuildWithSiftedOrder(AstNode, int, int, CancellationToken) reorder variables in place with adjacent-level swaps instead of rebuilding the whole diagram.

BinaryNode: Base class for the derived binary connectives (ImpNode, XorNode, NandNode, NorNode, EqvNode) that live outside the canonical core. The core connectives And/Or are n-ary (NaryNode); Import(AstNode) decomposes derived nodes into And/Or/Not. Nodes are immutable and the hash code is computed once in the constructor.

BooleanExpressionExporter: Exporter for boolean expressions to various standard formats

BooleanExpressionOptimizer

CSharpExpressionExporter: Exports boolean expressions as compilable C# code

CardinalityEncoder: Cardinality constraints over literals. The parameterless overloads encode with the sequential counter (Sinz 2005): O(n·k) clauses and auxiliaries, unit-propagation preserves generalized arc consistency. Overloads taking a CardinalityEncoding select from a portfolio of semantically equivalent encodings and report the size they introduced.

CircuitSerializationException

Experimental (until v4). Raised when a compiled-circuit binary blob (the Save/Load format shared by BinaryDecisionDiagram and DnnfCircuit) is malformed: a bad magic marker, an unrecognised — in particular a newer, forward — format version, the wrong engine byte, a checksum mismatch, a truncated stream, or a structurally invalid node table (an out-of-range index, a non-topological reference, an invalid root or terminal). A checksum only catches corruption; the loader still validates structure and reports every violation as this typed exception rather than misreading the input. A resource limit hit while loading is reported separately as NodeBudgetExceededException, never as this type.

The binary format is experimental and carries no cross-version compatibility guarantee before v4 other than the version gate, which refuses a blob written by a newer build.

CnfBuilder: Accumulates a CNF (clauses over 1-based DIMACS literals) with auxiliary-variable allocation, for feeding encoders and the SatSolver.

CnfProblem: A CNF satisfiability problem parsed from DIMACS: a fixed variable count and a list of clauses over 1-based signed literals (a positive literal v asserts variable v, a negative literal -v its negation). Hands off directly to the in-house SatSolver; also convertible to an AstNode for the BDD / d-DNNF engines.

ComputationBudgetExceededException: Raised when an exact algorithm gives up because it hit an explicit work budget (e.g. Quine–McCluskey prime-generation pair-comparison limit) rather than because of a programming error. It derives from InvalidOperationException for backward compatibility with callers that caught the broader type, but its distinct identity lets the facade tell a budget exhaustion (report MinimizationStatus.BudgetExceeded) apart from a genuine invariant violation, which must never be silently swallowed.

ConstantNode: Boolean constant (0 or 1). A dedicated node type so that algorithms never have to remember that some "variables" are not really variables.

CsvTruthTableParser: Parser for CSV truth tables that converts them to boolean expressions

DimacsParser: Streaming parser for the DIMACS CNF format: c comment lines, a p cnf <nvars> <nclauses> header, and clauses of space-separated non-zero signed integers each terminated by 0 (a clause may span several lines). Reads line by line from the TextReader and never materializes the whole input; oversized variable indices or an overrun of ParseTokenLimit raise ComputationBudgetExceededException, and any other malformation raises FormatParseException with the offending line/column.

DnnfCircuit

A compiled d-DNNF (deterministic, decomposable Negation Normal Form) circuit for a boolean formula. Compilation happens once (see KnowledgeCompilation); afterwards exact model counting, weighted model counting and model enumeration are all linear in the circuit size.

The circuit is compiled over the full equisatisfiable Tseitin CNF of the input formula (input variables plus functionally-determined gate auxiliaries). Because the full biconditional Tseitin encoding is equi-count over the input variables — every satisfying input assignment extends to exactly one auxiliary assignment — the model count of the whole circuit equals the model count of the original formula over its input variables, with no projection needed. Variables and EnumerateModels(CancellationToken) expose only the original input variables; the auxiliaries are projected away.

EquivalenceCheckResult: Verdict of an equivalence query. AreEquivalent is null when the conflict budget ran out before a proof either way (only possible far beyond the truth-table range).

EquivalenceChecker: Equivalence of two boolean expressions at any scale. Small expressions are compared by truth table; larger ones through a miter (XOR of both sides) put through the Tseitin transformation and the built-in SAT solver — UNSAT proves equivalence without enumerating 2^n rows, SAT yields a concrete counterexample.

EqvNode: Tree node for equivalence (biconditional) operation

ExternalSatEquivalenceChecker

Equivalence backend that routes the SAT-miter query through a user-supplied IExternalSatSolver (e.g. a process adapter around CaDiCaL or Kissat) while everything else — miter construction, Tseitin encoding, counterexample decoding — stays in-library. Opt-in only: the default backends remain HybridEquivalenceChecker and BddEquivalenceChecker on the embedded engines.

Trust model: a Satisfiable verdict (non-equivalence) is VERIFIED — the returned model must satisfy the miter CNF (checked in linear time via IsSatisfiedBy(IReadOnlyList<int>)), otherwise the solver is lying or broken and an InvalidOperationException is thrown. An Unsatisfiable verdict (equivalence) is TRUSTED — refuting it cheaply is not possible; demand a DRAT/LRAT proof from the solver and check it out of band if the equivalence claim must be independently verifiable.

ExternalSatProblem: A one-shot CNF satisfiability query for an IExternalSatSolver. Literals follow the DIMACS convention: variables are 1-based, a positive literal v asserts variable v, a negative literal -v its negation. Optional assumptions are unit constraints for this query; adapters that speak plain DIMACS may append them as unit clauses (equivalent for a single call), which is exactly what ToDimacs() does.

ExternalSatResult: Verdict of an IExternalSatSolver query, reusing the embedded solver's SatResult vocabulary. A Satisfiable verdict carries the model; Unsatisfiable and Unknown carry nothing.

FormatParseException: Raised when a standard-format stream (DIMACS CNF, WCNF or OPB) is syntactically malformed. Carries the 1-based Line and Column of the offending token so callers can point at the exact position in the input. A resource limit being hit is reported separately as ComputationBudgetExceededException, never as this type.

FormulaAnalysis: Semantic queries over a formula, built on the incremental SAT solver: backbone (literals forced in every model), projected model counting and enumeration, and backbone-based simplification. All queries work at any scale — no 2^n enumeration is involved.

FormulaFactory: LogicNG-style formula construction: n-ary And/Or with automatic flattening, duplicate-operand removal, constant folding, complement folding (x and !x collapse the connective), canonical operand ordering and structural interning — equal formulas built through the factory are the SAME instance, so reference equality works as structural equality and repeated subformulas share memory. Because operands are sorted with a stable canonical key at construction time, structural (order-sensitive) equality is effectively commutative for factory-built trees. The intern table is a ConcurrentDictionary<TKey, TValue>, so a factory instance may be shared across threads.

FormulaParseException: Thrown when a string is not a valid boolean expression. Derives from ArgumentException for backward compatibility, and exposes a structured Diagnostic (position, length, expected tokens, machine-readable code and a caret snippet). Use TryParse(string, out AstNode?, out ParseDiagnostic?) to handle invalid input without exceptions.

HybridEquivalenceChecker: Default backend: exhaustive truth-table comparison up to the guard range, SAT-based miter proof beyond it. Verdicts are exact; Unknown appears only when the conflict budget runs out on very large instances.

ImpNode: Implication node representing logical implication operation

KnowledgeCompilation: Knowledge compilation entry point: turn a boolean formula into a d-DNNF circuit that answers model-counting and enumeration queries in time linear in the circuit size.

MaxSatResult: Outcome of a MaxSAT optimization.

MaxSatSolver

Weighted partial MaxSAT: hard clauses must hold, soft clauses carry positive weights and the total weight of falsified softs is minimized. Two algorithms are available (see MaxSatAlgorithm):

Linear — each soft clause gets a relaxation literal and a linear search tightens a pseudo-Boolean bound on the relaxation weights until UNSAT proves optimality;
CoreGuided — an MSU3-style lower-bound search that solves under soft-selector assumptions, extracts UNSAT cores and relaxes only the cores with a cardinality / pseudo-Boolean bound raised round by round.

Built entirely on the in-house solver and encoders — no dependencies. Either algorithm, run to completion, returns the same PROVEN optimum; an incumbent found under a spent budget is reported as Unknown, never as Optimal.

MultiOutputFunction: One output of a multi-output table. The don't-care set is shared (unspecified rows).

MultiOutputTable: A multi-output truth table: shared inputs, one ON-set per output.

NandNode: Tree node for NAND (NOT-AND) operation

NaryNode: Base class for the n-ary associative connectives of the canonical core (AndNode and OrNode). Holds a flat, immutable operand list of at least two entries. Structural equality is order-sensitive over the operand list (operand order is canonical for factory-built trees), and the hash code is computed once in the constructor — trees are fully immutable.

NodeBudgetExceededException: Raised when a decision-diagram / knowledge-compilation build gives up because it hit an explicit node budget (BDD or d-DNNF), rather than because of a programming error. It derives from InvalidOperationException for backward compatibility with callers that caught the broader type, but its distinct identity lets a fallback path (try the next variable order, return an Unknown verdict) tell a budget exhaustion apart from a genuine invariant violation, which must never be silently swallowed.

NorNode: Tree node for NOR (NOT-OR) operation

NormalFormTooLargeException: Raised when a distribution-based normal-form conversion (equivalent CNF/DNF) is abandoned because the expression expands past its distribution-step budget, rather than because of a programming error. It derives from InvalidOperationException for backward compatibility, but its distinct identity lets callers fall back cleanly (mark the artifact TooLarge, or switch to the linear-size Tseitin encoding) without also swallowing a genuine invariant violation.

NotNode: Logical negation node. Immutable; hash code is computed once in the constructor.

OpbParser: Streaming parser for the OPB (pseudo-Boolean) format: comment lines (including the #variable= N #constraint= M header), an optional linear objective min: +c1 x1 -c2 x2 ... ;, and linear constraints +c1 x1 -c2 x2 ... OP b ; with OP one of >=, <=, =. Variables are written x<n> and may be negated as ~x<n>; a statement may span several lines up to its terminating ;. Reads line by line and never materializes the whole input; budget/variable overruns raise ComputationBudgetExceededException and other malformation raises FormatParseException.

OptimizationMetrics

OptimizationOptions: Which artifacts OptimizeExpression(string, OptimizationOptions) should produce. The optimized expression itself is always computed; everything else is opt-in so callers do not pay for normal forms they never read.

OptimizationQualityAnalyzer: Boolean expression optimization quality analyzer

OptimizationQualityAnalyzer.QualityMetrics: Optimization quality metrics

OptimizationResult

OptimizationTrace

Opt-in diagnostic record of how an optimization result was reached: which engine was chosen and why, which budgets applied, which candidates were produced, which one was adopted or rejected and on what cost, how equivalence and minimality were discharged, and why a run ended on a fallback or a non-proven status.

Enable it with IncludeTrace and read it from Trace. It is a diagnostic aid, not a stability contract: entry wording and ordering may change between minor versions, so log it or display it rather than asserting on exact text.

OptimizationTraceEntry: One recorded decision from an optimization run. Message explains the decision in words; Data carries the same facts as machine-readable key/value pairs so a production log or diagnostics UI can filter on them.

OrNode: N-ary disjunction node. The constructors are low-level: no flattening, sorting, deduplication or folding is performed — build through Or(params AstNode[]) to get canonical trees.

ParseDiagnostic: Structured, machine-readable description of a parse failure, produced by TryParse(string, out AstNode?, out ParseDiagnostic?) and carried by FormulaParseException. It reports where the error is (Position, Length), a stable Code, the tokens that would have been valid (Expected), and a caret Snippet for display.

PartialTruthTable: A partially specified single-output truth table parsed from CSV. Rows absent from the CSV are don't-care minterms. Bit convention: bit j of a minterm index is the value of Variables[j], variables sorted alphabetically.

ProjectedModelCountResult: Result of CountProjectedModels(AstNode, IReadOnlyCollection<string>, ResourceBudget?, CancellationToken). Count is non-null exactly when Status is Exact: a partial (budget-limited) run never carries a count that could be mistaken for exact.

PseudoBooleanConstraint: A single linear pseudo-Boolean constraint Σ coefficientᵢ · literalᵢ OP bound. A literal is a 1-based signed variable index: a positive value v is xv, a negative value -v is the negation ~xv. Coefficients may be negative.

PseudoBooleanEncoder: Linear pseudo-Boolean constraints (sum of positive-weighted literals compared to a bound). The parameterless overloads use a decision-diagram expansion with memoization — the classic BDD encoding, polynomial for practical weight ranges. Overloads taking a PseudoBooleanEncoding select from a portfolio of semantically equivalent encodings and report the size they introduced.

PseudoBooleanProblem: A pseudo-Boolean (0/1 integer linear) problem parsed from OPB: an optional linear min: objective (preserved for round-tripping but not optimized by the decision Solve(int, CancellationToken)) and a list of linear constraints. Feasibility is decided by encoding every constraint to CNF through PseudoBooleanEncoder / CardinalityEncoder and handing the result to the in-house SatSolver.

ResourceBudget

Unified work budgets for the potentially expensive engines. Every limit has a safe default; callers with harder latency requirements can tighten them per call via OptimizationOptions.Budget. Exhausting a budget never produces a wrong result — each engine falls back (heuristic simplification, Unknown verdict) or throws a documented exception.

Scale contract of the fixed limits: expressions accept up to 100 variables overall; truth-table-based operations (TruthTable, exact minimization input) cap at 20; exact minimization is guaranteed ≤10, budgeted ≤12; the SAT-based prime cover extends to 24; SAT/BDD/Tseitin engines have no variable cap, only these work budgets.

SatSolver: Self-contained CDCL SAT solver: two-watched literals, 1UIP clause learning, heap-based VSIDS activities, Luby restarts, LBD-driven learnt-clause database reduction, bounded subsumption preprocessing, incremental solving under assumptions with unsat cores, and optional DRAT proof logging. Variables are 1-based DIMACS indices; a positive literal v asserts variable v, a negative literal -v its negation. No dependencies.

Transformations: Standalone formula transformations usable outside the full optimization pipeline. Subsumption drops absorbed terms/clauses without any truth-table work, so it applies at any scale.

TruthTable: Class for generating and working with truth tables

TruthTableMinimizer: Exact two-level minimization: Quine–McCluskey prime implicant generation followed by an exact minimum cover search (essential primes + branch-and-bound, greedy fallback past a work limit). Cost order: total literals, then term count. Minterm bit convention: bit j of a minterm index is the value of variables[j] (variables are expected in sorted order).

TseitinCnf: Equisatisfiable CNF produced by LogicalOptimizer.TseitinConverter. Variable indices are 1-based DIMACS style: input variables first (sorted by name), auxiliary gate variables after.

VariableNode: Named boolean variable. Immutable; hash code is computed once in the constructor.

WcnfParser

Streaming parser for the WCNF (weighted partial MaxSAT) format. Two dialects are accepted, the classic one first and by default:

Classic — a p wcnf <nvars> <nclauses> <top> header (the trailing top is optional; when absent every clause is soft), then one <weight> <lit...> 0 clause per record (records may span lines). A clause whose weight equals top is hard.
New-style (MaxSAT Evaluation 2022+) — no p line; one clause per line, a leading h marking a hard clause and a leading positive integer marking a soft clause of that weight. A trailing 0 is tolerated but not required. top is synthesized as (Σ soft weights)+1 so the writer can round-trip through the classic form.

c comment lines are ignored. Reads line by line and never materializes the whole input; budget/variable overruns raise ComputationBudgetExceededException and other malformation raises FormatParseException.

WeightedCnfProblem: A weighted partial MaxSAT problem parsed from WCNF: hard clauses that must hold and soft clauses that carry a positive weight, the total weight of the falsified softs being minimized. Hands off directly to the in-house MaxSatSolver. Top is the hard-clause weight sentinel of the classic format, preserved so the writer round-trips.

XorNode: Tree node for exclusive OR (XOR) operation

Structs

EncodingStats: The size an encoding call added to a CnfBuilder: the number of clauses and auxiliary variables introduced. Available from the encoding-selecting overloads for diagnostics and for comparing encodings; the same numbers are also readable directly off Clauses.Count and VariableCount deltas.

Interfaces

IEquivalenceChecker: Pluggable equivalence backend. The core library ships two implementations: HybridEquivalenceChecker (truth table small / SAT miter large) and BddEquivalenceChecker (canonical diagrams, best for repeated queries). External adapters (e.g. an optional Z3 package) implement the same contract for production verification at scales beyond the built-in budgets.

IExternalSatSolver

Seam for plugging an external SAT solver (CaDiCaL, Kissat, a solver behind a service, ...) into consumers that otherwise use the embedded CDCL solver. The contract is deliberately minimal and one-shot — CNF in, verdict out — not an incremental IPASIR binding: the library keeps parsing, Tseitin encoding and counterexample decoding, and only the raw CNF query is handed off.

Trust model (asymmetric, enforced by the in-library consumers such as ExternalSatEquivalenceChecker): a Satisfiable verdict must come with a model, and the model IS verified against the CNF (cheap, linear in the clause count) — a bogus model is detected and rejected. A Unsatisfiable verdict cannot be checked cheaply and is TRUSTED; if that matters, run a proof-producing solver and check its DRAT/LRAT certificate out of band (e.g. with drat-trim).

Enums

CardinalityEncoding: Which CNF encoding a cardinality constraint (CardinalityEncoder) is expanded with. Auto measures the applicable encodings and picks the smallest (by clauses + auxiliary variables); it may change its choice between minor releases, but only with a CHANGELOG note and never worse than the stable default beyond a documented threshold on the fixed calibration corpus. All values are semantically equivalent — they differ only in size and propagation strength.

CnfEncodingStyle: Gate-encoding style for LogicalOptimizer.TseitinConverter.

CnfMode: How the CNF artifact is produced.

ComputationStatus: Outcome of a potentially expensive computation on the result object.

MaxSatAlgorithm: Which MaxSAT search the solver runs. All values return the SAME proven optimum on the instances they solve to completion; they differ only in the search path (and therefore in which instances stay within a given conflict budget).

MaxSatStatus

MinimizationStatus: Provenance of the minimality claim for an optimization result. Refers to the two-level cover cost model: total literals first, then term count. The returned optimized (multi-level) expression never has more literals than that cover.

OptimizationTraceCategory: What kind of decision a OptimizationTraceEntry records.

ParseErrorCode: Stable, machine-readable classification of a formula parse failure.

ProjectedCountStatus: Outcome kind of a CountProjectedModels(AstNode, IReadOnlyCollection<string>, ResourceBudget?, CancellationToken) query.

PseudoBooleanComparison: The comparison operator of a pseudo-Boolean constraint.

PseudoBooleanEncoding: Which CNF encoding a pseudo-Boolean constraint (PseudoBooleanEncoder) is expanded with. Auto measures the applicable encodings and picks the smallest; see the note on Auto for the between-release policy. All values are semantically equivalent.

SatResult