dDNNFTreeDecompositionBuilder.h File Reference

Constructs a d-DNNF from a Boolean circuit and its tree decomposition. More...

#include <cassert>
#include <unordered_map>
#include <map>
#include <boost/container/static_vector.hpp>
#include "flat_map.hpp"
#include "flat_set.hpp"
#include "TreeDecomposition.h"
#include "dDNNF.h"
#include "BooleanCircuit.h"

Include dependency graph for dDNNFTreeDecompositionBuilder.h:

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

Go to the source code of this file.

Classes
class	dDNNFTreeDecompositionBuilder
	Builds a d-DNNF from a Boolean circuit using a tree decomposition. More...
struct	dDNNFTreeDecompositionBuilder::dDNNFGate
	Intermediate representation of a partially built d-DNNF gate. More...

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

Detailed Description

Constructs a d-DNNF from a Boolean circuit and its tree decomposition.

dDNNFTreeDecompositionBuilder implements the knowledge-compilation algorithm described in:

‍A. Jha and D. Suciu, "Knowledge Compilation Meets Database Theory: Compiling Queries to d-DNNFs". ICDT 2013.

The algorithm traverses the tree decomposition bottom-up. At each bag it enumerates valuations (assignments of Boolean values to the gates in the bag) that are consistent with the circuit's constraints. For each valuation it builds a d-DNNF AND gate whose children are the (negated) input gates for that valuation. The OR combination of all valid valuations at the root bag gives the final d-DNNF.

Key types

• valuation_t: a flat_map<gate_t, bool> (bounded by treewidth+1) mapping each in-bag gate to its truth value.
• suspicious_t: a flat_set<gate_t> of gates whose values have not yet been "confirmed" by their responsible bag.
• dDNNFGate: an intermediate gate in the constructed d-DNNF, bundling a gate ID with a valuation and a suspicious set.
• gates_to_or_t: the main DP table mapping (valuation, suspicious) pairs to lists of dDNNFGate children to be OR'd.

Usage

dDNNFTreeDecompositionBuilder builder(circuit, root_gate, td);
dDNNF dd = std::move(builder).build();

Definition in file dDNNFTreeDecompositionBuilder.h.

Function Documentation

operator<<()

std::ostream & operator<<	(	std::ostream &	o,
		const dDNNFTreeDecompositionBuilder::dDNNFGate &	g
	)

Debug output for a dDNNFTreeDecompositionBuilder::dDNNFGate.

Parameters

o	Output stream.
g	Gate to display.

Returns

Reference to o.

Definition at line 207 of file dDNNFTreeDecompositionBuilder.cpp.

Here is the call graph for this function: