Class ExternalSatProblem

Namespace

LogicalOptimizer

Assembly

LogicalOptimizer.Sat.dll

A one-shot CNF satisfiability query for an IExternalSatSolver. Literals follow the DIMACS convention: variables are 1-based, a positive literal v asserts variable v, a negative literal -v its negation. Optional assumptions are unit constraints for this query; adapters that speak plain DIMACS may append them as unit clauses (equivalent for a single call), which is exactly what ToDimacs() does.

public sealed class ExternalSatProblem

Inheritance

object

ExternalSatProblem

Inherited Members

object.Equals(object)

object.Equals(object, object)

object.GetHashCode()

object.GetType()

object.ReferenceEquals(object, object)

object.ToString()

Constructors

ExternalSatProblem(int, IReadOnlyList<int[]>, IReadOnlyList<int>?)

Create a problem over variables 1..variableCount. Every literal in clauses and assumptions must be non-zero and within range. The constructor snapshots both collections (including every clause array); later mutation of the caller's collections cannot change the validated problem.

public ExternalSatProblem(int variableCount, IReadOnlyList<int[]> clauses, IReadOnlyList<int>? assumptions = null)

Parameters

variableCount int

clauses IReadOnlyList<int[]>

assumptions IReadOnlyList<int>

Properties

Assumptions

Assumption literals for this query; empty when none.

public IReadOnlyList<int> Assumptions { get; }

Property Value

IReadOnlyList<int>

Clauses

Clauses as arrays of DIMACS literals (no terminating 0). Reading a clause returns an independent copy — the validated snapshot cannot be mutated through this property.

public IReadOnlyList<int[]> Clauses { get; }

Property Value

IReadOnlyList<int[]>

VariableCount

Number of variables; valid DIMACS indices are 1..VariableCount.

public int VariableCount { get; }

Property Value

int

Methods

FromCnf(TseitinCnf, IReadOnlyList<int>?)

Build a problem from an equisatisfiable TseitinCnf.

public static ExternalSatProblem FromCnf(TseitinCnf cnf, IReadOnlyList<int>? assumptions = null)

Parameters

cnf TseitinCnf

assumptions IReadOnlyList<int>

Returns

ExternalSatProblem

IsSatisfiedBy(IReadOnlyList<int>)

Verify a claimed model against this problem — the cheap half of the seam's trust contract, linear in the total literal count. The model is a set of DIMACS literals (as printed on a solver's "v" lines, without the final 0); it may be partial, but every clause and every assumption must contain a literal the model asserts. Contradictory or out-of-range literals fail.

public bool IsSatisfiedBy(IReadOnlyList<int> model)

Parameters

model IReadOnlyList<int>

Returns

bool

ToDimacs()

The problem in DIMACS CNF format, ready to hand to any standard solver. Assumptions are appended as unit clauses (plain DIMACS has no assumption syntax; for a one-shot query the two are equivalent).

public string ToDimacs()

Returns

string