dDNNFTreeDecompositionBuilder.cpp File Reference

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

#include <algorithm>
#include <stack>
#include <variant>
#include "dDNNFTreeDecompositionBuilder.h"
#include "Circuit.hpp"
#include "postgres.h"
#include "miscadmin.h"

Include dependency graph for dDNNFTreeDecompositionBuilder.cpp:

Go to the source code of this file.

Functions
constexpr bool	isStrong (BooleanGate type, bool value)
	Return true if assigning value to a gate of type type is a "strong" assignment.
static bool	isConnectible (const dDNNFTreeDecompositionBuilder::suspicious_t &suspicious, const TreeDecomposition::Bag &b)
	Check whether all suspicious gates in suspicious appear in bag b.
std::ostream &	operator<< (std::ostream &o, const dDNNFTreeDecompositionBuilder::gates_to_or_t &gates_to_or)
	Write a gates_to_or_t DP table to an output stream for debugging.
std::ostream &	operator<< (std::ostream &o, const dDNNFTreeDecompositionBuilder::dDNNFGate &g)
	Debug output for a dDNNFTreeDecompositionBuilder::dDNNFGate.

Detailed Description

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

Implements the dDNNFTreeDecompositionBuilder::build() algorithm, which converts a bounded-treewidth Boolean circuit into a d-DNNF by following the construction in Section 5.1 of:

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. For each bag it maintains a set of dDNNFGate partial results, each carrying a valuation (truth-value assignment for the gates in the bag) and a suspicious set (gates not yet confirmed by their responsible bag).

Private helpers:

• builddDNNFLeaf(): generate partial results for a leaf bag.
• collectGatesToOr(): group partial results by (valuation, suspicious).
• builddDNNF(): main bottom-up recursion.
• isAlmostValuation(), getInnocent(): utilities for the DP.
• circuitHasWire(): O(log n) wire lookup using wiresSet.

Definition in file dDNNFTreeDecompositionBuilder.cpp.

Function Documentation

isConnectible()

bool isConnectible ( const dDNNFTreeDecompositionBuilder::suspicious_t & suspicious, const TreeDecomposition::Bag & b )

static

Check whether all suspicious gates in suspicious appear in bag b.

Parameters

suspicious	Set of gates that must be confirmed in the parent bag.
b	Bag to check against.

Returns

true if every gate in suspicious is in b.

Definition at line 127 of file dDNNFTreeDecompositionBuilder.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

isStrong()

bool isStrong ( BooleanGate type, bool value )

constexpr

Return true if assigning value to a gate of type type is a "strong" assignment.

A strong assignment is one that forces the gate's output to be determined by a single input (e.g., true for OR, false for AND).

Parameters

type	Gate type (AND, OR, IN, or other).
value	Truth value assigned to the gate.

Returns

true if the assignment is strong for this gate type.

Definition at line 107 of file dDNNFTreeDecompositionBuilder.cpp.

Here is the caller graph for this function:

operator<<() [1/2]

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 512 of file dDNNFTreeDecompositionBuilder.cpp.

operator<<() [2/2]

std::ostream & operator<<	(	std::ostream &	o,
		const dDNNFTreeDecompositionBuilder::gates_to_or_t &	gates_to_or )

Write a gates_to_or_t DP table to an output stream for debugging.

Parameters

o	Output stream.
gates_to_or	The DP table to display.

Returns

Reference to o.

Definition at line 261 of file dDNNFTreeDecompositionBuilder.cpp.