Class SatProblem<T>

Namespace

NanoByte.SatSolver

Assembly

NanoByte.SatSolver.dll

A mutable SAT problem builder.

public sealed class SatProblem<T> where T : IEquatable<T>

Type Parameters

T

The user-data type used to identify variables. Each distinct value gets one Boolean variable.

Inheritance

object

SatProblem<T>

Remarks

Allocate variables for the values you care about, add clauses and other constraints, then call Solve(Func<Literal<T>?>?) to obtain a satisfying assignment (or null if unsatisfiable).

Methods

AddClause(params Literal<T>[])

Adds a clause requiring at least one of literals to be true. An empty clause makes the problem unsatisfiable. A single literal becomes an unconditional fact.

public void AddClause(params Literal<T>[] literals)

Parameters

literals Literal<T>[]

AddClause(IEnumerable<Literal<T>>)

Adds a clause requiring at least one of literals to be true. An empty clause makes the problem unsatisfiable. A single literal becomes an unconditional fact.

public void AddClause(IEnumerable<Literal<T>> literals)

Parameters

literals IEnumerable<Literal<T>>

AddFormula(Formula<T>)

Adds all clauses from formula to the problem.

public void AddFormula(Formula<T> formula)

Parameters

formula Formula<T>

AddVariable(T)

Returns the literal for value, allocating a new variable on first use.

public Literal<T> AddVariable(T value)

Parameters

value T

Returns

Literal<T>

AtMostOne(params Literal<T>[])

Adds an at-most-one constraint over the given literals. Returns the constraint object so callers (e.g., deciders) can query it.

public AtMostOneConstraint<T> AtMostOne(params Literal<T>[] literals)

Parameters

literals Literal<T>[]

Returns

AtMostOneConstraint<T>

AtMostOne(IEnumerable<Literal<T>>)

Adds an at-most-one constraint over the given literals. Returns the constraint object so callers (e.g., deciders) can query it.

public AtMostOneConstraint<T> AtMostOne(IEnumerable<Literal<T>> literals)

Parameters

literals IEnumerable<Literal<T>>

Returns

AtMostOneConstraint<T>

GetValue(Literal<T>)

Returns the current truth value of literal in the engine, or null if it has not yet been assigned. Useful from inside a decider callback.

public bool? GetValue(Literal<T> literal)

Parameters

literal Literal<T>

Returns

bool?

Implies(Literal<T>, params Literal<T>[])

Adds the implication antecedent → at-least-one-of(consequents). Equivalent to a clause: !antecedent ∨ c1 ∨ c2 ∨ ....

public void Implies(Literal<T> antecedent, params Literal<T>[] consequents)

Parameters

antecedent Literal<T>

consequents Literal<T>[]

Solve(Func<Literal<T>?>?)

Solves the problem.

public Model<T>? Solve(Func<Literal<T>?>? decider = null)

Parameters

decider Func<Literal<T>?>

Optional callback to choose the next literal to branch on. Returning null means "no preference; set remaining variables to false". The callback receives no arguments; it should inspect external state (e.g., a dependency graph) plus any held AtMostOneConstraint<T> references to decide.

Returns

Model<T>

A model with the satisfying assignment, or null if the problem is unsatisfiable.

Operators

operator +(SatProblem<T>, Clause<T>)

Adds a clause to the problem. Enables problem += literal1 | literal2 syntax.

public static SatProblem<T> operator +(SatProblem<T> problem, Clause<T> clause)

Parameters

problem SatProblem<T>

clause Clause<T>

Returns

SatProblem<T>

operator +(SatProblem<T>, Formula<T>)

Adds all clauses from a formula to the problem. Enables problem += (a | b) & (!a | c) syntax.

public static SatProblem<T> operator +(SatProblem<T> problem, Formula<T> formula)

Parameters

problem SatProblem<T>

formula Formula<T>

Returns

SatProblem<T>