Top-down structured-d-DNNF builder over a query-derived variable order. More...

#include "StructuredDNNF.h"

Collaboration diagram for StructuredDNNFBuilder:

[legend]

Classes
struct	InputKey
	Structured per-input order key carried by the planner's markers. More...
struct	CacheKey
struct	CacheKeyHash

Public Member Functions
	StructuredDNNFBuilder (const BooleanCircuit &bc, gate_t root, const std::map< gate_t, int > &input_rank, std::size_t max_nodes=0)
const dDNNF &	dnnf () const
	The constructed d-DNNF (root set, simplified).
gate_t	rootGate () const
	Root gate of the constructed d-DNNF (current after simplify).
double	probability () const
	Probability that the function is true (independent inputs).
std::size_t	size () const
	d-DNNF gates reachable from the root.

Static Public Attributes
static constexpr int	GUARD_FACTOR = -1

Private Types
using	Var = int
	Variable rank in [0,ninputs).
using	Term = std::vector<Var>
	A product: sorted, duplicate-free vars.
using	DNF = std::vector<Term>
	A sum of products: canonicalised.

Private Member Functions
DNF	extract (const BooleanCircuit &bc, gate_t g, const std::map< gate_t, int > &rank, std::map< gate_t, DNF > &memo) const
std::vector< DNF >	orDecompose (const DNF &d) const
std::vector< DNF >	andDecompose (const DNF &d) const
gate_t	mkAnd (const std::vector< gate_t > &children)
gate_t	mkLit (Var v)
	shared positive literal IN
gate_t	mkNeg (Var v)
	shared negative literal NOT(IN)
gate_t	newGate (BooleanGate type)
	setGate + size guard
gate_t	build (const DNF &d, gate_t false_sink)

Static Private Member Functions
static DNF	canonical (DNF d)
	sort, dedup, drop supersets
static DNF	condition (const DNF &d, Var v, bool value)

Private Attributes
dDNNF	dd_
gate_t	root_
std::size_t	max_nodes_
std::vector< double >	prob_
	prob_[rank] = P(variable)
std::vector< std::string >	uuid_
	rank -> source input UUID (for labels)
std::vector< gate_t >	in_gate_
	rank -> shared dDNNF IN gate
std::vector< gate_t >	not_gate_
	rank -> shared dDNNF NOT(IN) gate (lazy)
gate_t	true_gate_
gate_t	false_gate_
	empty AND / empty OR terminals
std::unordered_map< CacheKey, gate_t, CacheKeyHash >	cache_

Detailed Description

Top-down structured-d-DNNF builder over a query-derived variable order.

This is the §4 construction of the inversion-free plan: rather than the bottom-up apply of StructuredDNNF (kept above as a reference oracle), it compiles the monotone lineage top-down into a genuine ProvSQL dDNNF with two node kinds, placed by structure:

Decomposable AND at independence points. When the residual function is a product of variable-disjoint sub-functions \(\varphi_1\wedge\dots\) (the consistent-unification self-join's A-part and B-part once the shared separator variables are fixed; or a pure product term), emit a flat AND and recurse per factor. Decomposability (children share no variable) holds by construction and is the structural win an OBDD cannot express.
Deterministic OR at Shannon decisions. Otherwise pick the lowest-rank variable still present and branch on it, emitting OR(AND(v,hi),AND(¬v,lo)). Determinism (children mutually exclusive) holds because both branches come from a decision on the same variable.

A component cache (keyed on the canonical residual) shares equal sub-d-DNNFs, which is what keeps the result linear in the lineage under the Prop. 4.5 order (and bounds the work). The function is taken as a monotone DNF expanded from the BooleanCircuit (AND distributes, OR unions, IN is a single literal; NOT and multivalued inputs are rejected, out of scope for the TID inversion-free path).

Output is a finished dDNNF (root set, simplify() applied) ready for dDNNF::probabilityEvaluation(). Pure C++ so it builds in the extension and the standalone -DTDKC harness.

Definition at line 59 of file StructuredDNNF.h.

Member Typedef Documentation

◆ DNF

using StructuredDNNFBuilder::DNF = std::vector<Term>

private

A sum of products: canonicalised.

Definition at line 109 of file StructuredDNNF.h.

◆ Term

using StructuredDNNFBuilder::Term = std::vector<Var>

private

A product: sorted, duplicate-free vars.

Definition at line 108 of file StructuredDNNF.h.

◆ Var

using StructuredDNNFBuilder::Var = int

private

Variable rank in [0,ninputs).

Definition at line 107 of file StructuredDNNF.h.

Constructor & Destructor Documentation

◆ StructuredDNNFBuilder()

StructuredDNNFBuilder::StructuredDNNFBuilder	(	const BooleanCircuit &	bc,
		gate_t	root,
		const std::map< gate_t, int > &	input_rank,
		std::size_t	max_nodes = 0 )

Parameters

bc	Boolean circuit (monotone AND/OR/IN, no multivalued inputs, no NOT).
root	Root gate of the function to compile.
input_rank	Maps every IN gate reachable from `root` to a distinct rank in [0,ninputs). Lower rank = decided earlier (a Prop. 4.5-consistent order, derived by the caller).
max_nodes	Size guard: throw `CircuitException` once this many d-DNNF gates have been created (0 = no guard).

Exceptions

CircuitException on multivalued/NOT/unsupported gates, a reachable input without a rank, or the size guard tripping.

Definition at line 412 of file StructuredDNNF.cpp.

Here is the call graph for this function:

Member Function Documentation

◆ andDecompose()

std::vector< StructuredDNNFBuilder::DNF > StructuredDNNFBuilder::andDecompose ( const DNF & d ) const

private

Definition at line 131 of file StructuredDNNF.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ build()

gate_t StructuredDNNFBuilder::build	(	const DNF &	d,
		gate_t	false_sink )

private

Definition at line 354 of file StructuredDNNF.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ canonical()

StructuredDNNFBuilder::DNF StructuredDNNFBuilder::canonical ( DNF d )

staticprivate

sort, dedup, drop supersets

Definition at line 68 of file StructuredDNNF.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ condition()

StructuredDNNFBuilder::DNF StructuredDNNFBuilder::condition	(	const DNF &	d,
		Var	v,
		bool	value )

staticprivate

Definition at line 111 of file StructuredDNNF.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ dnnf()

const dDNNF & StructuredDNNFBuilder::dnnf ( ) const

inline

The constructed d-DNNF (root set, simplified).

Definition at line 95 of file StructuredDNNF.h.

Here is the caller graph for this function:

◆ extract()

StructuredDNNFBuilder::DNF StructuredDNNFBuilder::extract	(	const BooleanCircuit &	bc,
		gate_t	g,
		const std::map< gate_t, int > &	rank,
		std::map< gate_t, DNF > &	memo ) const

private

Definition at line 216 of file StructuredDNNF.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ mkAnd()

gate_t StructuredDNNFBuilder::mkAnd ( const std::vector< gate_t > & children )

private

Definition at line 298 of file StructuredDNNF.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ mkLit()

gate_t StructuredDNNFBuilder::mkLit ( Var v )

private

shared positive literal IN

Definition at line 279 of file StructuredDNNF.cpp.

Here is the caller graph for this function:

◆ mkNeg()

gate_t StructuredDNNFBuilder::mkNeg ( Var v )

private

shared negative literal NOT(IN)

Definition at line 288 of file StructuredDNNF.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ newGate()

gate_t StructuredDNNFBuilder::newGate ( BooleanGate type )

private

setGate + size guard

Definition at line 271 of file StructuredDNNF.cpp.

Here is the caller graph for this function:

◆ orDecompose()

std::vector< StructuredDNNFBuilder::DNF > StructuredDNNFBuilder::orDecompose ( const DNF & d ) const

private

Definition at line 314 of file StructuredDNNF.cpp.

Here is the caller graph for this function:

◆ probability()

double StructuredDNNFBuilder::probability ( ) const

inline

Probability that the function is true (independent inputs).

Definition at line 101 of file StructuredDNNF.h.

Here is the caller graph for this function:

◆ rootGate()

gate_t StructuredDNNFBuilder::rootGate ( ) const

inline

Root gate of the constructed d-DNNF (current after simplify).

Definition at line 98 of file StructuredDNNF.h.

◆ size()

std::size_t StructuredDNNFBuilder::size ( ) const

d-DNNF gates reachable from the root.

Definition at line 449 of file StructuredDNNF.cpp.

Here is the caller graph for this function:

Member Data Documentation

◆ cache_

std::unordered_map<CacheKey, gate_t, CacheKeyHash> StructuredDNNFBuilder::cache_

private

Definition at line 127 of file StructuredDNNF.h.

◆ dd_

dDNNF StructuredDNNFBuilder::dd_

private

Definition at line 111 of file StructuredDNNF.h.

◆ false_gate_

gate_t StructuredDNNFBuilder::false_gate_

private

empty AND / empty OR terminals

Definition at line 119 of file StructuredDNNF.h.

◆ GUARD_FACTOR

int StructuredDNNFBuilder::GUARD_FACTOR = -1

staticconstexpr

Definition at line 92 of file StructuredDNNF.h.

◆ in_gate_

std::vector<gate_t> StructuredDNNFBuilder::in_gate_

private

rank -> shared dDNNF IN gate

Definition at line 117 of file StructuredDNNF.h.

◆ max_nodes_

std::size_t StructuredDNNFBuilder::max_nodes_

private

Definition at line 113 of file StructuredDNNF.h.

◆ not_gate_

std::vector<gate_t> StructuredDNNFBuilder::not_gate_

private

rank -> shared dDNNF NOT(IN) gate (lazy)

Definition at line 118 of file StructuredDNNF.h.

◆ prob_

std::vector<double> StructuredDNNFBuilder::prob_

private

prob_[rank] = P(variable)

Definition at line 115 of file StructuredDNNF.h.

◆ root_

gate_t StructuredDNNFBuilder::root_

private

Definition at line 112 of file StructuredDNNF.h.

◆ true_gate_

gate_t StructuredDNNFBuilder::true_gate_

private

Definition at line 119 of file StructuredDNNF.h.

◆ uuid_

std::vector<std::string> StructuredDNNFBuilder::uuid_

private

rank -> source input UUID (for labels)

Definition at line 116 of file StructuredDNNF.h.

The documentation for this class was generated from the following files:

/home/pierre/git/software/provsql/src/StructuredDNNF.h
/home/pierre/git/software/provsql/src/StructuredDNNF.cpp

Classes

Public Member Functions

Static Public Attributes

Private Types

Private Member Functions

Static Private Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

◆ DNF

◆ Term

◆ Var

Constructor & Destructor Documentation

◆ StructuredDNNFBuilder()

Member Function Documentation

◆ andDecompose()

◆ build()

◆ canonical()

◆ condition()

◆ dnnf()

◆ extract()

◆ mkAnd()

◆ mkLit()

◆ mkNeg()

◆ newGate()

◆ orDecompose()

◆ probability()

◆ rootGate()

◆ size()

Member Data Documentation

◆ cache_

◆ dd_

◆ false_gate_

◆ GUARD_FACTOR

◆ in_gate_

◆ max_nodes_

◆ not_gate_

◆ prob_

◆ root_

◆ true_gate_

◆ uuid_