Class SatSolver

Namespace

LogicalOptimizer

Assembly

LogicalOptimizer.Sat.dll

Self-contained CDCL SAT solver: two-watched literals, 1UIP clause learning, heap-based VSIDS activities, Luby restarts, LBD-driven learnt-clause database reduction, bounded subsumption preprocessing, incremental solving under assumptions with unsat cores, and optional DRAT proof logging. Variables are 1-based DIMACS indices; a positive literal v asserts variable v, a negative literal -v its negation. No dependencies.

public sealed class SatSolver

Inheritance

object

SatSolver

Inherited Members

object.Equals(object)

object.Equals(object, object)

object.GetHashCode()

object.GetType()

object.ReferenceEquals(object, object)

object.ToString()

Constructors

SatSolver(int)

public SatSolver(int variableCount)

Parameters

variableCount int

Properties

ConflictCount

Conflicts spent by the last Solve(int, CancellationToken) call.

public int ConflictCount { get; }

Property Value

int

UnsatCore

After an Unsatisfiable verdict from the assumption overload: the subset of assumption literals jointly inconsistent with the formula. Empty means the formula is unsatisfiable without any assumptions. Null after Satisfiable/Unknown.

public IReadOnlyList<int>? UnsatCore { get; }

Property Value

IReadOnlyList<int>

Methods

AddClause(IReadOnlyCollection<int>)

public void AddClause(IReadOnlyCollection<int> literals)

Parameters

literals IReadOnlyCollection<int>

AddClause(params int[])

public void AddClause(params int[] literals)

Parameters

literals int[]

EnableProofLogging()

Start recording a DRAT proof (learnt and deleted clauses in order, ending with the empty clause on UNSAT). Must be called before the first Solve(int, CancellationToken). Every addition step is RUP-checkable against the original clauses plus preceding steps, so an Unsatisfiable verdict becomes externally verifiable (e.g. with drat-trim).

public void EnableProofLogging()

FromCnf(TseitinCnf)

public static SatSolver FromCnf(TseitinCnf cnf)

Parameters

cnf TseitinCnf

Returns

SatSolver

GetValue(int)

Value of a variable in the satisfying assignment found by the last Solve.

public bool GetValue(int variable)

Parameters

variable int

Returns

bool

Solve(IReadOnlyList<int>, int, CancellationToken)

Incremental solve under assumptions: temporary unit constraints that hold for this call only. Learnt clauses and level-0 facts persist across calls, and clauses may be added between calls. On Unsatisfiable, UnsatCore holds the subset of assumptions responsible (empty = UNSAT regardless of them).

public SatResult Solve(IReadOnlyList<int> assumptions, int maxConflicts = 1000000, CancellationToken cancellationToken = default)

Parameters

assumptions IReadOnlyList<int>

maxConflicts int

cancellationToken CancellationToken

Returns

SatResult

Solve(int, CancellationToken)

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

Parameters

maxConflicts int

cancellationToken CancellationToken

Returns

SatResult

ToDrat()

Proof in textual DRAT format ("d " prefix for deletions, 0-terminated lines).

public string ToDrat()

Returns

string