ProvSQL C/C++ API
Adding support for provenance and uncertainty management to PostgreSQL databases
Loading...
Searching...
No Matches
BooleanCircuit.h
Go to the documentation of this file.
1/**
2 * @file BooleanCircuit.h
3 * @brief Boolean provenance circuit with support for knowledge compilation.
4 *
5 * @c BooleanCircuit represents the provenance formula of a query result
6 * as a Boolean circuit (AND/OR/NOT/IN gates). It supports multiple
7 * methods for computing the probability of the formula being true under
8 * tuple-independent probabilistic databases:
9 *
10 * | Method | Description |
11 * |------------------------|----------------------------------------------------------|
12 * | @c possibleWorlds() | Exact enumeration over all 2^n possible worlds |
13 * | @c compilation() | Knowledge compilation to d-DNNF via an external tool |
14 * | @c monteCarlo() | Monte Carlo sampling approximation |
15 * | @c WeightMC() | Weighted model counting via weightmc |
16 * | @c independentEvaluation() | Exact evaluation for disconnected circuits |
17 * | @c interpretAsDD() | Direct tree-decomposition-based compilation |
18 * | @c makeDD() | Generic d-DNNF construction dispatcher |
19 *
20 * ### Multivalued inputs (@c MULIN / @c MULVAR)
21 * Multivalued input gates model tuples drawn from a discrete probability
22 * distribution. @c rewriteMultivaluedGates() rewrites them into standard
23 * AND/OR/NOT circuits before knowledge compilation.
24 *
25 * The circuit is Boost-serialisable for transmission to external processes.
26 */
27#ifndef BOOLEAN_CIRCUIT_H
28#define BOOLEAN_CIRCUIT_H
29
30#include <unordered_map>
31#include <unordered_set>
32#include <set>
33#include <map>
34#include <vector>
35
36#include <boost/archive/binary_oarchive.hpp>
37#include <boost/serialization/unordered_map.hpp>
38#include <boost/serialization/map.hpp>
39#include <boost/serialization/set.hpp>
40#include <boost/serialization/vector.hpp>
41
42#include "Circuit.hpp"
43
44/**
45 * @brief Gate types for a Boolean provenance circuit.
46 *
47 * - @c UNDETERMINED Placeholder for a gate whose type has not been set yet.
48 * - @c AND Logical conjunction of child gates.
49 * - @c OR Logical disjunction of child gates.
50 * - @c NOT Logical negation of a single child gate.
51 * - @c IN An input (variable) gate representing a base tuple.
52 * - @c MULIN A multivalued-input gate (one of several options).
53 * - @c MULVAR Auxiliary gate grouping all @c MULIN siblings.
54 */
55enum class BooleanGate {
56 UNDETERMINED, ///< Placeholder gate whose type has not been set yet
57 AND, ///< Logical conjunction of child gates
58 OR, ///< Logical disjunction of child gates
59 NOT, ///< Logical negation of a single child gate
60 IN, ///< Input (variable) gate representing a base tuple
61 MULIN, ///< Multivalued-input gate (one of several options)
62 MULVAR ///< Auxiliary gate grouping all MULIN siblings
63};
64class dDNNF;
65
66/**
67 * @brief Boolean circuit for provenance formula evaluation.
68 *
69 * Inherits the gate/wire infrastructure from @c Circuit<BooleanGate> and
70 * adds probability annotation, info integers (for multivalued inputs), and
71 * a rich set of evaluation algorithms.
72 */
73class BooleanCircuit : public Circuit<BooleanGate> {
74private:
75/**
76 * @brief Evaluate the sub-circuit at @p g on one sampled world.
77 *
78 * Each gate in @p sampled is treated as @c true; all other @c IN gates
79 * are @c false.
80 *
81 * @param g Root gate to evaluate.
82 * @param sampled Set of input gates that are @c true in this world.
83 * @return Boolean value of the circuit at gate @p g.
84 */
85bool evaluate(gate_t g, const std::unordered_set<gate_t> &sampled) const;
86
87/**
88 * @brief Generate a Tseytin transformation of the sub-circuit at @p g.
89 *
90 * Produces a CNF/DIMACS-style encoding suitable for input to model
91 * counters such as @c weightmc or @c d4.
92 *
93 * @param g Root gate.
94 * @param display_prob Include probability weights in the output.
95 * @return DIMACS string.
96 */
97std::string Tseytin(gate_t g, bool display_prob) const;
98
99/**
100 * @brief Recursive helper for @c interpretAsDD().
101 * @param g Current gate to process.
102 * @param seen Set of gates already visited (prevents re-processing).
103 * @param dd The d-DNNF being constructed.
104 * @return Gate ID in @p dd corresponding to @p g.
105 */
106gate_t interpretAsDDInternal(gate_t g, std::set<gate_t> &seen, dDNNF &dd) const;
107/**
108 * @brief Recursive helper for @c independentEvaluation().
109 * @param g Current gate to evaluate.
110 * @param seen Set of gates already evaluated (for memoisation).
111 * @return Probability at gate @p g.
112 */
113double independentEvaluationInternal(gate_t g, std::set<gate_t> &seen) const;
114/**
115 * @brief Recursive helper for @c rewriteMultivaluedGates().
116 * @param muls Gates in the MULVAR group being rewritten.
117 * @param cumulated_probs Cumulative probability thresholds for each MULIN.
118 * @param start First index in @p muls to process.
119 * @param end One past the last index in @p muls to process.
120 * @param prefix Current AND-chain prefix being built.
121 */
123 const std::vector<gate_t> &muls,
124 const std::vector<double> &cumulated_probs,
125 unsigned start,
126 unsigned end,
127 std::vector<gate_t> &prefix);
128
129protected:
130std::set<gate_t> inputs; ///< Set of IN (input) gate IDs
131std::set<gate_t> mulinputs; ///< Set of MULVAR gate IDs
132std::vector<double> prob; ///< Per-gate probability (for IN gates)
133std::map<gate_t, unsigned> info; ///< Per-gate integer info (for MULIN gates)
134bool probabilistic=false; ///< @c true if any gate has a non-unit probability
135
136public:
137/** @brief Construct an empty Boolean circuit. */
141}
142
143/** @copydoc Circuit::addGate() */
144gate_t addGate() override;
145/** @copydoc Circuit::setGate(gateType) */
146gate_t setGate(BooleanGate type) override;
147/** @copydoc Circuit::setGate(const uuid&, gateType) */
148gate_t setGate(const uuid &u, BooleanGate type) override;
149
150/**
151 * @brief Create a new gate with a probability annotation.
152 * @param t Gate type (typically @c BooleanGate::IN).
153 * @param p Probability of this gate being @c true.
154 * @return Gate identifier.
155 */
156gate_t setGate(BooleanGate t, double p);
157
158/**
159 * @brief Create (or update) a gate with a UUID and probability.
160 * @param u UUID string.
161 * @param t Gate type.
162 * @param p Probability of this gate being @c true.
163 * @return Gate identifier.
164 */
165gate_t setGate(const uuid &u, BooleanGate t, double p);
166
167/**
168 * @brief Return the set of input (IN) gate IDs.
169 * @return Const reference to the set of IN gate identifiers.
170 */
171const std::set<gate_t> &getInputs() const {
172 return inputs;
173}
174
175/**
176 * @brief Set the probability for gate @p g and mark the circuit as probabilistic.
177 * @param g Gate identifier.
178 * @param p Probability value in [0, 1].
179 */
180void setProb(gate_t g, double p) {
181 if(!probabilistic && p!=1.)
182 probabilistic=true;
183 prob[static_cast<std::underlying_type<gate_t>::type>(g)]=p;
184}
185
186/**
187 * @brief Return the probability stored for gate @p g.
188 * @param g Gate identifier.
189 * @return Probability value.
190 */
191double getProb(gate_t g) const {
192 return prob[static_cast<std::underlying_type<gate_t>::type>(g)];
193}
194
195/**
196 * @brief Return @c true if any gate has a non-trivial (< 1) probability.
197 * @return @c true iff at least one gate has a probability strictly less than 1.
198 */
199bool isProbabilistic() const {
200 return probabilistic;
201}
202
203/**
204 * @brief Store an integer annotation on gate @p g.
205 *
206 * Used to record the index of a @c MULIN gate within its @c MULVAR group.
207 *
208 * @param g Gate identifier.
209 * @param info Integer to store.
210 */
211void setInfo(gate_t g, unsigned info);
212
213/**
214 * @brief Return the integer annotation for gate @p g.
215 * @param g Gate identifier.
216 * @return Stored integer, or 0 if not set.
217 */
218unsigned getInfo(gate_t g) const;
219
220/**
221 * @brief Compute the probability by exact enumeration of all possible worlds.
222 *
223 * Only tractable for circuits with a small number of input gates.
224 *
225 * @param g Root gate.
226 * @return Exact probability.
227 */
228double possibleWorlds(gate_t g) const;
229
230/**
231 * @brief Compile the sub-circuit rooted at @p g to a @c dDNNF via an external tool.
232 *
233 * Writes the circuit in DIMACS/DNNF format, invokes @p compiler as a
234 * subprocess, and parses the resulting d-DNNF.
235 *
236 * @param g Root gate.
237 * @param compiler Command to invoke (e.g. "d4", "c2d", "minic2d").
238 * @return The compiled @c dDNNF.
239 */
240dDNNF compilation(gate_t g, std::string compiler) const;
241
242/**
243 * @brief Estimate the probability via Monte Carlo sampling.
244 *
245 * @param g Root gate.
246 * @param samples Number of independent worlds to sample.
247 * @return Estimated probability.
248 */
249double monteCarlo(gate_t g, unsigned samples) const;
250
251/**
252 * @brief Compute the probability using the @c weightmc model counter.
253 *
254 * @param g Root gate.
255 * @param opt Additional command-line options forwarded to @c weightmc.
256 * @return Probability estimate returned by @c weightmc.
257 */
258double WeightMC(gate_t g, std::string opt) const;
259
260/**
261 * @brief Compute the probability exactly when inputs are independent.
262 *
263 * Applicable when the circuit has no shared input gate (i.e., each
264 * input appears at most once).
265 *
266 * @param g Root gate.
267 * @return Exact probability.
268 */
269double independentEvaluation(gate_t g) const;
270
271/**
272 * @brief Rewrite all MULVAR/MULIN gate clusters into standard AND/OR/NOT circuits.
273 *
274 * Must be called before any evaluation method when the circuit contains
275 * multivalued input gates.
276 */
278
279/**
280 * @brief Build a @c dDNNF directly from the Boolean circuit's structure.
281 *
282 * Used as a fallback when no external compiler is available and the
283 * circuit is already in a form that can be interpreted as a d-DNNF.
284 *
285 * @param g Root gate.
286 * @return A @c dDNNF wrapping the same structure.
287 */
288dDNNF interpretAsDD(gate_t g) const;
289
290/**
291 * @brief Dispatch to the appropriate d-DNNF construction method.
292 *
293 * @param g Root gate.
294 * @param method Compilation method name (e.g. "tree-decomposition",
295 * "d4", "c2d", …).
296 * @param args Additional arguments forwarded to the chosen method.
297 * @return The constructed @c dDNNF.
298 */
299dDNNF makeDD(gate_t g, const std::string &method, const std::string &args) const;
300
301/** @copydoc Circuit::toString() */
302virtual std::string toString(gate_t g) const override;
303
304/**
305 * @brief Export the circuit in the textual format expected by external compilers.
306 *
307 * Produces a multi-line string encoding all gates reachable from the
308 * circuit in the format used by the standalone @c tdkc tool and external
309 * model counters.
310 *
311 * @param g Root gate.
312 * @return Circuit description string.
313 */
314std::string exportCircuit(gate_t g) const;
315
316/**
317 * @brief Boost serialisation support.
318 * @param ar Boost archive (input or output).
319 * @param version Archive version (unused).
320 */
321template<class Archive>
322void serialize (Archive & ar, const unsigned int version)
323{
324 ar & uuid2id;
325 ar & id2uuid;
326 ar & gates;
327 ar & wires;
328 ar & inputs;
329 ar & mulinputs;
330 ar & prob;
331 ar & info;
332 ar & probabilistic;
333}
334
337};
338
339#endif /* BOOLEAN_CIRCUIT_H */
BooleanGate
Gate types for a Boolean provenance circuit.
@ MULVAR
Auxiliary gate grouping all MULIN siblings.
@ NOT
Logical negation of a single child gate.
@ OR
Logical disjunction of child gates.
@ AND
Logical conjunction of child gates.
@ IN
Input (variable) gate representing a base tuple.
@ UNDETERMINED
Placeholder gate whose type has not been set yet.
@ MULIN
Multivalued-input gate (one of several options)
gate_t
Strongly-typed gate identifier.
Definition Circuit.h:48
Out-of-line template method implementations for Circuit<gateType>.
Boolean circuit for provenance formula evaluation.
std::vector< double > prob
Per-gate probability (for IN gates)
virtual ~BooleanCircuit()
double WeightMC(gate_t g, std::string opt) const
Compute the probability using the weightmc model counter.
bool evaluate(gate_t g, const std::unordered_set< gate_t > &sampled) const
Evaluate the sub-circuit at g on one sampled world.
dDNNF interpretAsDD(gate_t g) const
Build a dDNNF directly from the Boolean circuit's structure.
double possibleWorlds(gate_t g) const
Compute the probability by exact enumeration of all possible worlds.
bool probabilistic
true if any gate has a non-unit probability
void setProb(gate_t g, double p)
Set the probability for gate g and mark the circuit as probabilistic.
std::set< gate_t > inputs
Set of IN (input) gate IDs.
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().
double independentEvaluationInternal(gate_t g, std::set< gate_t > &seen) const
Recursive helper for independentEvaluation().
std::string exportCircuit(gate_t g) const
Export the circuit in the textual format expected by external compilers.
const std::set< gate_t > & getInputs() const
Return the set of input (IN) gate IDs.
std::string Tseytin(gate_t g, bool display_prob) const
Generate a Tseytin transformation of the sub-circuit at g.
dDNNF makeDD(gate_t g, const std::string &method, const std::string &args) const
Dispatch to the appropriate d-DNNF construction method.
gate_t setGate(BooleanGate type) override
Allocate a new gate with type type and no UUID.
unsigned getInfo(gate_t g) const
Return the integer annotation for gate g.
gate_t addGate() override
Allocate a new gate with a default-initialised type.
double monteCarlo(gate_t g, unsigned samples) const
Estimate the probability via Monte Carlo sampling.
void rewriteMultivaluedGates()
Rewrite all MULVAR/MULIN gate clusters into standard AND/OR/NOT circuits.
double getProb(gate_t g) const
Return the probability stored for gate g.
void setInfo(gate_t g, unsigned info)
Store an integer annotation on gate g.
virtual std::string toString(gate_t g) const override
Return a textual description of gate g for debugging.
BooleanCircuit()
Construct an empty Boolean circuit.
void serialize(Archive &ar, const unsigned int version)
Boost serialisation support.
std::map< gate_t, unsigned > info
Per-gate integer info (for MULIN gates)
friend class boost::serialization::access
dDNNF compilation(gate_t g, std::string compiler) const
Compile the sub-circuit rooted at g to a dDNNF via an external tool.
bool isProbabilistic() const
Return true if any gate has a non-trivial (< 1) probability.
gate_t interpretAsDDInternal(gate_t g, std::set< gate_t > &seen, dDNNF &dd) const
Recursive helper for interpretAsDD().
double independentEvaluation(gate_t g) const
Compute the probability exactly when inputs are independent.
std::set< gate_t > mulinputs
Set of MULVAR gate IDs.
Generic template base class for provenance circuits.
Definition Circuit.h:61
std::string uuid
UUID type used in this circuit (always std::string).
Definition Circuit.h:64
std::unordered_map< gate_t, uuid > id2uuid
Gate index → UUID string.
Definition Circuit.h:68
std::unordered_map< uuid, gate_t > uuid2id
UUID string → gate index.
Definition Circuit.h:67
std::vector< BooleanGate > gates
Gate type for each gate.
Definition Circuit.h:70
std::vector< std::vector< gate_t > > wires
Child wire lists for each gate.
Definition Circuit.h:71
Builds a d-DNNF from a Boolean circuit using a tree decomposition.
A d-DNNF circuit supporting exact probabilistic and game-theoretic evaluation.
Definition dDNNF.h:69