SumCmpEvaluator.h File Reference

Closed-form probability resolution for HAVING SUM(a) op C gate_cmps via a weighted-sum DP. More...

#include "GenericCircuit.h"

Include dependency graph for SumCmpEvaluator.h:

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

Go to the source code of this file.

Namespaces
namespace	provsql

Functions
unsigned	provsql::runSumCmpEvaluator (GenericCircuit &gc)
	Run the weighted-sum DP pre-pass over gc.

Detailed Description

Closed-form probability resolution for HAVING SUM(a) op C gate_cmps via a weighted-sum DP.

For comparators that reduce to gate_cmp(gate_agg(SUM, semimod_i(K_i, m_i)*), gate_value(C)) where the contributors are mutually independent Bernoulli trials (each K_i a private read-once sub-circuit, the same soundness contract as CountCmpEvaluator), the running sum S = sum of the present rows' integer weights m_i is a weighted Poisson-binomial. Its full distribution dp[s] = Pr(S = s) is computed by a subset-sum convolution – dp'[s] = dp[s](1 - p_i) + dp[s - m_i] p_i per child – over the reachable range [sum of negative m_i, sum of positive m_i]. The comparator's probability is then sum_{s : s op C} dp[s], with the empty-group world subtracted (see below). Cost O(N x R) where R is the reachable-sum range.

Pseudo-polynomial caveat. R is linear in the magnitude of the weights and the threshold, i.e. exponential in their bit-length, so this DP is only pseudo-polynomial (unlike COUNT, where the analogous range is bounded by N). The pass therefore declines (leaving the cmp for provsql_having) when R exceeds kMaxSumRange, falling back to the general enumeration path.

Soundness condition (checked per cmp gate, identical to CountCmpEvaluator) :

• shape matches gate_cmp(gate_agg(SUM, semimod_i(K_i, m_i)*), gate_value(C)) in either order ;
• the aggregate is consumed by this cmp alone, each semimod by the aggregate alone, and every randomness-bearing gate inside each K_i has reference count 1 – so the contributors are pairwise leaf-disjoint, private to the cmp, and individually read-once.

Empty-group semantics mirror count_enum / CountCmpEvaluator : the all-absent world (the only world with no present row) never satisfies HAVING. Its sum is the empty sum 0, so when 0 op C holds its mass prod_i (1 - p_i) is subtracted from the answer. Worlds that are non-empty but happen to sum to 0 (a present m_i = 0, or cancelling signed weights) are legitimately kept.

After replacement the cmp is a Bernoulli gate_input carrying the numeric probability, semantically meaningful only on the probability path. Like runCountCmpEvaluator, the pass runs inside probability_evaluate.cpp, gated on provsql.cmp_probability_evaluation, not at load time.

Definition in file SumCmpEvaluator.h.