Class TseitinCnf

Namespace: LogicalOptimizer

Assembly: LogicalOptimizer.Sat.dll

Equisatisfiable CNF produced by LogicalOptimizer.TseitinConverter. Variable indices are 1-based DIMACS style: input variables first (sorted by name), auxiliary gate variables after.

public sealed class TseitinCnf

Inheritance: object

TseitinCnf

Inherited Members: object.Equals(object)

object.Equals(object, object)

object.GetHashCode()

object.GetType()

object.ReferenceEquals(object, object)

Properties

AuxiliaryVariableCount

public int AuxiliaryVariableCount { get; }

Property Value

int

Clauses

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

Property Value

IReadOnlyList<int[]>

InputVariables

public IReadOnlyList<string> InputVariables { get; }

Property Value

IReadOnlyList<string>

TotalVariableCount

public int TotalVariableCount { get; }

Property Value

int

Methods

ToAst()

CNF as an AST over input and auxiliary (_tN) variables.

public AstNode ToAst()

Returns

AstNode

ToDimacs()

public string ToDimacs()

Returns

string

ToString()

Returns a string that represents the current object.

public override string ToString()

Returns

string: A string that represents the current object.

VariableName(int)

Name of a 1-based DIMACS variable index: input name or _tN for auxiliaries.

public string VariableName(int index)

Parameters

index int

Returns

string