Class MaxSatResult

Namespace

LogicalOptimizer

Assembly

LogicalOptimizer.Sat.dll

Outcome of a MaxSAT optimization.

public sealed class MaxSatResult

Inheritance

object

MaxSatResult

Inherited Members

object.Equals(object)

object.Equals(object, object)

object.GetHashCode()

object.GetType()

object.ReferenceEquals(object, object)

object.ToString()

Properties

Cost

Total weight of falsified soft clauses (optimal when Status is Optimal).

public long Cost { get; }

Property Value

long

LowerBound

A proven lower bound on the optimal cost: LowerBound ≤ optimum ≤ UpperBound. When Status is Optimal the two bounds coincide with Cost; when the search stops early (Unknown) they bracket the still-unknown optimum. Undefined when no model exists (HardClausesUnsatisfiable).

public long LowerBound { get; }

Property Value

long

Status

public MaxSatStatus Status { get; }

Property Value

MaxSatStatus

UpperBound

The cost of the best model found so far (the incumbent), an upper bound on the optimum. Equals Cost whenever a model is available. Never a proven optimum unless Status is Optimal.

public long UpperBound { get; }

Property Value

long

Values

Variable values indexed 1..variableCount; null when hard clauses are UNSAT.

public bool[]? Values { get; }

Property Value

bool[]

Methods

GetValue(int)

public bool GetValue(int variable)

Parameters

variable int

Returns

bool