Tree decomposition of a Boolean circuit's primal graph. More...

#include "TreeDecomposition.h"

Public Types
template<class T >
using	small_vector = boost::container::static_vector< T, MAX_TREEWIDTH+1 >
	Stack-allocated vector type bounded by `MAX_TREEWIDTH+1` elements.

using	Bag = flat_set< gate_t, small_vector >
	The type of a bag: a small flat set of gate IDs.

Public Member Functions
	TreeDecomposition (const BooleanCircuit &bc)
	Compute a tree decomposition of the primal graph of `bc`.

	TreeDecomposition (std::istream &in)
	Parse a tree decomposition from a stream (PACE challenge format).

	TreeDecomposition (const TreeDecomposition &td)
	Copy constructor.

TreeDecomposition &	operator= (const TreeDecomposition &td)
	Copy assignment.

unsigned	getTreewidth () const
	Return the treewidth of this decomposition.

void	makeFriendly (gate_t root)
	Restructure the tree into the friendly normal form.

std::string	toDot () const
	Render the tree decomposition as a GraphViz DOT string.

Static Public Attributes
static constexpr int	MAX_TREEWIDTH = 10
	Maximum supported treewidth.

static constexpr int	OPTIMAL_ARITY = 2
	Preferred maximum arity of bags in the friendly form.

Private Member Functions
	TreeDecomposition ()=default

bag_t	findGateConnection (gate_t v) const
	Find the bag whose gate set is closest to gate `v` (for rooting).

void	reroot (bag_t bag)
	Re-root the tree so that `bag` becomes the root.

bag_t	addEmptyBag (bag_t parent, const std::vector< bag_t > &children=std::vector< bag_t >())
	Insert a new empty bag as a child of `parent`.

void	addGateToBag (gate_t g, bag_t b)
	Add gate `g` to the contents of bag `b`.

Bag &	getBag (bag_t b)
	Mutable access to bag `b`.

const Bag &	getBag (bag_t b) const
	Const access to bag `b`.

std::vector< bag_t > &	getChildren (bag_t b)
	Mutable access to the children of bag `b`.

const std::vector< bag_t > &	getChildren (bag_t b) const
	Const access to the children of bag `b`.

bag_t	getParent (bag_t b) const
	Return the parent of bag `b`.

void	setParent (bag_t b, bag_t p)
	Set the parent of bag `b` to `p`.

Private Attributes
std::vector< Bag >	bags
	Bag contents, indexed by `bag_t`.

std::vector< bag_t >	parent
	Parent of each bag (root points to itself)

std::vector< std::vector< bag_t > >	children
	Children of each bag.

bag_t	root
	Identifier of the root bag.

unsigned	treewidth
	Treewidth of the decomposition.

Friends
class	dDNNFTreeDecompositionBuilder

std::istream &	operator>> (std::istream &in, TreeDecomposition &td)
	Read a tree decomposition in PACE challenge format.

Detailed Description

Tree decomposition of a Boolean circuit's primal graph.

Provides constructors that compute the decomposition from a BooleanCircuit using the min-fill heuristic, or parse it from an input stream. After construction, makeFriendly() restructures the tree into the "friendly" normal form required by dDNNFTreeDecompositionBuilder.

Definition at line 57 of file TreeDecomposition.h.

Member Typedef Documentation

◆ Bag

using TreeDecomposition::Bag = flat_set<gate_t, small_vector>

The type of a bag: a small flat set of gate IDs.

Definition at line 73 of file TreeDecomposition.h.

◆ small_vector

template<class T >

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

Stack-allocated vector type bounded by MAX_TREEWIDTH+1 elements.

Used for bag contents to avoid heap allocation for small, bounded sets.

Definition at line 70 of file TreeDecomposition.h.

Constructor & Destructor Documentation

◆ TreeDecomposition() [1/4]

TreeDecomposition::TreeDecomposition ( )

privatedefault

◆ TreeDecomposition() [2/4]

TreeDecomposition::TreeDecomposition ( const BooleanCircuit & bc )

Compute a tree decomposition of the primal graph of bc.

Uses the min-fill elimination ordering heuristic. Throws TreeDecompositionException if the computed treewidth exceeds MAX_TREEWIDTH.

Parameters

bc	The Boolean circuit to decompose.

Definition at line 285 of file TreeDecomposition.cpp.

Here is the call graph for this function:

◆ TreeDecomposition() [3/4]

TreeDecomposition::TreeDecomposition ( std::istream & in )

Parse a tree decomposition from a stream (PACE challenge format).

Parameters

in	Input stream containing the decomposition.

Definition at line 34 of file TreeDecomposition.cpp.

◆ TreeDecomposition() [4/4]

TreeDecomposition::TreeDecomposition ( const TreeDecomposition & td )

Copy constructor.

Parameters

td	Source decomposition.

Member Function Documentation

◆ addEmptyBag()

bag_t TreeDecomposition::addEmptyBag	(	bag_t	parent,
		const std::vector< bag_t > &	children = `std::vector<bag_t>()`
	)

private

Insert a new empty bag as a child of parent.

Parameters

parent	Parent bag of the new empty bag.
children	Children to transfer from `parent` to the new bag.

Returns: ID of the newly created bag.

Definition at line 159 of file TreeDecomposition.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ addGateToBag()

void TreeDecomposition::addGateToBag	(	gate_t	g,
		bag_t	b
	)

private

Add gate g to the contents of bag b.

Parameters

g	Gate to add.
b	Destination bag.

Definition at line 179 of file TreeDecomposition.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ findGateConnection()

bag_t TreeDecomposition::findGateConnection ( gate_t v ) const

private

Find the bag whose gate set is closest to gate v (for rooting).

Parameters

v	Gate to search for.

Returns: ID of the bag that contains or is nearest to v.

Definition at line 41 of file TreeDecomposition.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ getBag() [1/2]

Bag & TreeDecomposition::getBag ( bag_t b )

inlineprivate

Mutable access to bag b.

Parameters

b	Bag identifier.

Returns: Reference to the bag's gate set.

Definition at line 114 of file TreeDecomposition.h.

Here is the caller graph for this function:

◆ getBag() [2/2]

const Bag & TreeDecomposition::getBag ( bag_t b ) const

inlineprivate

Const access to bag b.

Parameters

b	Bag identifier.

Returns: Const reference to the bag's gate set.

Definition at line 123 of file TreeDecomposition.h.

◆ getChildren() [1/2]

std::vector< bag_t > & TreeDecomposition::getChildren ( bag_t b )

inlineprivate

Mutable access to the children of bag b.

Parameters

b	Bag identifier.

Returns: Reference to the vector of child bag IDs.

Definition at line 132 of file TreeDecomposition.h.

Here is the caller graph for this function:

◆ getChildren() [2/2]

const std::vector< bag_t > & TreeDecomposition::getChildren ( bag_t b ) const

inlineprivate

Const access to the children of bag b.

Parameters

b	Bag identifier.

Returns: Const reference to the vector of child bag IDs.

Definition at line 141 of file TreeDecomposition.h.

◆ getParent()

bag_t TreeDecomposition::getParent ( bag_t b ) const

inlineprivate

Return the parent of bag b.

Parameters

b	Bag identifier.

Returns: Parent bag identifier.

Definition at line 150 of file TreeDecomposition.h.

Here is the caller graph for this function:

◆ getTreewidth()

unsigned TreeDecomposition::getTreewidth ( ) const

inline

Return the treewidth of this decomposition.

Returns: Treewidth (maximum bag size minus one).

Definition at line 196 of file TreeDecomposition.h.

Here is the caller graph for this function:

◆ makeFriendly()

void TreeDecomposition::makeFriendly ( gate_t root )

Restructure the tree into the friendly normal form.

Reroots the tree at the bag that covers the circuit's root gate and splits/merges bags so that dDNNFTreeDecompositionBuilder can process them efficiently.

Parameters

root	The gate that should be covered by the root bag.

Definition at line 59 of file TreeDecomposition.cpp.

Here is the call graph for this function:

◆ operator=()

TreeDecomposition & TreeDecomposition::operator= ( const TreeDecomposition & td )

Copy assignment.

Parameters

td	Source decomposition.

Returns: Reference to this decomposition after assignment.

◆ reroot()

void TreeDecomposition::reroot ( bag_t bag )

private

Re-root the tree so that bag becomes the root.

Parameters

bag	The bag to use as the new root.

Definition at line 184 of file TreeDecomposition.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ setParent()

void TreeDecomposition::setParent	(	bag_t	b,
		bag_t	p
	)

inlineprivate

Set the parent of bag b to p.

Parameters

b	Bag whose parent is to be set.
p	New parent bag.

Definition at line 159 of file TreeDecomposition.h.

Here is the caller graph for this function:

◆ toDot()

std::string TreeDecomposition::toDot ( ) const

Render the tree decomposition as a GraphViz DOT string.

Returns: DOT digraph string for visualisation.

Definition at line 206 of file TreeDecomposition.cpp.

Here is the call graph for this function:

Friends And Related Symbol Documentation

◆ dDNNFTreeDecompositionBuilder

friend class dDNNFTreeDecompositionBuilder

friend

Definition at line 218 of file TreeDecomposition.h.

◆ operator>>

std::istream & operator>>	(	std::istream &	in,
		TreeDecomposition &	td
	)

friend

Read a tree decomposition in PACE challenge format.

Parameters

in	Input stream.
td	Tree decomposition to populate.

Returns: Reference to in.

Definition at line 232 of file TreeDecomposition.cpp.

Member Data Documentation

◆ bags

std::vector<Bag> TreeDecomposition::bags

private

Bag contents, indexed by bag_t.

Definition at line 76 of file TreeDecomposition.h.

◆ children

std::vector<std::vector<bag_t> > TreeDecomposition::children

private

Children of each bag.

Definition at line 78 of file TreeDecomposition.h.

◆ MAX_TREEWIDTH

constexpr int TreeDecomposition::MAX_TREEWIDTH = 10

staticconstexpr

Maximum supported treewidth.

Circuits exceeding this cause an error.

Definition at line 60 of file TreeDecomposition.h.

◆ OPTIMAL_ARITY

constexpr int TreeDecomposition::OPTIMAL_ARITY = 2

staticconstexpr

Preferred maximum arity of bags in the friendly form.

Definition at line 62 of file TreeDecomposition.h.

◆ parent

std::vector<bag_t> TreeDecomposition::parent

private

Parent of each bag (root points to itself)

Definition at line 77 of file TreeDecomposition.h.

◆ root

bag_t TreeDecomposition::root

private

Identifier of the root bag.

Definition at line 79 of file TreeDecomposition.h.

◆ treewidth

unsigned TreeDecomposition::treewidth

private

Treewidth of the decomposition.

Definition at line 80 of file TreeDecomposition.h.

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

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

Public Types

Public Member Functions

Static Public Attributes

Private Member Functions

Private Attributes

Friends

Detailed Description

Member Typedef Documentation

◆ Bag

◆ small_vector

Constructor & Destructor Documentation

◆ TreeDecomposition() [1/4]

◆ TreeDecomposition() [2/4]

◆ TreeDecomposition() [3/4]

◆ TreeDecomposition() [4/4]

Member Function Documentation

◆ addEmptyBag()

◆ addGateToBag()

◆ findGateConnection()

◆ getBag() [1/2]

◆ getBag() [2/2]

◆ getChildren() [1/2]

◆ getChildren() [2/2]

◆ getParent()

◆ getTreewidth()

◆ makeFriendly()

◆ operator=()

◆ reroot()

◆ setParent()

◆ toDot()

Friends And Related Symbol Documentation

◆ dDNNFTreeDecompositionBuilder

◆ operator>>

Member Data Documentation

◆ bags

◆ children

◆ MAX_TREEWIDTH

◆ OPTIMAL_ARITY

◆ parent

◆ root

◆ treewidth