Class ExternalSatResult

Namespace

LogicalOptimizer

Assembly

LogicalOptimizer.Sat.dll

Verdict of an IExternalSatSolver query, reusing the embedded solver's SatResult vocabulary. A Satisfiable verdict carries the model; Unsatisfiable and Unknown carry nothing.

public sealed class ExternalSatResult

Inheritance

object

ExternalSatResult

Inherited Members

object.Equals(object)

object.Equals(object, object)

object.GetHashCode()

object.GetType()

object.ReferenceEquals(object, object)

object.ToString()

Properties

Model

Satisfying assignment as DIMACS literals (a solver's "v" lines without the final 0); set exactly when Verdict is Satisfiable. Consumers verify it via IsSatisfiedBy(IReadOnlyList<int>) — SAT claims are checked, UNSAT claims are trusted.

public IReadOnlyList<int>? Model { get; }

Property Value

IReadOnlyList<int>

Verdict

Satisfiable, Unsatisfiable, or Unknown (gave up without a verdict).

public SatResult Verdict { get; }

Property Value

SatResult

Methods

Satisfiable(IReadOnlyList<int>)

A Satisfiable verdict with its model. The model is snapshotted, so a consumer's verify-then-decode sequence always sees the assignment that was verified, even if the adapter keeps mutating its own buffer.

public static ExternalSatResult Satisfiable(IReadOnlyList<int> model)

Parameters

model IReadOnlyList<int>

Returns

ExternalSatResult

Unknown()

No verdict — timeout, budget, or solver unavailable.

public static ExternalSatResult Unknown()

Returns

ExternalSatResult

Unsatisfiable()

An Unsatisfiable verdict (trusted by consumers; see the seam's trust model).

public static ExternalSatResult Unsatisfiable()

Returns

ExternalSatResult