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. Amarilli, F. Capelli, M. Monet, P. Senellart, "Connecting Knowledge Compilation Classes and Width Parameters". Theory of Computing Systems 64(5):861–914, 2020. https://doi.org/10.1007/s00224-019-09930-2

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.