Class KnowledgeCompilation

Namespace: LogicalOptimizer

Assembly: LogicalOptimizer.Dnnf.dll

Knowledge compilation entry point: turn a boolean formula into a d-DNNF circuit that answers model-counting and enumeration queries in time linear in the circuit size.

public static class KnowledgeCompilation

Inheritance: object

KnowledgeCompilation

Inherited Members: object.Equals(object)

object.Equals(object, object)

object.GetHashCode()

object.GetType()

object.MemberwiseClone()

object.ReferenceEquals(object, object)

object.ToString()

Fields

DefaultNodeBudget

Default node budget for CompileToDnnf(AstNode, int, CancellationToken).

public const int DefaultNodeBudget = 1000000

Field Value

int

Methods

CompileToDnnf(AstNode, int, CancellationToken)

Compile formula into a DnnfCircuit using a top-down decision-DNNF compiler with component caching. Compilation can blow up on hard CNF, so nodeBudget caps the DAG size (an InvalidOperationException is thrown when it is exceeded) and cancellationToken interrupts a long compile. Both are heuristic safety limits, not guarantees of tractability.

public static DnnfCircuit CompileToDnnf(AstNode formula, int nodeBudget = 1000000, CancellationToken cancellationToken = default)

Parameters

formula AstNode: The formula to compile.
nodeBudget int: Maximum number of DAG nodes before compilation aborts.
cancellationToken CancellationToken: Cancels a long-running compilation.

Returns

DnnfCircuit

Exceptions

InvalidOperationException: The node budget was exceeded.
OperationCanceledException: The token was cancelled.