A d-DNNF circuit supporting exact probabilistic and game-theoretic evaluation. More...

#include "dDNNF.h"

Inheritance diagram for dDNNF:

[legend]

Collaboration diagram for dDNNF:

[legend]

Classes
struct	Stats
	Structural statistics of a compiled d-DNNF. More...

Public Member Functions
gate_t	getRoot () const
	Return the root gate of this d-DNNF.
void	setRoot (gate_t g)
	Set the root gate.
std::unordered_set< gate_t >	vars (gate_t root) const
	Return the set of all variable (IN) gates reachable from `root`.
void	makeSmooth ()
	Make the d-DNNF smooth.
void	makeGatesBinary (BooleanGate type)
	Rewrite all n-ary AND/OR gates into binary trees.
void	simplify ()
	Simplify the d-DNNF by removing redundant constants.
dDNNF	conditionAndSimplify (gate_t var, bool value) const
	Condition on variable `var` having value `value` and simplify.
dDNNF	condition (gate_t var, bool value) const
	Condition on variable `var` having value `value` (no simplification).
double	probabilityEvaluation () const
	Compute the exact probability of the d-DNNF being `true`.
double	shapley (gate_t var) const
	Compute the Shapley value of input gate `var`.
double	banzhaf (gate_t var) const
	Compute the Banzhaf power index of input gate `var`.
Stats	nodeStats () const
	Compute structural statistics over the gates reachable from `root`.
std::string	toDot () const
	Return a GraphViz DOT representation of the d-DNNF.
std::string	toNNF (const std::function< int(const std::string &)> &var_of_uuid={}) const
	Serialise the d-DNNF in the c2d / d4 `".nnf"` text format.
Public Member Functions inherited from BooleanCircuit
bool	isDNNFCertified (gate_t g) const
	Is gate `g` certified by the d-DNNF per-gate marking?
	BooleanCircuit ()
	Construct an empty Boolean circuit.
virtual	~BooleanCircuit ()
gate_t	addGate () override
	Allocate a new gate with a default-initialised type.
gate_t	setGate (BooleanGate type) override
	Allocate a new gate with type `type` and no UUID.
gate_t	setGate (const uuid &u, BooleanGate type) override
	Create or update the gate associated with UUID `u`.
gate_t	setGate (BooleanGate t, double p)
	Create a new gate with a probability annotation.
gate_t	setGate (const uuid &u, BooleanGate t, double p)
	Create (or update) a gate with a UUID and probability.
const std::set< gate_t > &	getInputs () const
	Return the set of input (IN) gate IDs.
bool	hasMultivaluedGates () const
	Return `true` if the circuit contains any MULIN gates.
void	setProb (gate_t g, double p)
	Set the probability for gate `g` and mark the circuit as probabilistic.
double	getProb (gate_t g) const
	Return the probability stored for gate `g`.
bool	isProbabilistic () const
	Return `true` if any gate has a non-trivial (< 1) probability.
void	setInfo (gate_t g, unsigned info)
	Store an integer annotation on gate `g`.
unsigned	getInfo (gate_t g) const
	Return the integer annotation for gate `g`.
double	possibleWorlds (gate_t g) const
	Compute the probability by exact enumeration of all possible worlds.
dDNNF	compilation (gate_t g, std::string compiler, std::string *resolved=nullptr) const
	Compile the sub-circuit rooted at `g` to a `dDNNF` via an external tool.
dDNNF	parseDDNNF (std::istream &in, const std::vector< gate_t > &inputOrder) const
	Parse a c2d/d4 NNF stream into a `dDNNF` over this circuit's input gates.
double	monteCarlo (gate_t g, unsigned samples) const
	Estimate the probability via Monte Carlo sampling.
bool	dnfShape (gate_t g, std::vector< gate_t > &clauses, std::vector< std::set< gate_t > > &supports) const
	Detect the DNF shape the Karp-Luby FPRAS requires.
bool	dnfShapeInfo (gate_t g, std::size_t &num_clauses) const
	Cheap shape test: is the circuit DNF-shaped, and how many clauses?
double	karpLuby (const std::vector< gate_t > &clauses, const std::vector< std::set< gate_t > > &supports, unsigned long samples) const
	Karp-Luby FPRAS estimate of a DNF-shaped circuit's probability (fixed sample budget, stratified).
double	sieve (const std::vector< gate_t > &clauses, const std::vector< std::set< gate_t > > &supports) const
	Exact probability of a monotone DNF by inclusion-exclusion (sieve).
void	dnfBounds (const std::vector< std::set< gate_t > > &clauses, double &lower, double &upper) const
	Cheap certified probability interval [lower,upper] of a monotone DNF, without compiling it (Olteanu-Huang-Koch d-tree leaf bound).
double	karpLubyStopping (const std::vector< gate_t > &clauses, const std::vector< std::set< gate_t > > &supports, double eps, double delta, unsigned long max_samples, unsigned long &samples_used, bool &reached_target) const
	Karp-Luby FPRAS with the self-adjusting stopping rule (adaptive sample count for a relative (eps,delta) guarantee).
double	wmcCount (gate_t g, const std::string &tool, const std::string &opt) const
	Weighted model counting through a registered external counter.
double	independentEvaluation (gate_t g) const
	Compute the probability exactly when inputs are independent.
void	rewriteMultivaluedGates ()
	Rewrite all MULVAR/MULIN gate clusters into standard AND/OR/NOT circuits.
dDNNF	interpretAsDD (gate_t g) const
	Build a `dDNNF` directly from the Boolean circuit's structure.
dDNNF	makeDD (gate_t g, const std::string &method, const std::string &args) const
	Dispatch to the appropriate d-DNNF construction method.
dDNNF	makeDDByName (gate_t g, const std::string &name) const
	Build a `dDNNF` from a single compiler/route name.
virtual std::string	toString (gate_t g) const override
	Return a textual description of gate `g` for debugging.
std::string	toString (gate_t g, const std::unordered_map< gate_t, std::string > &labels) const
	Render the sub-circuit at `g`, labelling input gates from a map.
std::string	exportCircuit (gate_t g) const
	Export the circuit in the textual format expected by external compilers.
std::string	TseytinCNF (gate_t g, bool display_prob, bool mapping=false) const
	Return the Tseytin transformation of the sub-circuit at `g` as a DIMACS string.
std::vector< CNFInputMapping >	tseytinVariableMapping () const
	Map each input gate to its DIMACS variable, UUID, probability.
std::string	BCS12 (gate_t g, std::vector< gate_t > &inputOrder) const
	Serialise the sub-circuit at `g` in d4's BC-S1.2 circuit format.
dDNNF	parsePaniniDD (const std::string &outfilename) const
	Parse a Panini (KCBox) DD output file into a ProvSQL d-DNNF.
template<class Archive>
void	serialize (Archive &ar, const unsigned int version)
	Boost serialisation support.
Public Member Functions inherited from Circuit< BooleanGate >
virtual	~Circuit ()
std::vector< gate_t >::size_type	getNbGates () const
	Return the total number of gates in the circuit.
gate_t	getGate (const uuid &u)
	Return (or create) the gate associated with UUID `u`.
uuid	getUUID (gate_t g) const
	Return the UUID string associated with gate `g`.
BooleanGate	getGateType (gate_t g) const
	Return the type of gate `g`.
std::vector< gate_t > &	getWires (gate_t g)
	Return a mutable reference to the child-wire list of gate `g`.
virtual gate_t	setGate (const uuid &u, BooleanGate type)
	Create or update the gate associated with UUID `u`.
bool	hasGate (const uuid &u) const
	Test whether a gate with UUID `u` exists.
void	addWire (gate_t f, gate_t t)
	Add a directed wire from gate `f` (parent) to gate `t` (child).

Public Attributes
friend	dDNNFTreeDecompositionBuilder
	Allowed to construct and populate this d-DNNF.
friend	StructuredDNNFBuilder
	Inversion-free structured builder: constructs and populates this d-DNNF.

Private Member Functions
std::unordered_map< gate_t, std::vector< double > >	shapley_delta () const
	Compute the δ table used in the Shapley algorithm.
std::vector< std::vector< double > >	shapley_alpha () const
	Compute the α table used in the Shapley algorithm.
double	banzhaf_internal () const
	Compute the unnormalised Banzhaf value for the whole circuit.
std::vector< gate_t >	topological_order (const std::vector< std::vector< gate_t > > &reversedWires) const
	Compute a topological ordering of the circuit.

Private Attributes
std::unordered_map< gate_t, double, hash_gate_t >	probability_cache
	Memoisation cache mapping gates to their probability values.
gate_t	root {0}
	The root gate of the d-DNNF.

Friends
dDNNF	BooleanCircuit::compilation (gate_t g, std::string compiler, std::string *resolved) const
	Allowed to access internal d-DNNF state.

Additional Inherited Members
Public Types inherited from Circuit< BooleanGate >
using	uuid
	UUID type used in this circuit (always `std::string`).
Protected Member Functions inherited from Circuit< BooleanGate >
void	setGateType (gate_t g, BooleanGate t)
	Update the type of an existing gate.
Protected Attributes inherited from BooleanCircuit
std::set< gate_t >	inputs
	Set of IN (input) gate IDs.
std::set< gate_t >	mulinputs
	Set of MULVAR gate IDs.
std::vector< double >	prob
	Per-gate probability (for IN gates).
std::map< gate_t, unsigned >	info
	Per-gate integer info (for MULIN gates).
bool	probabilistic =false
	`true` if any gate has a non-unit probability
Protected Attributes inherited from Circuit< BooleanGate >
std::unordered_map< uuid, gate_t >	uuid2id
	UUID string → gate index.
std::unordered_map< gate_t, uuid >	id2uuid
	Gate index → UUID string.
std::vector< BooleanGate >	gates
	Gate type for each gate.
std::vector< std::vector< gate_t > >	wires
	Child wire lists for each gate.

Detailed Description

A d-DNNF circuit supporting exact probabilistic and game-theoretic evaluation.

Inherits the full BooleanCircuit structure and adds a root gate and algorithms that exploit the d-DNNF structural properties for efficient computation.

Definition at line 71 of file dDNNF.h.

Member Function Documentation

◆ banzhaf()

double dDNNF::banzhaf ( gate_t var ) const

Compute the Banzhaf power index of input gate var.

Uses repeated conditioning and probability evaluation.

Parameters

var	Input gate whose Banzhaf index is requested.

Returns: Banzhaf power index.

Definition at line 554 of file dDNNF.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ banzhaf_internal()

double dDNNF::banzhaf_internal ( ) const

private

Compute the unnormalised Banzhaf value for the whole circuit.

Used internally by banzhaf() to compute the Banzhaf power index for a specific variable after conditioning.

Returns: Unnormalised Banzhaf value.

Definition at line 228 of file dDNNF.cpp.

Here is the call graph for this function:

◆ condition()

dDNNF dDNNF::condition	(	gate_t	var,
		bool	value ) const

Condition on variable var having value value (no simplification).

Parameters

var	Input gate to condition on.
value	Truth value to assign to `var`.

Returns: A copy of the circuit with var fixed to value.

Definition at line 564 of file dDNNF.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ conditionAndSimplify()

dDNNF dDNNF::conditionAndSimplify	(	gate_t	var,
		bool	value ) const

Condition on variable var having value value and simplify.

Sets input gate var to value and propagates the simplification through the circuit, returning a new (simplified) dDNNF.

Parameters

var	Input gate to condition on.
value	Truth value to assign to `var`.

Returns: A simplified copy of the conditioned circuit.

◆ getRoot()

gate_t dDNNF::getRoot ( ) const

inline

Return the root gate of this d-DNNF.

Returns: Gate identifier of the root.

Definition at line 120 of file dDNNF.h.

Here is the caller graph for this function:

◆ makeGatesBinary()

void dDNNF::makeGatesBinary ( BooleanGate type )

Rewrite all n-ary AND/OR gates into binary trees.

Some evaluation algorithms assume binary gates. This method replaces every AND (or OR, depending on type) gate with more than two children by a balanced binary tree of the same type.

Parameters

type	The gate type (`BooleanGate::AND` or `BooleanGate::OR`) to binarise.

Definition at line 108 of file dDNNF.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ makeSmooth()

void dDNNF::makeSmooth ( )

Make the d-DNNF smooth.

A d-DNNF is smooth if every OR gate's children mention exactly the same set of variables. Smoothing is required before probability evaluation to ensure correctness.

Definition at line 61 of file dDNNF.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ nodeStats()

dDNNF::Stats dDNNF::nodeStats ( ) const

Compute structural statistics over the gates reachable from root.

Returns: Filled Stats.

Definition at line 744 of file dDNNF.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ probabilityEvaluation()

double dDNNF::probabilityEvaluation ( ) const

Compute the exact probability of the d-DNNF being true.

Requires the circuit to be smooth. Uses the structural properties of the d-DNNF to evaluate in time linear in the circuit size.

Returns: Probability in [0, 1].

Definition at line 141 of file dDNNF.cpp.

Here is the call graph for this function:

◆ setRoot()

void dDNNF::setRoot ( gate_t g )

inline

Set the root gate.

Parameters

g	New root gate.

Definition at line 127 of file dDNNF.h.

Here is the caller graph for this function:

◆ shapley()

double dDNNF::shapley ( gate_t var ) const

Compute the Shapley value of input gate var.

Implements the polynomial-time Shapley-value algorithm for d-DNNFs described in Livshits et al. (PODS 2021).

Parameters

var	Input gate whose Shapley value is requested.

Returns: Shapley value.

Definition at line 526 of file dDNNF.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ shapley_alpha()

std::vector< std::vector< double > > dDNNF::shapley_alpha ( ) const

private

Compute the α table used in the Shapley algorithm.

Returns a 2-D vector of α coefficients that weight the δ values when computing the Shapley value of each input gate.

Returns: 2-D vector of α coefficients (indexed by defection count).

Definition at line 422 of file dDNNF.cpp.

Here is the call graph for this function:

◆ shapley_delta()

std::unordered_map< gate_t, std::vector< double > > dDNNF::shapley_delta ( ) const

private

Compute the δ table used in the Shapley algorithm.

Returns a map from each input gate to a vector of δ values (one per possible "defection count"), as described in the algorithm of Choicenet / Livshits et al.

Returns: Map from each input gate to its vector of δ values.

Definition at line 320 of file dDNNF.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ simplify()

void dDNNF::simplify ( )

Simplify the d-DNNF by removing redundant constants.

Propagates constant true / false values upward and removes gates that have become trivially constant after conditioning.

Definition at line 604 of file dDNNF.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ toDot()

std::string dDNNF::toDot ( ) const

Return a GraphViz DOT representation of the d-DNNF.

Walks gates reachable from root and emits a digraph with one node per gate (AND as "∧", OR as "∨", NOT as "¬", IN labelled by the short prefix of its UUID and its probability). The root node is rendered with a thicker border. Unreachable or unset gates are skipped.

Returns: DOT source as a string.

Definition at line 903 of file dDNNF.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ toNNF()

std::string dDNNF::toNNF ( const std::function< int(const std::string &)> & var_of_uuid = {} ) const

Serialise the d-DNNF in the c2d / d4 ".nnf" text format.

Header "nnf <#nodes> <#edges> <#vars>", then one line per node in an order where children precede parents:

"L <lit>" –literal leaf: an IN gate is +var, a NOT over an input is -var.
"A <k> <c1>..<ck>" --AND over k earlier nodes ("A 0" is constant true).
"O <j> <k> <c1>..<ck>" –OR; j is the decision variable or 0 when none is recorded. ProvSQL does not track it, so j is always 0 ("O 0 0" is constant false).

Parameters

var_of_uuid optional map from an input's original-circuit UUID to its variable index. When supplied, input variables use this numbering (so a .nnf and the tseytin_cnf of the same circuit cross-reference, even when an external compiler renumbered the variables internally); a UUID it does not know, or an empty callback, falls back to the d-DNNF's own gate id.

Returns: NNF text.

Exceptions

CircuitException if a NOT gate is not directly over an input (the circuit is then not in negation normal form).

Definition at line 811 of file dDNNF.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ topological_order()

std::vector< gate_t > dDNNF::topological_order ( const std::vector< std::vector< gate_t > > & reversedWires ) const

private

Compute a topological ordering of the circuit.

Parameters

reversedWires Adjacency list of the reversed wires.

Returns: Gates in topological order (leaves first).

Definition at line 581 of file dDNNF.cpp.

Here is the caller graph for this function:

◆ vars()

std::unordered_set< gate_t > dDNNF::vars ( gate_t root ) const

Return the set of all variable (IN) gates reachable from root.

Parameters

root	Root gate of the sub-circuit.

Returns: Set of reachable IN gate identifiers.

Definition at line 33 of file dDNNF.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ BooleanCircuit::compilation

dDNNF BooleanCircuit::compilation	(	gate_t	g,
		std::string	compiler,
		std::string *	resolved ) const

friend

Allowed to access internal d-DNNF state.

Member Data Documentation

◆ dDNNFTreeDecompositionBuilder

friend dDNNF::dDNNFTreeDecompositionBuilder

Allowed to construct and populate this d-DNNF.

Definition at line 283 of file dDNNF.h.

◆ probability_cache

std::unordered_map<gate_t, double, hash_gate_t> dDNNF::probability_cache

mutableprivate

Memoisation cache mapping gates to their probability values.

Definition at line 74 of file dDNNF.h.

◆ root

gate_t dDNNF::root {0}

private

The root gate of the d-DNNF.

Definition at line 113 of file dDNNF.h.

◆ StructuredDNNFBuilder

friend dDNNF::StructuredDNNFBuilder

Inversion-free structured builder: constructs and populates this d-DNNF.

Definition at line 284 of file dDNNF.h.

The documentation for this class was generated from the following files:

/home/senellar/git/software/provsql/src/dDNNF.h
/home/senellar/git/software/provsql/src/dDNNF.cpp

Classes

Public Member Functions

Public Attributes

Private Member Functions

Private Attributes

Friends

Additional Inherited Members

Detailed Description

Member Function Documentation

◆ banzhaf()

◆ banzhaf_internal()

◆ condition()

◆ conditionAndSimplify()

◆ getRoot()

◆ makeGatesBinary()

◆ makeSmooth()

◆ nodeStats()

◆ probabilityEvaluation()

◆ setRoot()

◆ shapley()

◆ shapley_alpha()

◆ shapley_delta()

◆ simplify()

◆ toDot()

◆ toNNF()

◆ topological_order()

◆ vars()

Friends And Related Symbol Documentation

◆ BooleanCircuit::compilation

Member Data Documentation

◆ dDNNFTreeDecompositionBuilder

◆ probability_cache

◆ root

◆ StructuredDNNFBuilder