Enum CnfMode

Namespace
LogicalOptimizer
Assembly
LogicalOptimizer.dll

How the CNF artifact is produced.

public enum CnfMode

Fields

Equivalent = 0

Equivalent CNF over the original variables. In the exact-minimization range it is a minimum-cover POS whose proof status is reported by CnfMinimizationStatus (proven in the ≤10 guarantee zone, possibly budget-limited at 11–12); beyond the threshold it is budgeted distribution and may end as TooLarge.

Tseitin = 1

Equisatisfiable CNF via Tseitin transformation: always linear in expression size, introduces auxiliary _tN variables. Never TooLarge.

Edit this page