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]

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`.

Public Member Functions inherited from BooleanCircuit
	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.

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) const
	Compile the sub-circuit rooted at `g` to a `dDNNF` via an external tool.

double	monteCarlo (gate_t g, unsigned samples) const
	Estimate the probability via Monte Carlo sampling.

double	WeightMC (gate_t g, std::string opt) const
	Compute the probability using the `weightmc` model 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.

virtual std::string	toString (gate_t g) const override
	Return a textual description of gate `g` for debugging.

std::string	exportCircuit (gate_t g) const
	Export the circuit in the textual format expected by external compilers.

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`.

const std::vector< gate_t > &	getWires (gate_t g) const
	Return a const 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`.

virtual gate_t	setGate (BooleanGate type)
	Allocate a new gate with type `type` and no UUID.

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.

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) const
	Allowed to access internal d-DNNF state.

Additional Inherited Members
Public Types inherited from Circuit< BooleanGate >
using	uuid = std::string
	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 69 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 543 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 217 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 553 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 118 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 104 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 57 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 137 of file dDNNF.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ setRoot()

void dDNNF::setRoot ( gate_t g )

inline

Set the root gate.

Parameters

g	New root gate.

Definition at line 125 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 515 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 411 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 309 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 593 of file dDNNF.cpp.

Here is the call 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 570 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 29 of file dDNNF.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

Friends And Related Symbol Documentation

◆ BooleanCircuit::compilation

dDNNF BooleanCircuit::compilation	(	gate_t	g,
		std::string	compiler
	)		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 217 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 72 of file dDNNF.h.

◆ root

gate_t dDNNF::root {0}

private

The root gate of the d-DNNF.

Definition at line 111 of file dDNNF.h.

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

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

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()

◆ probabilityEvaluation()

◆ setRoot()

◆ shapley()

◆ shapley_alpha()

◆ shapley_delta()

◆ simplify()

◆ topological_order()

◆ vars()

Friends And Related Symbol Documentation

◆ BooleanCircuit::compilation

Member Data Documentation

◆ dDNNFTreeDecompositionBuilder

◆ probability_cache

◆ root