Class PseudoBooleanProblem

Namespace: LogicalOptimizer

Assembly: LogicalOptimizer.Formats.dll

A pseudo-Boolean (0/1 integer linear) problem parsed from OPB: an optional linear min: objective (preserved for round-tripping but not optimized by the decision Solve(int, CancellationToken)) and a list of linear constraints. Feasibility is decided by encoding every constraint to CNF through PseudoBooleanEncoder / CardinalityEncoder and handing the result to the in-house SatSolver.

public sealed class PseudoBooleanProblem

Inheritance: object

PseudoBooleanProblem

Inherited Members: object.Equals(object)

object.Equals(object, object)

object.GetHashCode()

object.GetType()

object.ReferenceEquals(object, object)

object.ToString()

Properties

Constraints

public IReadOnlyList<PseudoBooleanConstraint> Constraints { get; }

Property Value

IReadOnlyList<PseudoBooleanConstraint>

Objective

The linear minimization objective, or null when the instance has none.

public IReadOnlyList<(long Coefficient, int Literal)>? Objective { get; }

Property Value

IReadOnlyList<(long Coefficient, int Literal)>

VariableCount

Declared number of variables (indices 1..VariableCount).

public int VariableCount { get; }

Property Value

int

Methods

Solve(int, CancellationToken)

Decide whether this pseudo-Boolean instance is feasible.

public SatResult Solve(int maxConflicts = 1000000, CancellationToken cancellationToken = default)

Parameters

maxConflicts int
cancellationToken CancellationToken

Returns

SatResult

ToSolver()

Encode all constraints to CNF and build a SatSolver whose satisfiability is exactly the feasibility of this pseudo-Boolean instance. The objective is ignored: this is a decision, not an optimization, encoding.

public SatSolver ToSolver()

Returns

SatSolver

Write(TextWriter)

Write this problem back out as OPB text (round-trips through the parser): the * #variable= n #constraint= m header, an optional min: objective, and one terms OP bound ; line per constraint.

public void Write(TextWriter writer)

Parameters

writer TextWriter