Enum PseudoBooleanEncoding

Namespace: LogicalOptimizer

Assembly: LogicalOptimizer.Sat.dll

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.

public enum PseudoBooleanEncoding

Fields

Auto = 0: Measure the applicable encodings and pick the smallest (guaranteed ≤ the default).
BinaryMerge = 2: Binary adder network (weights summed as binary numbers) compared against the bound.
DynamicProgramming = 1: The decision-diagram / dynamic-programming expansion. The stable default.
GeneralizedTotalizer = 3: Generalized totalizer (Joshi et al. 2015): a weighted unary-counter tree, capped at bound+1.