Boolean provenance circuit with support for knowledge compilation. More...

#include <unordered_map>
#include <unordered_set>
#include <set>
#include <map>
#include <vector>
#include <iosfwd>
#include <boost/archive/binary_oarchive.hpp>
#include <boost/serialization/unordered_map.hpp>
#include <boost/serialization/map.hpp>
#include <boost/serialization/set.hpp>
#include <boost/serialization/vector.hpp>
#include "Circuit.hpp"

Include dependency graph for BooleanCircuit.h:

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

Go to the source code of this file.

Classes
class	BooleanCircuit
	Boolean circuit for provenance formula evaluation. More...
struct	BooleanCircuit::CNFInputMapping
	One row of the Tseytin variable mapping. More...

Enumerations
enum class	BooleanGate { UNDETERMINED , AND , OR , NOT , IN , MULIN , MULVAR }
	Gate types for a Boolean provenance circuit. More...

Variables
constexpr unsigned	DNNF_CERT_INFO = 1
	d-DNNF certificate value for the (gate-type-specific) per-gate info field.

Detailed Description

Boolean provenance circuit with support for knowledge compilation.

BooleanCircuit represents the provenance formula of a query result as a Boolean circuit (AND/OR/NOT/IN gates). It supports multiple methods for computing the probability of the formula being true under tuple-independent probabilistic databases:

Method	Description
`possibleWorlds()`	Exact enumeration over all 2^n possible worlds
`compilation()`	Knowledge compilation to d-DNNF via an external tool
`monteCarlo()`	Monte Carlo sampling approximation
`WeightMC()`	Weighted model counting via weightmc
`independentEvaluation()`	Exact evaluation for disconnected circuits
`interpretAsDD()`	Direct tree-decomposition-based compilation
`makeDD()`	Generic d-DNNF construction dispatcher

Multivalued inputs (`MULIN` / `MULVAR`)

Multivalued input gates model tuples drawn from a discrete probability distribution. rewriteMultivaluedGates() rewrites them into standard AND/OR/NOT circuits before knowledge compilation.

The circuit is Boost-serialisable for transmission to external processes.

Definition in file BooleanCircuit.h.

Enumeration Type Documentation

◆ BooleanGate

enum class BooleanGate

strong

Gate types for a Boolean provenance circuit.

UNDETERMINED Placeholder for a gate whose type has not been set yet.
AND Logical conjunction of child gates.
OR Logical disjunction of child gates.
NOT Logical negation of a single child gate.
IN An input (variable) gate representing a base tuple.
MULIN A multivalued-input gate (one of several options).
MULVAR Auxiliary gate grouping all MULIN siblings.

Enumerator
UNDETERMINED	Placeholder gate whose type has not been set yet.
AND	Logical conjunction of child gates.
OR	Logical disjunction of child gates.
NOT	Logical negation of a single child gate.
IN	Input (variable) gate representing a base tuple.
MULIN	Multivalued-input gate (one of several options).
MULVAR	Auxiliary gate grouping all MULIN siblings.

Definition at line 56 of file BooleanCircuit.h.

Variable Documentation

◆ DNNF_CERT_INFO

unsigned DNNF_CERT_INFO = 1

constexpr

d-DNNF certificate value for the (gate-type-specific) per-gate info field.

On an OR (gate_plus) gate, info = DNNF_CERT_INFO asserts determinism: the children are mutually exclusive. On an AND (gate_times) gate it asserts decomposability: the children mention disjoint sets of variables. Both are semantic properties of the gate's (content-addressed) children, so a truthfully-set mark remains true however the gate is later re-derived. Set by constructions that establish the property structurally (the decomposition-aligned reachability compilation); trusted by independentEvaluation() and interpretAsDD(), the same trust model as the planner-asserted inversion-free certificate.

Definition at line 82 of file BooleanCircuit.h.

Classes

Enumerations