Class Transformations

Namespace: LogicalOptimizer

Assembly: LogicalOptimizer.dll

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.

public static class Transformations

Inheritance: object

Transformations

Inherited Members: object.Equals(object)

object.Equals(object, object)

object.GetHashCode()

object.GetType()

object.MemberwiseClone()

object.ReferenceEquals(object, object)

object.ToString()

Methods

MinimizeDnfHeuristic(AstNode, int, CancellationToken)

Espresso-style heuristic DNF minimization on cube lists (EXPAND → IRREDUNDANT → REDUCE with exact cofactor-tautology validation) — no 2^n table, so it applies far beyond the exact zone. The input must be a flat sum of products over plain literals; anything else is returned unchanged. Sound by construction: only cover-preserving steps are ever applied, and the step budget merely stops further improvement.

public static AstNode MinimizeDnfHeuristic(AstNode dnf, int stepLimit = 500000, CancellationToken cancellationToken = default)

Parameters

dnf AstNode
stepLimit int
cancellationToken CancellationToken

Returns

AstNode

SubsumeCnf(AstNode)

CNF subsumption: remove every clause absorbed by a more general one ((a | b) & a → a). The input is treated as a conjunction of clauses.

public static AstNode SubsumeCnf(AstNode formula)

Parameters

formula AstNode

Returns

AstNode

SubsumeDnf(AstNode)

DNF subsumption: remove every term absorbed by a more general one (a & b | a → a). The input is treated as a disjunction of terms.

public static AstNode SubsumeDnf(AstNode formula)

Parameters

formula AstNode

Returns

AstNode

ToAlgebraicNormalForm(AstNode, CancellationToken)

Convert a formula to its Algebraic Normal Form (ANF / Zhegalkin / Reed–Muller polynomial): the unique XOR of AND-monomials over the variables. Coefficients come from the fast Möbius transform over the truth table, so this is 2^n work capped at MaxVariables variables (an ArgumentException is thrown beyond the cap) and honors the supplied cancellationToken. The empty monomial renders as the constant 1; the everywhere-false function as the constant 0.

public static AstNode ToAlgebraicNormalForm(AstNode formula, CancellationToken cancellationToken = default)

Parameters

formula AstNode
cancellationToken CancellationToken

Returns

AstNode