Class PseudoBooleanEncoder

Namespace

LogicalOptimizer

Assembly

LogicalOptimizer.Sat.dll

Linear pseudo-Boolean constraints (sum of positive-weighted literals compared to a bound). The parameterless overloads use a decision-diagram expansion with memoization — the classic BDD encoding, polynomial for practical weight ranges. Overloads taking a PseudoBooleanEncoding select from a portfolio of semantically equivalent encodings and report the size they introduced.

public static class PseudoBooleanEncoder

Inheritance

object

PseudoBooleanEncoder

Inherited Members

object.Equals(object)

object.Equals(object, object)

object.GetHashCode()

object.GetType()

object.MemberwiseClone()

object.ReferenceEquals(object, object)

object.ToString()

Methods

AtLeast(CnfBuilder, IReadOnlyList<int>, IReadOnlyList<long>, long)

Σ weight_i · literal_i ≥ bound. Weights must be positive (stable default output).

public static void AtLeast(CnfBuilder builder, IReadOnlyList<int> literals, IReadOnlyList<long> weights, long bound)

Parameters

builder CnfBuilder

literals IReadOnlyList<int>

weights IReadOnlyList<long>

bound long

AtLeast(CnfBuilder, IReadOnlyList<int>, IReadOnlyList<long>, long, PseudoBooleanEncoding)

Σ weight_i · literal_i ≥ bound, encoded with the chosen strategy.

public static EncodingStats AtLeast(CnfBuilder builder, IReadOnlyList<int> literals, IReadOnlyList<long> weights, long bound, PseudoBooleanEncoding encoding)

Parameters

builder CnfBuilder

literals IReadOnlyList<int>

weights IReadOnlyList<long>

bound long

encoding PseudoBooleanEncoding

Returns

EncodingStats

AtMost(CnfBuilder, IReadOnlyList<int>, IReadOnlyList<long>, long)

Σ weight_i · literal_i ≤ bound. Weights must be positive (stable default output).

public static void AtMost(CnfBuilder builder, IReadOnlyList<int> literals, IReadOnlyList<long> weights, long bound)

Parameters

builder CnfBuilder

literals IReadOnlyList<int>

weights IReadOnlyList<long>

bound long

AtMost(CnfBuilder, IReadOnlyList<int>, IReadOnlyList<long>, long, PseudoBooleanEncoding)

Σ weight_i · literal_i ≤ bound, encoded with the chosen strategy. Returns the clauses / auxiliary variables the call introduced. Passing DynamicProgramming reproduces the default output.

public static EncodingStats AtMost(CnfBuilder builder, IReadOnlyList<int> literals, IReadOnlyList<long> weights, long bound, PseudoBooleanEncoding encoding)

Parameters

builder CnfBuilder

literals IReadOnlyList<int>

weights IReadOnlyList<long>

bound long

encoding PseudoBooleanEncoding

Returns

EncodingStats