Knowledge Compilation & Model Counting

The LogicalOptimizer.Dnnf package compiles a boolean formula into a d-DNNF (deterministic, decomposable Negation Normal Form) circuit. Compilation happens once; afterwards every query — exact model counting, weighted model counting and model enumeration — runs in time linear in the compiled circuit size.

API

using LogicalOptimizer;

AstNode formula = new FormulaFactory().Parse("(a | b) & (b | c)");

DnnfCircuit circuit = KnowledgeCompilation.CompileToDnnf(formula);

bool sat            = circuit.IsSatisfiable;     // has at least one model
System.Numerics.BigInteger count = circuit.CountModels();  // exact #SAT

// Weighted model count: per-variable (positive, negative) literal weights.
double weighted = circuit.WeightedModelCount(new Dictionary<string, (double, double)>
{
    ["a"] = (0.7, 0.3),
    ["b"] = (0.5, 0.5),
    ["c"] = (0.9, 0.1),
});

// Lazy enumeration over the original input variables.
foreach (IReadOnlyDictionary<string, bool> model in circuit.EnumerateModels())
{
    // ...
}

Conditioning and evidence queries

Once compiled, a circuit can be queried under a partial assignment (evidence) without recompiling the formula:

var evidence = new Dictionary<string, bool> { ["a"] = true };

// #models consistent with the evidence — a single bottom-up pass, no new circuit.
System.Numerics.BigInteger given = circuit.CountModels(evidence);
double weightedGiven          = circuit.WeightedModelCount(weights, evidence);

// Or materialize a NEW circuit with the variables pinned; the original is untouched.
DnnfCircuit conditioned = circuit.Condition(evidence);
// conditioned.CountModels() == circuit.CountModels(evidence)

Condition keeps the same variable universe — Variables is unchanged and each pinned variable stays in the model-count universe fixed to one value — so Condition(evidence).CountModels() is exactly the number of the original circuit's models consistent with evidence. Empty evidence reproduces the unconditioned query; a full assignment yields 0 or 1. Every evidence/assignment key must be one of the circuit's Variables, otherwise an ArgumentException is thrown.

Marginals and model sampling

The weighted count also powers probabilistic and configuration queries:

// Weighted marginal probability that a is true:
//   WeightedModelCount(weights, {a = true}) / WeightedModelCount(weights).
// With uniform weights this is just the fraction of models in which a is true.
double pA = circuit.MarginalProbability("a", weights);

// Draw models by standard top-down weighted d-DNNF sampling. weights == null => uniform over
// the satisfying models; otherwise proportional to each model's weighted-count share. Every
// sampled model assigns exactly the circuit's Variables.
IReadOnlyDictionary<string, bool> one = circuit.SampleModel(new Random(), weights);

// Deterministic for a given seed — the same seed yields the same sequence on every run.
foreach (IReadOnlyDictionary<string, bool> model in circuit.SampleModels(1000, seed: 42))
{
    // ...
}

A zero total weight — an unsatisfiable formula or all-zero weights — has no model to draw, so MarginalProbability/SampleModel/SampleModels throw an InvalidOperationException rather than fabricate one; an unknown marginal variable, or a negative, NaN or infinite weight, is an ArgumentException. Sampling is pseudo-random with no cryptographic guarantee; branch probabilities are evaluated in double and share the weighted count's floating-point behaviour.

CompileToDnnf(AstNode formula, int nodeBudget = 1_000_000, CancellationToken ct = default) caps the DAG size with nodeBudget (a NodeBudgetExceededException — a public InvalidOperationException subtype — is thrown when it is exceeded) and honors the cancellation token. Both are heuristic safety limits: knowledge compilation can blow up on hard CNF, so treat them as guardrails, not guarantees of tractability.

How it works

The compiler is a top-down decision-DNNF compiler in the style of c2d / D4:

  1. The formula is turned into its full (biconditional) Tseitin CNF. That encoding is equisatisfiable and equi-count over the input variables — every satisfying input assignment extends to exactly one assignment of the gate auxiliaries — so the model count of the whole CNF already equals the model count of the original formula over its inputs. No projection is needed for counting; enumeration simply drops the functionally-determined auxiliary variables.
  2. The residual clause set is compiled recursively:
    • Unit propagation to a fixpoint yields a conjunction of implied literal nodes.
    • Connected-component decomposition partitions the remaining clauses by shared variables into a decomposable AND (each component is compiled independently).
    • A decision on a variable branches into v / ¬v, forming a deterministic OR (the two branches are mutually exclusive on the decision variable).
    • Component caching, keyed by the normalized active clause set, turns the search into a shared DAG rather than an exponential tree.
  3. The circuit is kept smooth: every variable in a node's scope is represented explicitly, so counting is a single bottom-up pass — literal → 1, decomposable AND → product of children, deterministic OR → sum of branches — with no gap/smoothing correction. Counts use BigInteger; weighted counts apply per-literal weights with the same recurrence.

Variables and EnumerateModels expose only the original input variables; the Tseitin auxiliaries are projected away.

Correctness

Exact model counting is only useful if it is exact. The d-DNNF count is checked against the independent ROBDD oracle: for a large corpus of random and structured formulas, CompileToDnnf(f).CountModels() must equal BinaryDecisionDiagram.BuildWithBestOrder(f).CountSatisfyingAssignments() exactly, and also matches full truth-table brute force on small formulas. Enumeration is cross-checked against FormulaAnalysis.EnumerateModels.

Serialization (experimental)

A compiled circuit can be persisted and reloaded so counting/enumeration need not recompile:

using var file = File.Create("circuit.locx");
circuit.Save(file);
// ...later / another process:
var reloaded = DnnfCircuit.Load(File.OpenRead("circuit.locx"));
reloaded.CountModels();  // identical to the original

The format is experimental until v4 (no cross-version guarantee beyond the version gate, which refuses — never misreads — a blob from a newer build). It is deterministic, little-endian and CRC-32 checked; Load is structurally validated (indices in range, acyclic/topological, valid root and terminals) and budgeted — a hostile size header aborts with NodeBudgetExceededException rather than pre-allocating, and malformed input is a CircuitSerializationException. There is no reflection or object deserialization, and the engine byte makes loading a BDD blob as a d-DNNF circuit a typed error. A round-trip preserves the variables, model count, weighted counts and evaluation exactly.

Edit this page