Class DnnfCircuit

Namespace: LogicalOptimizer

Assembly: LogicalOptimizer.Dnnf.dll

A compiled d-DNNF (deterministic, decomposable Negation Normal Form) circuit for a boolean formula. Compilation happens once (see KnowledgeCompilation); afterwards exact model counting, weighted model counting and model enumeration are all linear in the circuit size.

The circuit is compiled over the full equisatisfiable Tseitin CNF of the input formula (input variables plus functionally-determined gate auxiliaries). Because the full biconditional Tseitin encoding is equi-count over the input variables — every satisfying input assignment extends to exactly one auxiliary assignment — the model count of the whole circuit equals the model count of the original formula over its input variables, with no projection needed. Variables and EnumerateModels(CancellationToken) expose only the original input variables; the auxiliaries are projected away.

public sealed class DnnfCircuit

Inheritance: object

DnnfCircuit

Inherited Members: object.Equals(object)

object.Equals(object, object)

object.GetHashCode()

object.GetType()

object.ReferenceEquals(object, object)

object.ToString()

Properties

IsSatisfiable

Whether the formula has at least one model.

public bool IsSatisfiable { get; }

Property Value

bool

NodeCount

Number of nodes in the compiled d-DNNF DAG.

public int NodeCount { get; }

Property Value

int

Variables

The original input variables of the compiled formula (sorted by name).

public IReadOnlyList<string> Variables { get; }

Property Value

IReadOnlyList<string>

Methods

Condition(IReadOnlyDictionary<string, bool>, CancellationToken)

Condition (cofactor) the circuit on a partial assignment, returning a NEW circuit in which every named variable is pinned to the given value; this is never mutated.

Semantics: the conditioned circuit keeps the SAME variable universe — Variables is unchanged and every conditioned variable stays in the model-count universe, now pinned to exactly one value. Consequently Condition(a).CountModels() equals the number of this's models that are consistent with assignment (a pinned variable contributes a factor of one, not two). Repeatedly conditioning composes: Condition(a).Condition(b) equals Condition(a ∪ b) when a and b agree.

Every key of assignment must be one of the circuit's Variables; an unknown name is an ArgumentException. An empty assignment returns an equivalent circuit (same model count). The rewrite is a single memoized pass over the shared DAG and allocates at most O(NodeCount) additional nodes, so it never exceeds the original compilation's node budget.

public DnnfCircuit Condition(IReadOnlyDictionary<string, bool> assignment, CancellationToken cancellationToken = default)

Parameters

assignment IReadOnlyDictionary<string, bool>: Variables to pin, each mapped to the value it is fixed to.
cancellationToken CancellationToken: Cancels the rewrite on a large circuit.

Returns

DnnfCircuit

Exceptions

ArgumentException: A key is not one of the circuit's variables.
OperationCanceledException: The token was cancelled.

CountModels()

Exact number of satisfying assignments (#SAT) of the original formula over its input variables. A single bottom-up pass over the DAG: literal -> 1, decomposable AND -> product of children, deterministic OR (decision on v) -> sum of the two branches. Because every variable in a node's scope is represented explicitly (the circuit is smooth), no gap/smoothing correction is needed.

public BigInteger CountModels()

Returns

BigInteger

CountModels(IReadOnlyDictionary<string, bool>)

Exact number of models consistent with evidence: the count over the circuit's input variables (see CountModels()) restricted to assignments that agree with the given partial assignment. Equivalent to Condition(evidence).CountModels() but computed in a single bottom-up pass without building a new circuit. Empty evidence reproduces CountModels() exactly; a full assignment yields 0 or 1.

Every key of evidence must be one of the circuit's Variables; an unknown name is an ArgumentException.

public BigInteger CountModels(IReadOnlyDictionary<string, bool> evidence)

Parameters

evidence IReadOnlyDictionary<string, bool>

Returns

BigInteger

Exceptions

ArgumentException: A key is not one of the circuit's variables.

EnumerateModels(CancellationToken)

Lazily enumerate every model, projected onto the original input variables. Free variables (unconstrained in a subtree) expand to both polarities. The count can be exponential — combine with Take/TakeWhile or call CountModels() first.

public IEnumerable<IReadOnlyDictionary<string, bool>> EnumerateModels(CancellationToken cancellationToken = default)

Parameters

cancellationToken CancellationToken

Returns

IEnumerable<IReadOnlyDictionary<string, bool>>

Load(Stream, ResourceBudget?, CancellationToken)

Experimental (until v4). Read a d-DNNF circuit back from a blob produced by Save(Stream). The load is fully validated — magic, format version (a newer version is refused, not misread), engine byte (a BDD blob is a typed error here), CRC-32 checksum, and the node table's structure (indices in range, children strictly before their parent so the graph is acyclic, a valid root and terminals). The checksum only catches corruption; it does not replace the structural checks.

The read is budgeted and never trusts a length field to pre-size an allocation: a header claiming a huge node count is checked against budget and against the actual stream, so a hostile blob aborts with NodeBudgetExceededException or a truncation error rather than allocating unboundedly. Any malformed input is a CircuitSerializationException.

public static DnnfCircuit Load(Stream source, ResourceBudget? budget = null, CancellationToken cancellationToken = default)

Parameters

source Stream: The stream to read the blob from.
budget ResourceBudget: Load budget; the node table is bounded by BddNodeLimit. Defaults to Default.
cancellationToken CancellationToken: Cancels a long load.

Returns

DnnfCircuit

Exceptions

ArgumentNullException: source is null.
CircuitSerializationException: The blob is malformed, corrupt, a newer version, or the wrong engine.
NodeBudgetExceededException: The blob's declared size exceeds the load budget.
OperationCanceledException: The token was cancelled.

MarginalProbability(string, IReadOnlyDictionary<string, (double positive, double negative)>)

The weighted marginal probability that variable is true: the weighted model count restricted to models in which the variable is true, divided by the unrestricted weighted model count — WeightedModelCount(weights, {variable = true}) / WeightedModelCount(weights), both computed with the evidence overload. The result lies in [0, 1].

With uniform weights — every entry (1, 1), or a variable simply omitted from weights (which defaults to (1, 1)) — this is exactly the fraction of the formula's models in which variable is true.

Floating-point: computed in double as the ratio of two weighted counts (see WeightedModelCount(IReadOnlyDictionary<string, (double positive, double negative)>)), so it inherits that overload's IEEE-754 accumulation behaviour — exact when the weights and intermediate sums are representable, otherwise carrying the usual rounding.

public double MarginalProbability(string variable, IReadOnlyDictionary<string, (double positive, double negative)> weights)

Parameters

variable string: One of the circuit's Variables.
weights IReadOnlyDictionary<string, (double positive, double negative)>: Per-variable (positive, negative) literal weights; a variable absent from the map defaults to (1, 1). Every weight must be finite and non-negative.

Returns

double

Exceptions

ArgumentException: variable is not one of the circuit's variables, or a weight is negative, NaN or infinite.
InvalidOperationException: The total weighted model count is zero (an unsatisfiable formula or all-zero weights), so the marginal is undefined — never a fabricated value.

SampleModel(Random, IReadOnlyDictionary<string, (double positive, double negative)>?)

Draw one model at random, projected onto the circuit's Variables — every variable is assigned exactly one value. Standard top-down d-DNNF sampling and the mirror of the bottom-up weighted pass: at a deterministic decision a branch is taken with probability proportional to its (weighted) share of the model count, at a decomposable conjunction every child is sampled independently, and a literal fixes its variable. With weights null the draw is uniform over the formula's satisfying assignments; otherwise each model is drawn with probability proportional to the product of its per-literal weights (its weighted-model-count share).

Randomness comes solely from random: the distribution is only as good as that source, and the method makes NO cryptographic guarantee. Branch probabilities are evaluated in double and inherit the weighted pass's IEEE-754 behaviour.

public IReadOnlyDictionary<string, bool> SampleModel(Random random, IReadOnlyDictionary<string, (double positive, double negative)>? weights = null)

Parameters

random Random: The random source consumed by the draw.
weights IReadOnlyDictionary<string, (double positive, double negative)>: Optional per-variable (positive, negative) literal weights; a variable absent from the map defaults to (1, 1) and every weight must be finite and non-negative. null samples uniformly.

Returns

IReadOnlyDictionary<string, bool>

Exceptions

ArgumentException: A weight is negative, NaN or infinite.
InvalidOperationException: The circuit has zero total weight (an unsatisfiable formula or all-zero weights): there is no model to draw, and none is fabricated.

SampleModels(int, int, IReadOnlyDictionary<string, (double positive, double negative)>?, CancellationToken)

Draw count models deterministically from seed: the same seed produces the exact same sequence on every run and platform (a fresh Random seeded with seed drives the draws). Each model is produced exactly as by SampleModel(Random, IReadOnlyDictionary<string, (double positive, double negative)>?) — uniform when weights is null, weighted otherwise, and every model assigns the full set of Variables. The sequence is lazy; combine with LINQ (Take/Where/…) as needed.

No cryptographic guarantee is made about the distribution.

public IEnumerable<IReadOnlyDictionary<string, bool>> SampleModels(int count, int seed, IReadOnlyDictionary<string, (double positive, double negative)>? weights = null, CancellationToken cancellationToken = default)

Parameters

count int: Number of models to draw (non-negative).
seed int: Seed for the deterministic pseudo-random sequence.
weights IReadOnlyDictionary<string, (double positive, double negative)>: Optional per-variable (positive, negative) literal weights (see SampleModel(Random, IReadOnlyDictionary<string, (double positive, double negative)>?)); null samples uniformly.
cancellationToken CancellationToken: Cancels the (potentially long) enumeration between draws.

Returns

IEnumerable<IReadOnlyDictionary<string, bool>>

Exceptions

ArgumentOutOfRangeException: count is negative.
ArgumentException: A weight is negative, NaN or infinite.
InvalidOperationException: The circuit has zero total weight (unsatisfiable or all-zero weights); no model is fabricated.

Save(Stream)

Experimental (until v4). Serialize this d-DNNF circuit to a compact, self-describing binary blob (little-endian, CRC-32 checked). The output is deterministic — the same circuit always produces identical bytes — and can be read back with Load(Stream, ResourceBudget?, CancellationToken); a round-trip preserves the variables, model count, weighted counts and evaluation exactly.

The format is EXPERIMENTAL: it may change before v4 and carries no cross-version compatibility guarantee other than the version gate, which makes a future build refuse (rather than misread) a blob it does not understand. The engine byte makes a d-DNNF blob a typed error if it is loaded as a BDD. No reflection or object deserialization is used.

public void Save(Stream destination)

Parameters

destination Stream: The stream the blob is written to.

Exceptions

ArgumentNullException: destination is null.

WeightedModelCount(IReadOnlyDictionary<string, (double positive, double negative)>)

Weighted model count: the sum over all models of the product of per-literal weights. weights maps each input variable name to its (positive, negative) literal weights; a variable absent from the map defaults to (1, 1). With every weight equal to (1, 1) this reproduces CountModels() as a floating-point value. Functionally-determined Tseitin auxiliaries always carry weight (1, 1), so they do not affect the result.

public double WeightedModelCount(IReadOnlyDictionary<string, (double positive, double negative)> weights)

Parameters

weights IReadOnlyDictionary<string, (double positive, double negative)>

Returns

double

WeightedModelCount(IReadOnlyDictionary<string, (double positive, double negative)>, IReadOnlyDictionary<string, bool>)

Weighted model count restricted to the models consistent with evidence: the sum over those models of the product of per-literal weights (see WeightedModelCount(IReadOnlyDictionary<string, (double positive, double negative)>)). Equivalent to weighting Condition(evidence); empty evidence reproduces the plain weighted count. The floating-point contract of the unconditioned overload carries over: the result is exact when the weights and intermediate sums are representable, and accumulates the usual IEEE-754 rounding otherwise (validated to a documented tolerance).

Every key of evidence must be one of the circuit's Variables; an unknown name is an ArgumentException. Unknown weights keys are ignored, exactly as in the unconditioned overload.

public double WeightedModelCount(IReadOnlyDictionary<string, (double positive, double negative)> weights, IReadOnlyDictionary<string, bool> evidence)

Parameters

weights IReadOnlyDictionary<string, (double positive, double negative)>
evidence IReadOnlyDictionary<string, bool>

Returns

double

Exceptions

ArgumentException: An evidence key is not one of the circuit's variables.