dDNNF.h File Reference

Decomposable Deterministic Negation Normal Form circuit. More...

#include <string>
#include <unordered_set>
#include "BooleanCircuit.h"

Include dependency graph for dDNNF.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	hash_gate_t
	std::hash functor for gate_t. More...
class	dDNNF
	A d-DNNF circuit supporting exact probabilistic and game-theoretic evaluation. More...

Detailed Description

Decomposable Deterministic Negation Normal Form circuit.

A d-DNNF (decomposable deterministic Negation Normal Form) is a Boolean circuit with two structural properties:

• Determinism: for every OR gate, the two sub-formulae are mutually exclusive (their models are disjoint).
• Decomposability: for every AND gate, the two sub-formulae share no variable.

These properties enable:

• Linear-time computation of the probability of satisfying assignments.
• Polynomial computation of Shapley and Banzhaf power indices.

dDNNF extends BooleanCircuit with:

• A designated root gate.
• A memoisation cache for probability evaluation.
• Normalisation methods (makeSmooth(), makeGatesBinary(), simplify()) that transform the circuit into a canonical form required by the evaluation algorithms.
• Conditioning methods (condition(), conditionAndSimplify()) used during Shapley/Banzhaf computation.

@c hash_gate_t

A standard-library compatible hash functor for gate_t, required because gate_t is a scoped enum and has no built-in std::hash specialisation.

Definition in file dDNNF.h.