Class CnfProblem

Namespace

LogicalOptimizer

Assembly

LogicalOptimizer.Formats.dll

A CNF satisfiability problem parsed from DIMACS: a fixed variable count and a list of clauses over 1-based signed literals (a positive literal v asserts variable v, a negative literal -v its negation). Hands off directly to the in-house SatSolver; also convertible to an AstNode for the BDD / d-DNNF engines.

public sealed class CnfProblem

Inheritance

object

CnfProblem

Inherited Members

object.Equals(object)

object.Equals(object, object)

object.GetHashCode()

object.GetType()

object.ReferenceEquals(object, object)

object.ToString()

Properties

Clauses

Clauses as arrays of non-zero signed literals; an empty array is the empty clause.

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

Property Value

IReadOnlyList<int[]>

VariableCount

Declared number of variables (indices 1..VariableCount).

public int VariableCount { get; }

Property Value

int

Methods

Solve(int, CancellationToken)

Solve this instance with the in-house CDCL solver.

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

Parameters

maxConflicts int

cancellationToken CancellationToken

Returns

SatResult

ToFormula()

Convert to a canonicalized boolean formula over variables named x1..xN (conjunction of clause disjunctions), suitable for the BDD or d-DNNF engines. An empty clause becomes the constant false; an instance with no clauses is the constant true. Variables that never appear in a clause are absent from the tree.

public AstNode ToFormula()

Returns

AstNode

ToSolver()

Build a SatSolver loaded with every clause of this problem.

public SatSolver ToSolver()

Returns

SatSolver

Write(TextWriter)

Write this problem back out as DIMACS CNF text (round-trips through the parser).

public void Write(TextWriter writer)

Parameters

writer TextWriter