Enum CardinalityEncoding

Namespace

LogicalOptimizer

Assembly

LogicalOptimizer.Sat.dll

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.

public enum CardinalityEncoding

Fields

Auto = 0

Measure the applicable encodings and pick the smallest (guaranteed ≤ the default).

Pairwise = 1

Binomial encoding: one clause per (k+1)-subset, no auxiliaries. Best for tiny n / k.

Product = 3

2D product encoding (Chen 2010) for at-most-one; falls back to the totalizer for k≠1.

SequentialCounter = 2

Sequential counter (Sinz 2005): O(n·k) clauses and auxiliaries. The stable default.

Totalizer = 4

Totalizer (Bailleux & Boufkhad 2003): a capped unary-counter tree, strong propagation.