StructuredDNNF.cpp File Reference

Implementation of the structured-d-DNNF builder (see StructuredDNNF.h). More...

#include "StructuredDNNF.h"
#include <algorithm>
#include <functional>
#include <map>
#include <set>
#include <stdexcept>

Include dependency graph for StructuredDNNF.cpp:

Go to the source code of this file.

Detailed Description

Implementation of the structured-d-DNNF builder (see StructuredDNNF.h).

The §4 top-down construction: the monotone lineage is expanded to a canonical DNF and compiled into a ProvSQL dDNNF by decomposable AND at independence points and deterministic OR at Shannon decisions on the caller-supplied (Prop. 4.5) variable order, with a component cache sharing equal sub-d-DNNFs. Size is linear in the lineage under that order, where the generic methods (tree-decomposition, d4) blow up.

Definition in file StructuredDNNF.cpp.