Builds a d-DNNF from a Boolean circuit using a tree decomposition. More...

#include "dDNNFTreeDecompositionBuilder.h"

Collaboration diagram for dDNNFTreeDecompositionBuilder:

[legend]

Classes
struct	dDNNFGate
	Intermediate representation of a partially built d-DNNF gate. More...

Public Types
template<class T >
using	small_vector = boost::container::static_vector< T, TreeDecomposition::MAX_TREEWIDTH+1 >
	Stack-allocated vector bounded by the maximum treewidth + 1.

using	valuation_t = flat_map< gate_t, bool, small_vector >
	Partial assignment of truth values to the gates of a bag.

using	suspicious_t = flat_set< gate_t, small_vector >
	Set of gates whose truth-value assignments are not yet confirmed.

template<class T >
using	gate_vector_t = std::vector< T >
	Generic bounded-capacity vector for intermediate d-DNNF gates.

using	gates_to_or_t = std::unordered_map< valuation_t, std::map< suspicious_t, gate_vector_t< gate_t > > >
	Dynamic-programming table: (valuation, suspicious) → list of children.

Public Member Functions
	dDNNFTreeDecompositionBuilder (const BooleanCircuit &circuit, gate_t gate, TreeDecomposition &tree_decomposition)
	Construct the builder for a specific circuit and tree decomposition.

dDNNF &&	build () &&
	Execute the compilation and return the resulting d-DNNF.

Private Member Functions
gates_to_or_t	collectGatesToOr (bag_t bag, const gate_vector_t< dDNNFGate > &gates, const gates_to_or_t &partial)
	Group a list of `dDNNFGate` entries by (valuation, suspicious) pairs.

gate_vector_t< dDNNFGate >	builddDNNFLeaf (bag_t bag)
	Build the d-DNNF contributions for a leaf bag.

gate_vector_t< dDNNFGate >	builddDNNF ()
	Main recursive procedure: build the d-DNNF bottom-up.

bool	circuitHasWire (gate_t u, gate_t v) const
	Return `true` if there is a wire from gate `u` to gate `v`.

bool	isAlmostValuation (const valuation_t &valuation) const
	Return `true` if `valuation` is a "almost valuation".

suspicious_t	getInnocent (const valuation_t &valuation, const suspicious_t &innocent) const
	Compute the subset of `innocent` that remains innocent.

Private Attributes
const BooleanCircuit &	c
	Source circuit.

gate_t	root_id
	Root gate of the source circuit.

TreeDecomposition &	td
	Tree decomposition of the circuit's primal graph.

dDNNF	d
	The d-DNNF being constructed.

std::unordered_map< gate_t, bag_t >	responsible_bag
	Maps each gate to its "responsible" bag.

std::unordered_map< gate_t, gate_t >	input_gate
	Maps original IN gates to d-DNNF IN gates.

std::unordered_map< gate_t, gate_t >	negated_input_gate
	Maps original IN gates to their negations.

std::set< std::pair< gate_t, gate_t > >	wiresSet
	Set of all wires in the source circuit.

Friends
std::ostream &	operator<< (std::ostream &o, const dDNNFGate &g)
	Debug output for a `dDNNFTreeDecompositionBuilder::dDNNFGate`.

Detailed Description

Builds a d-DNNF from a Boolean circuit using a tree decomposition.

This class is a one-shot builder: construct it, call build(), and the object is consumed (move-only).

Definition at line 54 of file dDNNFTreeDecompositionBuilder.h.

Member Typedef Documentation

◆ gate_vector_t

template<class T >

using dDNNFTreeDecompositionBuilder::gate_vector_t = std::vector<T>

Generic bounded-capacity vector for intermediate d-DNNF gates.

Definition at line 69 of file dDNNFTreeDecompositionBuilder.h.

◆ gates_to_or_t

using dDNNFTreeDecompositionBuilder::gates_to_or_t = std::unordered_map<valuation_t, std::map<suspicious_t, gate_vector_t<gate_t> > >

Dynamic-programming table: (valuation, suspicious) → list of children.

Definition at line 72 of file dDNNFTreeDecompositionBuilder.h.

◆ small_vector

template<class T >

using dDNNFTreeDecompositionBuilder::small_vector = boost::container::static_vector<T, TreeDecomposition::MAX_TREEWIDTH+1>

Stack-allocated vector bounded by the maximum treewidth + 1.

Definition at line 59 of file dDNNFTreeDecompositionBuilder.h.

◆ suspicious_t

using dDNNFTreeDecompositionBuilder::suspicious_t = flat_set<gate_t, small_vector>

Set of gates whose truth-value assignments are not yet confirmed.

Definition at line 65 of file dDNNFTreeDecompositionBuilder.h.

◆ valuation_t

using dDNNFTreeDecompositionBuilder::valuation_t = flat_map<gate_t, bool, small_vector>

Partial assignment of truth values to the gates of a bag.

Definition at line 62 of file dDNNFTreeDecompositionBuilder.h.

Constructor & Destructor Documentation

◆ dDNNFTreeDecompositionBuilder()

dDNNFTreeDecompositionBuilder::dDNNFTreeDecompositionBuilder	(	const BooleanCircuit &	circuit,
		gate_t	gate,
		TreeDecomposition &	tree_decomposition
	)

inline

Construct the builder for a specific circuit and tree decomposition.

Pre-computes the wire set for fast circuitHasWire() queries.

Parameters

circuit	Source Boolean circuit.
gate	Root gate of `circuit` to compile.
tree_decomposition	Tree decomposition of `circuit's` primal graph.

Definition at line 186 of file dDNNFTreeDecompositionBuilder.h.

Here is the call graph for this function:

Member Function Documentation

◆ build()

dDNNF && dDNNFTreeDecompositionBuilder::build ( ) &&

Execute the compilation and return the resulting d-DNNF.

This is a move-only operation: the builder object is consumed.

Returns: The compiled dDNNF (as an rvalue).

Definition at line 34 of file dDNNFTreeDecompositionBuilder.cpp.

◆ builddDNNF()

dDNNFTreeDecompositionBuilder::gate_vector_t< dDNNFTreeDecompositionBuilder::dDNNFGate > dDNNFTreeDecompositionBuilder::builddDNNF ( )

private

Main recursive procedure: build the d-DNNF bottom-up.

Returns: List of dDNNFGate entries at the root bag.

Definition at line 378 of file dDNNFTreeDecompositionBuilder.cpp.

Here is the call graph for this function:

◆ builddDNNFLeaf()

dDNNFTreeDecompositionBuilder::gate_vector_t< dDNNFTreeDecompositionBuilder::dDNNFGate > dDNNFTreeDecompositionBuilder::builddDNNFLeaf ( bag_t bag )

private

Build the d-DNNF contributions for a leaf bag.

Enumerates all consistent valuations for the gates in the leaf bag and creates the corresponding d-DNNF AND gates.

Parameters

bag	The leaf bag to process.

Returns: List of dDNNFGate entries, one per consistent valuation.

Definition at line 114 of file dDNNFTreeDecompositionBuilder.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ circuitHasWire()

bool dDNNFTreeDecompositionBuilder::circuitHasWire	(	gate_t	u,
		gate_t	v
	)		const

private

Return true if there is a wire from gate u to gate v.

Parameters

u	Source gate.
v	Target gate.

Returns: true if a wire from u to v exists in the source circuit.

Definition at line 490 of file dDNNFTreeDecompositionBuilder.cpp.

Here is the caller graph for this function:

◆ collectGatesToOr()

dDNNFTreeDecompositionBuilder::gates_to_or_t dDNNFTreeDecompositionBuilder::collectGatesToOr	(	bag_t	bag,
		const gate_vector_t< dDNNFGate > &	gates,
		const gates_to_or_t &	partial
	)

private

Group a list of dDNNFGate entries by (valuation, suspicious) pairs.

Used when processing a bag's children to identify which sub-results can be OR'd together.

Parameters

bag	Current bag being processed.
gates	List of d-DNNF gates from child bags.
partial	Partially accumulated DP table from previous children.

Returns: Updated DP table.

Definition at line 277 of file dDNNFTreeDecompositionBuilder.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ getInnocent()

dDNNFTreeDecompositionBuilder::suspicious_t dDNNFTreeDecompositionBuilder::getInnocent	(	const valuation_t &	valuation,
		const suspicious_t &	innocent
	)		const