Class CnfBuilder

Namespace

LogicalOptimizer

Assembly

LogicalOptimizer.Sat.dll

Accumulates a CNF (clauses over 1-based DIMACS literals) with auxiliary-variable allocation, for feeding encoders and the SatSolver.

public sealed class CnfBuilder

Inheritance

object

CnfBuilder

Inherited Members

object.Equals(object)

object.Equals(object, object)

object.GetHashCode()

object.GetType()

object.ReferenceEquals(object, object)

object.ToString()

Constructors

CnfBuilder(int)

public CnfBuilder(int variableCount)

Parameters

variableCount int

Properties

Clauses

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

Property Value

IReadOnlyList<int[]>

VariableCount

Total variables including allocated auxiliaries.

public int VariableCount { get; }

Property Value

int

Methods

AddClause(params int[])

public void AddClause(params int[] literals)

Parameters

literals int[]

NewVariable()

public int NewVariable()

Returns

int

ToSolver()

public SatSolver ToSolver()

Returns

SatSolver