Boolean circuit for provenance formula evaluation. More...

#include "BooleanCircuit.h"

Inheritance diagram for BooleanCircuit:

[legend]

Collaboration diagram for BooleanCircuit:

Classes
struct	CNFInputMapping
	One row of the Tseytin variable mapping. More...

Public Member Functions
bool	isDNNFCertified (gate_t g) const
	Is gate `g` certified by the d-DNNF per-gate marking?
	BooleanCircuit ()
	Construct an empty Boolean circuit.
virtual	~BooleanCircuit ()
gate_t	addGate () override
	Allocate a new gate with a default-initialised type.
gate_t	setGate (BooleanGate type) override
	Allocate a new gate with type `type` and no UUID.
gate_t	setGate (const uuid &u, BooleanGate type) override
	Create or update the gate associated with UUID `u`.
gate_t	setGate (BooleanGate t, double p)
	Create a new gate with a probability annotation.
gate_t	setGate (const uuid &u, BooleanGate t, double p)
	Create (or update) a gate with a UUID and probability.
const std::set< gate_t > &	getInputs () const
	Return the set of input (IN) gate IDs.
bool	hasMultivaluedGates () const
	Return `true` if the circuit contains any MULIN gates.
void	setProb (gate_t g, double p)
	Set the probability for gate `g` and mark the circuit as probabilistic.
double	getProb (gate_t g) const
	Return the probability stored for gate `g`.
bool	isProbabilistic () const
	Return `true` if any gate has a non-trivial (< 1) probability.
void	setInfo (gate_t g, unsigned info)
	Store an integer annotation on gate `g`.
unsigned	getInfo (gate_t g) const
	Return the integer annotation for gate `g`.
double	possibleWorlds (gate_t g) const
	Compute the probability by exact enumeration of all possible worlds.
dDNNF	compilation (gate_t g, std::string compiler, std::string *resolved=nullptr) const
	Compile the sub-circuit rooted at `g` to a `dDNNF` via an external tool.
dDNNF	parseDDNNF (std::istream &in, const std::vector< gate_t > &inputOrder) const
	Parse a c2d/d4 NNF stream into a `dDNNF` over this circuit's input gates.
double	monteCarlo (gate_t g, unsigned samples) const
	Estimate the probability via Monte Carlo sampling.
bool	dnfShape (gate_t g, std::vector< gate_t > &clauses, std::vector< std::set< gate_t > > &supports) const
	Detect the DNF shape the Karp-Luby FPRAS requires.
bool	dnfShapeInfo (gate_t g, std::size_t &num_clauses) const
	Cheap shape test: is the circuit DNF-shaped, and how many clauses?
double	karpLuby (const std::vector< gate_t > &clauses, const std::vector< std::set< gate_t > > &supports, unsigned long samples) const
	Karp-Luby FPRAS estimate of a DNF-shaped circuit's probability (fixed sample budget, stratified).
double	sieve (const std::vector< gate_t > &clauses, const std::vector< std::set< gate_t > > &supports) const
	Exact probability of a monotone DNF by inclusion-exclusion (sieve).
void	dnfBounds (const std::vector< std::set< gate_t > > &clauses, double &lower, double &upper) const
	Cheap certified probability interval [lower,upper] of a monotone DNF, without compiling it (Olteanu-Huang-Koch d-tree leaf bound).
double	karpLubyStopping (const std::vector< gate_t > &clauses, const std::vector< std::set< gate_t > > &supports, double eps, double delta, unsigned long max_samples, unsigned long &samples_used, bool &reached_target) const
	Karp-Luby FPRAS with the self-adjusting stopping rule (adaptive sample count for a relative (eps,delta) guarantee).
double	wmcCount (gate_t g, const std::string &tool, const std::string &opt) const
	Weighted model counting through a registered external counter.
double	independentEvaluation (gate_t g) const
	Compute the probability exactly when inputs are independent.
void	rewriteMultivaluedGates ()
	Rewrite all MULVAR/MULIN gate clusters into standard AND/OR/NOT circuits.
dDNNF	interpretAsDD (gate_t g) const
	Build a `dDNNF` directly from the Boolean circuit's structure.
dDNNF	makeDD (gate_t g, const std::string &method, const std::string &args) const
	Dispatch to the appropriate d-DNNF construction method.
dDNNF	makeDDByName (gate_t g, const std::string &name) const
	Build a `dDNNF` from a single compiler/route name.
virtual std::string	toString (gate_t g) const override
	Return a textual description of gate `g` for debugging.
std::string	toString (gate_t g, const std::unordered_map< gate_t, std::string > &labels) const
	Render the sub-circuit at `g`, labelling input gates from a map.
std::string	exportCircuit (gate_t g) const
	Export the circuit in the textual format expected by external compilers.
std::string	TseytinCNF (gate_t g, bool display_prob, bool mapping=false) const
	Return the Tseytin transformation of the sub-circuit at `g` as a DIMACS string.
std::vector< CNFInputMapping >	tseytinVariableMapping () const
	Map each input gate to its DIMACS variable, UUID, probability.
std::string	BCS12 (gate_t g, std::vector< gate_t > &inputOrder) const
	Serialise the sub-circuit at `g` in d4's BC-S1.2 circuit format.
dDNNF	parsePaniniDD (const std::string &outfilename) const
	Parse a Panini (KCBox) DD output file into a ProvSQL d-DNNF.
template<class Archive>
void	serialize (Archive &ar, const unsigned int version)
	Boost serialisation support.
Public Member Functions inherited from Circuit< BooleanGate >
virtual	~Circuit ()
std::vector< gate_t >::size_type	getNbGates () const
	Return the total number of gates in the circuit.
gate_t	getGate (const uuid &u)
	Return (or create) the gate associated with UUID `u`.
uuid	getUUID (gate_t g) const
	Return the UUID string associated with gate `g`.
BooleanGate	getGateType (gate_t g) const
	Return the type of gate `g`.
std::vector< gate_t > &	getWires (gate_t g)
	Return a mutable reference to the child-wire list of gate `g`.
virtual gate_t	setGate (const uuid &u, BooleanGate type)
	Create or update the gate associated with UUID `u`.
bool	hasGate (const uuid &u) const
	Test whether a gate with UUID `u` exists.
void	addWire (gate_t f, gate_t t)
	Add a directed wire from gate `f` (parent) to gate `t` (child).

Protected Attributes
std::set< gate_t >	inputs
	Set of IN (input) gate IDs.
std::set< gate_t >	mulinputs
	Set of MULVAR gate IDs.
std::vector< double >	prob
	Per-gate probability (for IN gates).
std::map< gate_t, unsigned >	info
	Per-gate integer info (for MULIN gates).
bool	probabilistic =false
	`true` if any gate has a non-unit probability
Protected Attributes inherited from Circuit< BooleanGate >
std::unordered_map< uuid, gate_t >	uuid2id
	UUID string → gate index.
std::unordered_map< gate_t, uuid >	id2uuid
	Gate index → UUID string.
std::vector< BooleanGate >	gates
	Gate type for each gate.
std::vector< std::vector< gate_t > >	wires
	Child wire lists for each gate.

Private Member Functions
bool	evaluate (gate_t g, const std::unordered_set< gate_t > &sampled) const
	Evaluate the sub-circuit at `g` on one sampled world.
gate_t	interpretAsDDInternal (gate_t g, std::set< gate_t > &seen, dDNNF &dd) const
	Recursive helper for `interpretAsDD()`.
gate_t	interpretCertifiedIsland (gate_t root, std::set< gate_t > &seen, dDNNF &dd) const
	Iteratively copy a certified island into `dd`.
double	independentEvaluationInternal (gate_t g, std::set< gate_t > &seen, std::unordered_map< gate_t, double > &memo) const
	Recursive helper for `independentEvaluation()`.
double	evaluateCertifiedIsland (gate_t root, std::set< gate_t > &seen, std::unordered_map< gate_t, double > &memo) const
	Iteratively evaluate a certified d-DNNF island.
void	rewriteMultivaluedGatesRec (const std::vector< gate_t > &muls, const std::vector< double > &cumulated_probs, unsigned start, unsigned end, std::vector< gate_t > &prefix)
	Recursive helper for `rewriteMultivaluedGates()`.
std::string	toStringHelper (gate_t g, BooleanGate parent, const std::unordered_map< gate_t, std::string > *labels) const
	Internal recursive helper for the two `toString()` variants.

Friends
class	dDNNFTreeDecompositionBuilder
class	boost::serialization::access

Additional Inherited Members
Public Types inherited from Circuit< BooleanGate >
using	uuid
	UUID type used in this circuit (always `std::string`).
Protected Member Functions inherited from Circuit< BooleanGate >
void	setGateType (gate_t g, BooleanGate t)
	Update the type of an existing gate.

Detailed Description

Boolean circuit for provenance formula evaluation.

Inherits the gate/wire infrastructure from Circuit<BooleanGate> and adds probability annotation, info integers (for multivalued inputs), and a rich set of evaluation algorithms.

Definition at line 91 of file BooleanCircuit.h.

Constructor & Destructor Documentation

◆ BooleanCircuit()

BooleanCircuit::BooleanCircuit ( )

inline

Construct an empty Boolean circuit.

Definition at line 225 of file BooleanCircuit.h.

◆ ~BooleanCircuit()

virtual BooleanCircuit::~BooleanCircuit ( )

inlinevirtual

Definition at line 227 of file BooleanCircuit.h.

Member Function Documentation

◆ addGate()

gate_t BooleanCircuit::addGate ( )

overridevirtual

Allocate a new gate with a default-initialised type.

Derived classes override this to perform additional initialisation (e.g. resizing auxiliary vectors).

Returns: The gate_t identifier of the newly created gate.

Reimplemented from Circuit< BooleanGate >.

Definition at line 175 of file BooleanCircuit.cpp.

Here is the call graph for this function:

◆ BCS12()

std::string BooleanCircuit::BCS12	(	gate_t	g,
		std::vector< gate_t > &	inputOrder ) const

Serialise the sub-circuit at g in d4's BC-S1.2 circuit format.

Emits the Boolean circuit directly (inputs as "I" declarations, AND/OR gates as "G name := A|O …" definitions, the root as "T"), inlining NOT gates as literal sign flips. This is the input consumed by d4v2's --input-type circuit mode, letting us skip the Tseytin transform.

Inputs are emitted first, so d4 (which numbers literals from 1 in first-seen order) assigns them variables 1..k in declaration order; every variable above k is an internal-gate variable. inputOrder is filled so that d4 variable v (1-based) corresponds to input gate inputOrder[v-1], which the d-DNNF parse-back uses to map decision literals to the right IN gate.

Throws CircuitException on a gate shape BC-S1.2 cannot express (a nullary AND/OR, or a non-AND/OR/NOT/IN gate); the caller falls back to the Tseytin CNF path.

Parameters

g	Root gate of the sub-circuit.
inputOrder	Output: input gate for each d4 variable (1-based).

Returns: BC-S1.2 circuit description as a string.

Definition at line 955 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ compilation()

dDNNF BooleanCircuit::compilation	(	gate_t	g,
		std::string	compiler,
		std::string *	resolved = nullptr ) const

Compile the sub-circuit rooted at g to a dDNNF via an external tool.

Writes the circuit in DIMACS/DNNF format, invokes compiler as a subprocess, and parses the resulting d-DNNF.

Parameters

g	Root gate.
compiler	Command to invoke (e.g. "d4", "c2d", "minic2d"). Empty auto-selects the highest-preference available tool.
resolved	If non-null, set to the tool actually used (after the empty -> auto-select resolution), so callers can report WHICH compiler ran rather than just "compilation".

Returns: The compiled dDNNF.

Definition at line 1222 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ dnfBounds()

void BooleanCircuit::dnfBounds	(	const std::vector< std::set< gate_t > > &	clauses,
		double &	lower,
		double &	upper ) const

Cheap certified probability interval [lower,upper] of a monotone DNF, without compiling it (Olteanu-Huang-Koch d-tree leaf bound).

Implements the Independent heuristic of Olteanu, Huang & Koch, "Approximate Confidence Computation in Probabilistic Databases" (ICDE 2010, Fig. 3). The clauses are greedily partitioned into buckets of pairwise independent clauses (disjoint supports), clauses taken in descending marginal-probability order so the most probable clauses anchor the buckets. Each bucket's clauses are mutually independent, so its probability is the independent-or 1-∏(1-P(d)) with P(d)=∏_{leaf∈supports[d]} getProb(leaf). Then, since Φ is the disjunction of all buckets:

lower = max_i P(B_i): a sub-disjunction is a lower bound;
upper = min(1, Σ_i P(B_i)): the union bound.

Both bounds are sound for any partition (the greedy one only affects tightness), so lower ≤ Pr[Φ] ≤ upper always holds. When the clauses are mutually independent (disjoint supports) they all land in a single bucket and lower=upper=Pr[Φ], i.e. the interval collapses to the exact value. O(m^2) in the clause count m.

A monotone DNF is fully determined (for probability) by its per-clause input supports, so this takes only the supports (the set per clause returned by dnfShape, or a cofactor's residual clause set in the DTree engine); the clause root gates are not needed.

Parameters

clauses	Per-clause input-leaf supports (a monotone DNF as a set of clauses, each a set of `IN` leaves).
lower	[out] Certified lower bound on `Pr`[Φ].
upper	[out] Certified upper bound on `Pr`[Φ].

Definition at line 754 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ dnfShape()

bool BooleanCircuit::dnfShape	(	gate_t	g,
		std::vector< gate_t > &	clauses,
		std::vector< std::set< gate_t > > &	supports ) const

Detect the DNF shape the Karp-Luby FPRAS requires.

Recognises the two tractable regimes: (a) a single AND-of-leaves clause, or (b) a top-level OR whose every child is an AND-only sub-circuit over IN leaves (no OR below the root, no NOT, no multivalued input). Cross-clause leaf sharing is allowed and is the normal Karp-Luby setting.

On success, clauses receives one root per top-level disjunct (or the singleton root g in regime (a)) and supports[i] the set of IN leaves reachable from clauses[i] through its AND-only stratum – the support determines Pr[C_i] (the product of leaf marginals) and the conditional sampler.

Parameters

g	Root gate.
clauses	Output: the top-level clause roots.
supports	Output: per-clause set of reachable `IN` leaves.

Returns: true iff the circuit is DNF-shaped (regime (a)/(b)).

Definition at line 394 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ dnfShapeInfo()

bool BooleanCircuit::dnfShapeInfo	(	gate_t	g,
		std::size_t &	num_clauses ) const

Cheap shape test: is the circuit DNF-shaped, and how many clauses?

The O(circuit) half of dnfShape – validates the OR-of-ANDs-of-leaves shape with a single global visited-set (no per-clause re-walk) and returns the clause count, WITHOUT materialising the per-clause supports (whose total size can be O(m*N)). Used by the chooser to rank sieve; the supports are built only if sieve / karp-luby actually runs (via dnfShape).

Parameters

g	Root gate.
num_clauses	Output: number of top-level clauses.

Returns: true iff DNF-shaped.

Definition at line 446 of file BooleanCircuit.cpp.

Here is the call graph for this function:

◆ evaluate()

bool BooleanCircuit::evaluate	(	gate_t	g,
		const std::unordered_set< gate_t > &	sampled ) const

private

Evaluate the sub-circuit at g on one sampled world.

Each gate in sampled is treated as true; all other IN gates are false.

Parameters

g	Root gate to evaluate.
sampled	Set of input gates that are `true` in this world.

Returns: Boolean value of the circuit at gate g.

Definition at line 322 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ evaluateCertifiedIsland()

double BooleanCircuit::evaluateCertifiedIsland	(	gate_t	root,
		std::set< gate_t > &	seen,
		std::unordered_map< gate_t, double > &	memo ) const

private

Iteratively evaluate a certified d-DNNF island.

Walks the maximal region of certified AND/OR gates (plus the NOT and input gates they reach) under root with an explicit post-order stack – certified circuits can be as deep as the data (e.g. the decomposition-aligned reachability circuits of path-like graphs), so recursion would overflow the stack. Within the island every gate is computed once (sharing is licensed by the certificate): certified OR = sum (determinism), certified AND = product (decomposability), and each variable registers once in seen, so entanglement with the outside – or with another island – throws like a read-once violation. An uncertified AND/OR inside the island falls back to independentEvaluationInternal() (standard read-once rules).

Parameters

root	Certified gate the island is rooted at.
seen	Global variable registration shared with the uncertified region.
memo	Constant-only global memo (used by the uncertified fallback).

Returns: Probability at root.

Definition at line 1800 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ exportCircuit()

std::string BooleanCircuit::exportCircuit ( gate_t g ) const

Export the circuit in the textual format expected by external compilers.

Produces a multi-line string encoding all gates reachable from the circuit in the format used by the standalone tdkc tool and external model counters.

Parameters

g	Root gate.

Returns: Circuit description string.

Definition at line 263 of file BooleanCircuit.cpp.

Here is the call graph for this function:

◆ getInfo()

unsigned BooleanCircuit::getInfo ( gate_t g ) const

Return the integer annotation for gate g.

Parameters

g	Gate identifier.

Returns: Stored integer, or 0 if not set.

Definition at line 1903 of file BooleanCircuit.cpp.

Here is the caller graph for this function:

◆ getInputs()

const std::set< gate_t > & BooleanCircuit::getInputs ( ) const

inline

Return the set of input (IN) gate IDs.

Returns: Const reference to the set of IN gate identifiers.

Definition at line 258 of file BooleanCircuit.h.

Here is the caller graph for this function:

◆ getProb()

double BooleanCircuit::getProb ( gate_t g ) const

inline

Return the probability stored for gate g.

Parameters

g	Gate identifier.

Returns: Probability value.

Definition at line 292 of file BooleanCircuit.h.

Here is the caller graph for this function:

◆ hasMultivaluedGates()

bool BooleanCircuit::hasMultivaluedGates ( ) const

inline

Return true if the circuit contains any MULIN gates.

Multivalued inputs are normally rewritten into AND/OR/NOT/IN gates by rewriteMultivaluedGates() before the circuit is consumed by an evaluation method. Algorithms that cannot handle multivalued inputs directly can use this as a precondition check.

Returns: true iff at least one MULIN gate is present.

Definition at line 272 of file BooleanCircuit.h.

Here is the caller graph for this function:

◆ independentEvaluation()

double BooleanCircuit::independentEvaluation ( gate_t g ) const

Compute the probability exactly when inputs are independent.

Applicable when the circuit has no shared input gate (i.e., each input appears at most once).

Parameters

g	Root gate.

Returns: Exact probability.

Definition at line 1891 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ independentEvaluationInternal()

double BooleanCircuit::independentEvaluationInternal	(	gate_t	g,
		std::set< gate_t > &	seen,
		std::unordered_map< gate_t, double > &	memo ) const

private

Recursive helper for independentEvaluation().

A certified (d-DNNF-marked) gate is handed to evaluateCertifiedIsland(); the recursion only walks the uncertified region.

Parameters

g	Current gate to evaluate.
seen	Set of variable gates (IN / MULVAR) already consumed; a second occurrence means the circuit is not read-once.
memo	Memoised probability of variable-free (constant-only) gates, so a shared constant subgraph is evaluated once – this is what keeps the whole evaluation `O(circuit)` rather than re-traversing shared subgraphs. Variable-bearing gates are never memoised (a re-visit must reach `seen` and throw).

Returns: Probability at gate g.

Definition at line 1683 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ interpretAsDD()

dDNNF BooleanCircuit::interpretAsDD ( gate_t g ) const

Build a dDNNF directly from the Boolean circuit's structure.

Used as a fallback when no external compiler is available and the circuit is already in a form that can be interpreted as a d-DNNF.

Parameters

g	Root gate.

Returns: A dDNNF wrapping the same structure.

Definition at line 2118 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ interpretAsDDInternal()

gate_t BooleanCircuit::interpretAsDDInternal	(	gate_t	g,
		std::set< gate_t > &	seen,
		dDNNF &	dd ) const

private

Recursive helper for interpretAsDD().

A certified (d-DNNF-marked) gate is handed to interpretCertifiedIsland(); the recursion only walks the uncertified region.

Parameters

g	Current gate to process.
seen	Set of variable gates already consumed (read-once check in the uncertified region; per-island registration inside certified islands).
dd	The d-DNNF being constructed.

Returns: Gate ID in dd corresponding to g.

Definition at line 1991 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ interpretCertifiedIsland()

gate_t BooleanCircuit::interpretCertifiedIsland	(	gate_t	root,
		std::set< gate_t > &	seen,
		dDNNF &	dd ) const

private

Iteratively copy a certified island into dd.

Island twin of evaluateCertifiedIsland() (same discipline, same iterative post-order): certified ORs are copied as native deterministic ORs (no De Morgan rewriting), certified ANDs as-is, shared sub-DAGs map to shared dd gates. An uncertified AND/OR inside the island falls back to interpretAsDDInternal().

Parameters

root	Certified gate the island is rooted at.
seen	Global variable registration (see `evaluateCertifiedIsland()`).
dd	The d-DNNF being constructed.

Returns: Gate ID in dd corresponding to root.

Definition at line 2054 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ isDNNFCertified()

bool BooleanCircuit::isDNNFCertified ( gate_t g ) const

inline

Is gate g certified by the d-DNNF per-gate marking?

true iff g is an OR marked deterministic or an AND marked decomposable (info = DNNF_CERT_INFO); see DNNF_CERT_INFO for the semantics and trust model.

Parameters

g	Gate to test.

Returns: Whether the gate carries the d-DNNF certificate.

Definition at line 194 of file BooleanCircuit.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ isProbabilistic()

bool BooleanCircuit::isProbabilistic ( ) const

inline

Return true if any gate has a non-trivial (< 1) probability.

Returns: true iff at least one gate has a probability strictly less than 1.

Definition at line 300 of file BooleanCircuit.h.

Here is the caller graph for this function:

◆ karpLuby()

double BooleanCircuit::karpLuby	(	const std::vector< gate_t > &	clauses,
		const std::vector< std::set< gate_t > > &	supports,
		unsigned long	samples ) const

Karp-Luby FPRAS estimate of a DNF-shaped circuit's probability (fixed sample budget, stratified).

Implements the Karp-Luby coverage estimator for the DNF-counting problem (#DNF) under tuple-independent inputs: with p_i the product of the marginals of supports[i] and S the sum of the p_i (so S in [Pr[F], m*Pr[F]]), the estimator over clause i samples a satisfying assignment of C_i (its support forced true, every other leaf drawn from its marginal), finds the smallest clause index j the assignment satisfies, and accepts iff j == i; Pr[F] is then sum_i p_i times the per-clause acceptance rate. The acceptance probability is Pr[F]/S in [1/m, 1], so the sample count for an (eps,delta) guarantee is independent of Pr[F], unlike naive Monte Carlo.

The samples rounds are spread across clauses by stratified allocation (n_i proportional to p_i/S, every clause sampled at least once), estimating each clause's acceptance rate separately and combining sum_i p_i * acceptRate_i. This removes the variance of the categorical clause draw used by the textbook estimator (between-strata variance), tightening the estimate at the same budget by up to a factor m. When samples < m there are too few rounds for one per clause, so the method falls back to the unstratified categorical-draw estimator (still unbiased for any budget).

The clauses / supports are those returned by dnfShape. The mt19937_64 is seeded from provsql.monte_carlo_seed exactly as monteCarlo, so the estimate is reproducible under a pinned seed.

Parameters

clauses	Top-level clause roots (from `dnfShape`).
supports	Per-clause reachable `IN` leaves (from `dnfShape`).
samples	Resolved number of sampling rounds.

Returns: The Karp-Luby probability estimate.

Definition at line 585 of file BooleanCircuit.cpp.

◆ karpLubyStopping()

double BooleanCircuit::karpLubyStopping	(	const std::vector< gate_t > &	clauses,
		const std::vector< std::set< gate_t > > &	supports,
		double	eps,
		double	delta,
		unsigned long	max_samples,
		unsigned long &	samples_used,
		bool &	reached_target ) const

Karp-Luby FPRAS with the self-adjusting stopping rule (adaptive sample count for a relative (eps,delta) guarantee).

The Dagum-Karp-Luby-Ross stopping rule (SICOMP 2000, the optimal form of the Karp-Luby-Madras 1989 self-adjusting rule): rather than fixing the number of rounds from the worst-case acceptance probability 1/m, draw coverage trials (clause i with probability p_i/S, then the smallest-index coverage test of karpLuby) until the accept count reaches the deterministic threshold Y1 = 1 + (1+eps) * 4*(e-2)*ln(2/delta)/eps^2, then return S * Y1 / N over the N rounds actually run. That estimate is a relative (eps,delta) approximation of Pr[F], and N adapts to the true acceptance probability Pr[F]/S (expected N is Y1*S/Pr[F], i.e. up to m times fewer rounds than the fixed bound when the clauses barely overlap).

Sampling stops early at max_samples rounds; reached_target is then false and the return is the plain unbiased S*accepts/N estimate over the spent budget (the (eps,delta) target was not met – the caller reports the weaker guarantee actually achieved).

Parameters

clauses	Top-level clause roots (from `dnfShape`).
supports	Per-clause reachable `IN` leaves (from `dnfShape`).
eps	Target relative error (in (0,1]).
delta	Target failure probability (in (0,1)).
max_samples	Hard cap on the number of rounds.
samples_used	Output: rounds actually run.
reached_target	Output: whether the stopping threshold was reached before `max_samples` (i.e. the guarantee holds).

Returns: The Karp-Luby probability estimate.

Definition at line 661 of file BooleanCircuit.cpp.

◆ makeDD()

dDNNF BooleanCircuit::makeDD	(	gate_t	g,
		const std::string &	method,
		const std::string &	args ) const

Dispatch to the appropriate d-DNNF construction method.

Parameters

g	Root gate.
method	Compilation method name (e.g. "tree-decomposition", "d4", "c2d"…).
args	Additional arguments forwarded to the chosen method.

Returns: The constructed dDNNF.

Definition at line 2137 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ makeDDByName()

dDNNF BooleanCircuit::makeDDByName	(	gate_t	g,
		const std::string &	name ) const

Build a dDNNF from a single compiler/route name.

Resolves the name the way a user (or Studio) thinks of it, with no separate method / args split:

the in-process meta-routes "tree-decomposition", "interpret-as-dd", "default" (and the empty string) go through makeDD;
any other name is an external compiler ("d4", "d4v2", "c2d", "minic2d", "dsharp", "panini-*") and is passed straight to compilation.

This is the single dispatch point shared by compile_to_ddnnf_dot, compile_to_ddnnf (NNF) and ddnnf_stats, so they cannot drift on which names they accept.

Parameters

g	Root gate.
name	Compiler or meta-route name.

Returns: The constructed dDNNF.

Definition at line 2180 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ monteCarlo()

double BooleanCircuit::monteCarlo	(	gate_t	g,
		unsigned	samples ) const

Estimate the probability via Monte Carlo sampling.

Parameters

g	Root gate.
samples	Number of independent worlds to sample.

Returns: Estimated probability.

Definition at line 359 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ parseDDNNF()

dDNNF BooleanCircuit::parseDDNNF	(	std::istream &	in,
		const std::vector< gate_t > &	inputOrder ) const

Parse a c2d/d4 NNF stream into a dDNNF over this circuit's input gates.

Shared by the CLI compilation() path and the KCMCP client: both obtain the same NNF text (from a temp file or a socket RESULT) and parse it identically. inputOrder maps d4 circuit-mode variables (1..k) to IN gates; an empty vector means CNF mode, where d-DNNF variable v stands for gate id v-1 (real only for IN gates, every other being a Tseytin auxiliary that is projected out).

Parameters

in	NNF text stream.
inputOrder	Circuit-mode input-variable to IN-gate map (empty = CNF).

Returns: The compiled dDNNF (empty if the formula is unsat).

Definition at line 1386 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ parsePaniniDD()

dDNNF BooleanCircuit::parsePaniniDD ( const std::string & outfilename ) const

Parse a Panini (KCBox) DD output file into a ProvSQL d-DNNF.

The panini-dd output parser, selected by compilation() for the panini-* records. Those records run the generic compile path (a Tseytin CNF written to the input, the record's argtpl run, the --lang carried in the template); they differ from the nnf compilers only in this parse-back. Panini's DD output is over the variables of our Tseytin CNF: decisions on input variables are translated to the corresponding IN gates; decisions on Tseytin auxiliaries are dropped (their branches are mutually exclusive over input assignments by Tseytin determinism, so the input-projection is still a sound d-DNNF). "R2-D2" / "CCDD" emit K (kernelize) nodes that break decomposability, so those variants are not registered and a K node here is an error.

Parameters

outfilename Path to Panini's DD output file.

Returns: The compiled d-DNNF.

Definition at line 1047 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ possibleWorlds()

double BooleanCircuit::possibleWorlds ( gate_t g ) const

Compute the probability by exact enumeration of all possible worlds.

Only tractable for circuits with a small number of input gates.

Parameters

g	Root gate.

Returns: Exact probability.

Definition at line 829 of file BooleanCircuit.cpp.

Here is the call graph for this function:

◆ rewriteMultivaluedGates()

void BooleanCircuit::rewriteMultivaluedGates ( )

Rewrite all MULVAR/MULIN gate clusters into standard AND/OR/NOT circuits.

Must be called before any evaluation method when the circuit contains multivalued input gates.

Definition at line 1961 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ rewriteMultivaluedGatesRec()

void BooleanCircuit::rewriteMultivaluedGatesRec	(	const std::vector< gate_t > &	muls,
		const std::vector< double > &	cumulated_probs,
		unsigned	start,
		unsigned	end,
		std::vector< gate_t > &	prefix )

private

Recursive helper for rewriteMultivaluedGates().

Parameters

muls	Gates in the MULVAR group being rewritten.
cumulated_probs	Cumulative probability thresholds for each MULIN.
start	First index in `muls` to process.
end	One past the last index in `muls` to process.
prefix	Current AND-chain prefix being built.

Definition at line 1913 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ serialize()

template<class Archive>

void BooleanCircuit::serialize	(	Archive &	ar,
		const unsigned int	version )

inline

Boost serialisation support.

Parameters

ar	Boost archive (input or output).
version	Archive version (unused).

Definition at line 781 of file BooleanCircuit.h.

◆ setGate() [1/4]

gate_t BooleanCircuit::setGate	(	BooleanGate	t,
		double	p )

Create a new gate with a probability annotation.

Parameters

t	Gate type (typically `BooleanGate::IN`).
p	Probability of this gate being `true`.

Returns: Gate identifier.

Definition at line 166 of file BooleanCircuit.cpp.

Here is the call graph for this function:

◆ setGate() [2/4]

gate_t BooleanCircuit::setGate ( BooleanGate type )

override

Allocate a new gate with type type and no UUID.

Parameters

type	Gate type.

Returns: Gate identifier.

Definition at line 133 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ setGate() [3/4]

gate_t BooleanCircuit::setGate	(	const uuid &	u,
		BooleanGate	t,
		double	p )

Create (or update) a gate with a UUID and probability.

Parameters

u	UUID string.
t	Gate type.
p	Probability of this gate being `true`.

Returns: Gate identifier.

Definition at line 157 of file BooleanCircuit.cpp.

Here is the call graph for this function:

◆ setGate() [4/4]

gate_t BooleanCircuit::setGate	(	const uuid &	u,
		BooleanGate	type )

override

Create or update the gate associated with UUID u.

If the UUID is already mapped the existing gate's type is updated. Otherwise a new gate is allocated.

Parameters

u	UUID string to associate with the gate.
type	Gate type.

Returns: Gate identifier.

Definition at line 145 of file BooleanCircuit.cpp.

Here is the call graph for this function:

◆ setInfo()

void BooleanCircuit::setInfo	(	gate_t	g,
		unsigned	info )

Store an integer annotation on gate g.

Used to record the index of a MULIN gate within its MULVAR group.

Parameters

g	Gate identifier.
info	Integer to store.

Definition at line 1898 of file BooleanCircuit.cpp.

Here is the caller graph for this function:

◆ setProb()

void BooleanCircuit::setProb	(	gate_t	g,
		double	p )

inline

Set the probability for gate g and mark the circuit as probabilistic.

Parameters

g	Gate identifier.
p	Probability value in [0, 1].

Definition at line 281 of file BooleanCircuit.h.

Here is the caller graph for this function:

◆ sieve()

double BooleanCircuit::sieve	(	const std::vector< gate_t > &	clauses,
		const std::vector< std::set< gate_t > > &	supports ) const

Exact probability of a monotone DNF by inclusion-exclusion (sieve).

Pr[∨_i c_i] = Σ_{∅≠S⊆clauses} (-1)^{|S|+1} Pr[∧_{i∈S} c_i]. Each clause is a conjunction of positive input leaves, so the conjunction of a set S of clauses is the AND of the union of their supports, and over independent inputs Pr[∧_{i∈S} c_i] = ∏_{leaf ∈ ∪supports(S)} getProb(leaf). Exact, and O(2^m) in the clause count m – the portfolio member to pick when m is small (a handful of clauses), where it beats the general compilers.

clauses / supports are those returned by dnfShape (monotone DNF over input leaves). Throws when m exceeds kSieveMaxClauses (the 2^m enumeration would be impractical) so the caller can pick another method.

Parameters

clauses	Top-level clause roots (from `dnfShape`).
supports	Per-clause reachable `IN` leaves (from `dnfShape`).

Returns: The exact probability.

Definition at line 718 of file BooleanCircuit.cpp.

Here is the call graph for this function:

◆ toString() [1/2]

std::string BooleanCircuit::toString ( gate_t g ) const

overridevirtual

Return a textual description of gate g for debugging.

Pure virtual; each concrete circuit class provides its own formatting.

Parameters

g	Gate to describe.

Returns: Human-readable string.

Implements Circuit< BooleanGate >.

Definition at line 182 of file BooleanCircuit.cpp.

Here is the call graph for this function:

◆ toString() [2/2]

std::string BooleanCircuit::toString	(	gate_t	g,
		const std::unordered_map< gate_t, std::string > &	labels ) const

Render the sub-circuit at g, labelling input gates from a map.

Same as toString(gate_t), but IN and MULIN gates whose gate identifier is present in labels are rendered using the mapped string instead of the default x<id> placeholder. Gates not found in labels fall back to the default rendering.

Parameters

g	Gate to render.
labels	Optional mapping from input/mulinput gate IDs to user-supplied labels.

Returns: Human-readable string.

Definition at line 187 of file BooleanCircuit.cpp.

Here is the call graph for this function:

◆ toStringHelper()

std::string BooleanCircuit::toStringHelper	(	gate_t	g,
		BooleanGate	parent,
		const std::unordered_map< gate_t, std::string > *	labels ) const

private

Internal recursive helper for the two toString() variants.

The parent parameter carries the gate type of the immediate caller. It drives parenthesis elision in two cases: at the root (parent set to UNDETERMINED) the outer wrap is omitted, and when parent matches the current gate type (associative AND/OR) the wrap is omitted to flatten same-op nesting. A 1-wire AND/OR also bypasses the wrap and delegates to its child since such single-element joins carry no information.

Parameters

g	Gate to render.
parent	Gate type of the caller, or `UNDETERMINED` at the root.
labels	Pointer to a label map, or `nullptr` for the unlabelled rendering.

Definition at line 194 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ TseytinCNF()

std::string BooleanCircuit::TseytinCNF	(	gate_t	g,
		bool	display_prob,
		bool	mapping = false ) const

Return the Tseytin transformation of the sub-circuit at g as a DIMACS string.

Same encoding as the private Tseytin file-emitting overload, but returned in memory without any file I/O. Useful for surfacing the CNF to a user or to a knowledge-compilation tool over stdin.

Parameters

g	Root gate.
display_prob	Include `w` lines listing each input's probability (and its complement).
mapping	Prepend `"c input <var> <uuid> <prob>"` comment lines, one per input gate, so the emitted DIMACS is self-documenting (the comments are ignored by every model counter / compiler).

Returns: DIMACS CNF as a string.

Definition at line 862 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ tseytinVariableMapping()

std::vector< BooleanCircuit::CNFInputMapping > BooleanCircuit::tseytinVariableMapping ( ) const

Map each input gate to its DIMACS variable, UUID, probability.

The variable numbering matches TseytinCNF (and dDNNF::toNNF): variable = gate id + 1. Inputs are listed in gate-id order so the mapping is deterministic.

Returns: One CNFInputMapping per input gate.

Definition at line 940 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ wmcCount()

double BooleanCircuit::wmcCount	(	gate_t	g,
		const std::string &	tool,
		const std::string &	opt ) const

Weighted model counting through a registered external counter.

Generic over the counter: tool names a registry record with the "wmc" operation (today weightmc, ganak, sharpsat-td, dpmc, or any tool an administrator registers). The record's binary, dependencies, argtpl and parser drive the whole call – which weighted-CNF dialect to write, the command to run, and how to read the count back – so there is no per-counter code path. Two output/input conventions are understood, by parser: "wmc-line" (MCC-2024 weighted DIMACS in, a "c s exact" / "s wmc" count line out) and "weightmc" (weightmc's own dialect in, a "mantissa x 2^exp" line out).

Parameters

g	Root gate of the sub-circuit.
tool	Logical name of the wmc tool to use.
opt	Tool options; for the approximate counters of the form `"delta;epsilon"` (drives the `{pivotAC}` placeholder).

Returns: The weighted model count = P(formula).

Definition at line 1566 of file BooleanCircuit.cpp.

Here is the call graph for this function:

◆ boost::serialization::access

friend class boost::serialization::access

friend

Definition at line 795 of file BooleanCircuit.h.

◆ dDNNFTreeDecompositionBuilder

friend class dDNNFTreeDecompositionBuilder

friend

Definition at line 794 of file BooleanCircuit.h.

Member Data Documentation

◆ info

std::map<gate_t, unsigned> BooleanCircuit::info

protected

Per-gate integer info (for MULIN gates).

Definition at line 220 of file BooleanCircuit.h.

◆ inputs

std::set<gate_t> BooleanCircuit::inputs

protected

Set of IN (input) gate IDs.

Definition at line 217 of file BooleanCircuit.h.

◆ mulinputs

std::set<gate_t> BooleanCircuit::mulinputs

protected

Set of MULVAR gate IDs.

Definition at line 218 of file BooleanCircuit.h.

◆ prob

std::vector<double> BooleanCircuit::prob

protected

Per-gate probability (for IN gates).

Definition at line 219 of file BooleanCircuit.h.

◆ probabilistic

bool BooleanCircuit::probabilistic =false

protected

true if any gate has a non-unit probability

Definition at line 221 of file BooleanCircuit.h.

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

/home/senellar/git/software/provsql/src/BooleanCircuit.h
/home/senellar/git/software/provsql/src/BooleanCircuit.cpp

Classes

Public Member Functions

Protected Attributes

Private Member Functions

Friends

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ BooleanCircuit()

◆ ~BooleanCircuit()

Member Function Documentation

◆ addGate()

◆ BCS12()

◆ compilation()

◆ dnfBounds()

◆ dnfShape()

◆ dnfShapeInfo()

◆ evaluate()

◆ evaluateCertifiedIsland()

◆ exportCircuit()

◆ getInfo()

◆ getInputs()

◆ getProb()

◆ hasMultivaluedGates()

◆ independentEvaluation()

◆ independentEvaluationInternal()

◆ interpretAsDD()

◆ interpretAsDDInternal()

◆ interpretCertifiedIsland()

◆ isDNNFCertified()

◆ isProbabilistic()

◆ karpLuby()

◆ karpLubyStopping()

◆ makeDD()

◆ makeDDByName()

◆ monteCarlo()

◆ parseDDNNF()

◆ parsePaniniDD()

◆ possibleWorlds()

◆ rewriteMultivaluedGates()

◆ rewriteMultivaluedGatesRec()

◆ serialize()

◆ setGate() [1/4]

◆ setGate() [2/4]

◆ setGate() [3/4]

◆ setGate() [4/4]

◆ setInfo()

◆ setProb()

◆ sieve()

◆ toString() [1/2]

◆ toString() [2/2]

◆ toStringHelper()

◆ TseytinCNF()

◆ tseytinVariableMapping()

◆ wmcCount()

Friends And Related Symbol Documentation

◆ boost::serialization::access

◆ dDNNFTreeDecompositionBuilder

Member Data Documentation

◆ info

◆ inputs

◆ mulinputs

◆ prob

◆ probabilistic