Class CardinalityEncoder

Namespace

LogicalOptimizer

Assembly

LogicalOptimizer.Sat.dll

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.

public static class CardinalityEncoder

Inheritance

object

CardinalityEncoder

Inherited Members

object.Equals(object)

object.Equals(object, object)

object.GetHashCode()

object.GetType()

object.MemberwiseClone()

object.ReferenceEquals(object, object)

object.ToString()

Methods

AtLeastK(CnfBuilder, IReadOnlyList<int>, int)

At least k of the literals are true (the stable default output).

public static void AtLeastK(CnfBuilder builder, IReadOnlyList<int> literals, int k)

Parameters

builder CnfBuilder

literals IReadOnlyList<int>

k int

AtLeastK(CnfBuilder, IReadOnlyList<int>, int, CardinalityEncoding)

At least k of the literals are true, encoded with the chosen strategy.

public static EncodingStats AtLeastK(CnfBuilder builder, IReadOnlyList<int> literals, int k, CardinalityEncoding encoding)

Parameters

builder CnfBuilder

literals IReadOnlyList<int>

k int

encoding CardinalityEncoding

Returns

EncodingStats

AtMostK(CnfBuilder, IReadOnlyList<int>, int)

At most k of the literals are true (sequential counter — the stable default output).

public static void AtMostK(CnfBuilder builder, IReadOnlyList<int> literals, int k)

Parameters

builder CnfBuilder

literals IReadOnlyList<int>

k int

AtMostK(CnfBuilder, IReadOnlyList<int>, int, CardinalityEncoding)

At most k of the literals are true, encoded with the chosen strategy. Returns the clauses / auxiliary variables the call introduced. Passing SequentialCounter reproduces the default output.

public static EncodingStats AtMostK(CnfBuilder builder, IReadOnlyList<int> literals, int k, CardinalityEncoding encoding)

Parameters

builder CnfBuilder

literals IReadOnlyList<int>

k int

encoding CardinalityEncoding

Returns

EncodingStats

ExactlyK(CnfBuilder, IReadOnlyList<int>, int)

Exactly k of the literals are true (the stable default output).

public static void ExactlyK(CnfBuilder builder, IReadOnlyList<int> literals, int k)

Parameters

builder CnfBuilder

literals IReadOnlyList<int>

k int

ExactlyK(CnfBuilder, IReadOnlyList<int>, int, CardinalityEncoding)

Exactly k of the literals are true, encoded with the chosen strategy.

public static EncodingStats ExactlyK(CnfBuilder builder, IReadOnlyList<int> literals, int k, CardinalityEncoding encoding)

Parameters

builder CnfBuilder

literals IReadOnlyList<int>

k int

encoding CardinalityEncoding

Returns

EncodingStats