StructuredDNNF.h File Reference

In-process structured-d-DNNF construction over a query-derived variable order, for the inversion-free UCQ(OBDD) probability path. More...

#include "BooleanCircuit.h"
#include "dDNNF.h"
#include <map>
#include <string>
#include <tuple>
#include <unordered_map>
#include <vector>
#include <cstddef>

Include dependency graph for StructuredDNNF.h:

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

Go to the source code of this file.

Classes
class	StructuredDNNFBuilder
	Top-down structured-d-DNNF builder over a query-derived variable order. More...
struct	StructuredDNNFBuilder::InputKey
	Structured per-input order key carried by the planner's markers. More...
struct	StructuredDNNFBuilder::CacheKey
struct	StructuredDNNFBuilder::CacheKeyHash

Detailed Description

In-process structured-d-DNNF construction over a query-derived variable order, for the inversion-free UCQ(OBDD) probability path.

Given a BooleanCircuit (monotone AND / OR / IN over independent inputs) and a total order on its input variables, compile the function into a ProvSQL dDNNF and read off its probability (inputs independent Bernoulli). For an inversion-free query the query-derived (Prop. 4.5) order yields a d-DNNF of size linear in the lineage, where the generic methods (tree-decomposition, d4) blow up.

Pure C++ (BooleanCircuit + STL, no PostgreSQL headers) so it builds both in the extension and the standalone -DTDKC harness.

Definition in file StructuredDNNF.h.