TreeDecomposition.h File Reference

Tree decomposition of a Boolean circuit for knowledge compilation. More...

#include <iostream>
#include <string>
#include <type_traits>
#include <vector>
#include <boost/container/static_vector.hpp>
#include "flat_set.hpp"
#include "BooleanCircuit.h"

Include dependency graph for TreeDecomposition.h:

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

Go to the source code of this file.

Classes
class	TreeDecomposition
	Tree decomposition of a Boolean circuit's primal graph. More...
class	TreeDecompositionException
	Exception thrown when a tree decomposition cannot be constructed. More...

Enumerations
enum class	bag_t : size_t
	Strongly-typed bag identifier for a tree decomposition. More...

Functions
std::istream &	operator>> (std::istream &in, TreeDecomposition &td)
	Read a tree decomposition in PACE challenge format.
bag_t &	operator++ (bag_t &b)
	Pre-increment operator for bag_t.
bag_t	operator++ (bag_t &b, int)
	Post-increment operator for bag_t.
bool	operator< (bag_t t, std::vector< bag_t >::size_type u)
	Compare a bag_t against a std::vector size type.
std::string	to_string (bag_t b)
	Convert a bag_t to its decimal string representation.
std::istream &	operator>> (std::istream &i, bag_t &b)
	Read a bag_t from an input stream.

Detailed Description

Tree decomposition of a Boolean circuit for knowledge compilation.

A tree decomposition of a graph \(G=(V,E)\) is a tree \(T\) whose nodes are labelled with bags (subsets of \(V\)) such that:

1. Every vertex of \(G\) appears in at least one bag.
2. For every edge \((u,v)\in E\), some bag contains both \(u\) and \(v\).
3. For every vertex \(v\), the bags containing \(v\) form a connected sub-tree of \(T\).

The treewidth is one less than the maximum bag size. ProvSQL builds a tree decomposition of the primal graph of a BooleanCircuit (using the min-fill elimination heuristic via PermutationStrategy) and then feeds it to dDNNFTreeDecompositionBuilder to construct a d-DNNF. Tractable compilation is guaranteed when the treewidth is bounded (empirically ≤ MAX_TREEWIDTH).

The decomposition can also be read from an external file in the standard PACE challenge format (via the streaming operator>>).

bag_t is a strongly-typed wrapper around size_t, analogous to gate_t, used as a bag identifier within the tree.

Definition in file TreeDecomposition.h.

Enumeration Type Documentation

bag_t

enum class bag_t : size_t

strong

Strongly-typed bag identifier for a tree decomposition.

Wraps a size_t, analogous to gate_t.

Definition at line 46 of file TreeDecomposition.h.

Function Documentation

operator++() [1/2]

bag_t & operator++ ( bag_t &  b )

inline

Pre-increment operator for bag_t.

Parameters

b	Bag to increment.

Returns

Reference to the incremented bag.

Definition at line 234 of file TreeDecomposition.h.

operator++() [2/2]

bag_t operator++ ( bag_t &  b, int    )

inline

Post-increment operator for bag_t.

Parameters

b	Bag to increment.

Returns

Original value of b before the increment.

Definition at line 242 of file TreeDecomposition.h.

operator<()

bool operator< ( bag_t  t, std::vector< bag_t >::size_type  u  )

inline

Compare a bag_t against a std::vector size type.

Parameters

t	Bag identifier.
u	Size to compare against.

Returns

true if the underlying integer of t is less than u.

Definition at line 254 of file TreeDecomposition.h.

operator>>() [1/2]

std::istream & operator>> ( std::istream &  i, bag_t &  b  )

inline

Read a bag_t from an input stream.

Parameters

i	Input stream.
b	Bag to populate.

Returns

Reference to i.

Definition at line 274 of file TreeDecomposition.h.

operator>>() [2/2]

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

Read a tree decomposition in PACE challenge format.

Parameters

in	Input stream.
td	Tree decomposition to populate.

Returns

Reference to in.

Definition at line 217 of file TreeDecomposition.cpp.

to_string()

std::string to_string ( bag_t  b )

inline

Convert a bag_t to its decimal string representation.

Parameters

b	Bag identifier.

Returns

Decimal string of the underlying integer.

Definition at line 264 of file TreeDecomposition.h.

Here is the caller graph for this function: