From 3dab908bb6f21a1e3b1c48ffd64e86157ee21002 Mon Sep 17 00:00:00 2001 From: Pierre Senellart Date: Tue, 7 Nov 2023 17:56:41 +0800 Subject: [PATCH] Simple procedure to try and interpret a circuit as dD if possible --- src/BooleanCircuit.cpp | 91 +++++++++++++++++++++- src/BooleanCircuit.h | 6 +- src/TreeDecompositionKnowledgeCompiler.cpp | 2 +- src/dDNNF.cpp | 7 +- src/dDNNF.h | 9 ++- src/probability_evaluate.cpp | 19 ++--- src/shapley.cpp | 22 ++---- 7 files changed, 115 insertions(+), 41 deletions(-) diff --git a/src/BooleanCircuit.cpp b/src/BooleanCircuit.cpp index 63ab6dc..ab48441 100644 --- a/src/BooleanCircuit.cpp +++ b/src/BooleanCircuit.cpp @@ -16,7 +16,7 @@ extern "C" { #include #include -#include "dDNNF.h" +#include "dDNNFTreeDecompositionBuilder.h" // "provsql_utils.h" #ifdef TDKC @@ -353,7 +353,7 @@ std::string BooleanCircuit::Tseytin(gate_t g, bool display_prob=false) const { return filename; } -double BooleanCircuit::compilation(gate_t g, std::string compiler) const { +dDNNF BooleanCircuit::compilation(gate_t g, std::string compiler) const { std::string filename=BooleanCircuit::Tseytin(g); std::string outfilename=filename+".nnf"; @@ -404,7 +404,7 @@ double BooleanCircuit::compilation(gate_t g, std::string compiler) const { if(compiler != "d4") { // unsatisfiable formula - return 0.; + return dDNNF(); } } else { std::string nnf; @@ -517,7 +517,9 @@ double BooleanCircuit::compilation(gate_t g, std::string compiler) const { } else elog(NOTICE, "Compiled d-DNNF in %s", outfilename.c_str()); - return dnnf.dDNNFProbabilityEvaluation(dnnf.getGate(new_d4?"1":std::to_string(i-1))); + dnnf.setRoot(dnnf.getGate(new_d4?"1":std::to_string(i-1))); + + return dnnf; } double BooleanCircuit::WeightMC(gate_t g, std::string opt) const { @@ -746,3 +748,84 @@ void BooleanCircuit::rewriteMultivaluedGates() rewriteMultivaluedGatesRec(muls, cumulated_probs, 0, n-1, prefix); } } + +gate_t BooleanCircuit::interpretAsDDInternal(gate_t g, std::set &seen, dDNNF &dd) const { + gate_t dg{0}; + + switch(getGateType(g)) { + case BooleanGate::AND: + { + dg = dd.setGate(BooleanGate::AND); + for(const auto &c: getWires(g)) { + auto dc = interpretAsDDInternal(c, seen, dd); + dd.addWire(dg, dc); + } + } + break; + + case BooleanGate::OR: + { + dg = dd.setGate(BooleanGate::NOT); + auto dng = dd.setGate(BooleanGate::AND); + dd.addWire(dg, dng); + for(const auto &c: getWires(g)) { + auto dc = interpretAsDDInternal(c, seen, dd); + auto dnc = dd.setGate(BooleanGate::NOT); + dd.addWire(dnc, dc); + dd.addWire(dng, dnc); + } + } + break; + + case BooleanGate::NOT: + { + dg = dd.setGate(BooleanGate::NOT); + auto dc = interpretAsDDInternal(getWires(g)[0], seen, dd); + dd.addWire(dg, dc); + } + break; + + case BooleanGate::IN: + if(seen.find(g)!=seen.end()) + throw CircuitException("Not an independent circuit"); + seen.insert(g); + dg = dd.setGate(getUUID(g), BooleanGate::IN, getProb(g)); + break; + + case BooleanGate::MULIN: + case BooleanGate::MULVAR: + case BooleanGate::UNDETERMINED: + throw CircuitException("Unsupported gate in interpretAsDD"); + } + + return dg; +} + +dDNNF BooleanCircuit::interpretAsDD(gate_t g) const +{ + dDNNF dd; + std::set seen; + + dd.setRoot(interpretAsDDInternal(g, seen, dd)); + + return dd; +} + +dDNNF BooleanCircuit::makeDD(gate_t g) const +{ + dDNNF dd; + + try { + dd = interpretAsDD(g); + } catch(CircuitException &) { + try { + TreeDecomposition td(*this); + dd = dDNNFTreeDecompositionBuilder{ + *this, id2uuid.find(g)->second, td}.build(); + } catch(TreeDecompositionException &) { + dd = compilation(g, "d4"); + } + } + + return dd; +} diff --git a/src/BooleanCircuit.h b/src/BooleanCircuit.h index c717cf3..642a631 100644 --- a/src/BooleanCircuit.h +++ b/src/BooleanCircuit.h @@ -10,11 +10,13 @@ #include "Circuit.hpp" enum class BooleanGate { UNDETERMINED, AND, OR, NOT, IN, MULIN, MULVAR }; +class dDNNF; class BooleanCircuit : public Circuit { private: bool evaluate(gate_t g, const std::unordered_set &sampled) const; std::string Tseytin(gate_t g, bool display_prob) const; +gate_t interpretAsDDInternal(gate_t g, std::set &seen, dDNNF &dd) const; double independentEvaluationInternal(gate_t g, std::set &seen) const; void rewriteMultivaluedGatesRec( const std::vector &muls, @@ -47,11 +49,13 @@ void setInfo(gate_t g, unsigned info); unsigned getInfo(gate_t g) const; double possibleWorlds(gate_t g) const; -double compilation(gate_t g, std::string compiler) const; +dDNNF compilation(gate_t g, std::string compiler) const; double monteCarlo(gate_t g, unsigned samples) const; double WeightMC(gate_t g, std::string opt) const; double independentEvaluation(gate_t g) const; void rewriteMultivaluedGates(); +dDNNF interpretAsDD(gate_t g) const; +dDNNF makeDD(gate_t g) const; virtual std::string toString(gate_t g) const override; std::string exportCircuit(gate_t g) const; diff --git a/src/TreeDecompositionKnowledgeCompiler.cpp b/src/TreeDecompositionKnowledgeCompiler.cpp index 7c8e9aa..5e6c8e1 100644 --- a/src/TreeDecompositionKnowledgeCompiler.cpp +++ b/src/TreeDecompositionKnowledgeCompiler.cpp @@ -65,7 +65,7 @@ int main(int argc, char **argv) { std::cerr << "Computing dDNNF took " << (t1-t0) << "s" << std::endl; t0 = t1; - std::cerr << "Probability: " << std::setprecision (15) << dnnf.dDNNFProbabilityEvaluation(dnnf.getRoot()) << std::endl; + std::cerr << "Probability: " << std::setprecision (15) << dnnf.probabilityEvaluation() << std::endl; t1 = get_timestamp(); std::cerr << "Evaluating dDNNF took " << (t1-t0) << "s" << std::endl; } catch(TreeDecompositionException&) { diff --git a/src/dDNNF.cpp b/src/dDNNF.cpp index 1868999..f051853 100644 --- a/src/dDNNF.cpp +++ b/src/dDNNF.cpp @@ -114,8 +114,11 @@ void dDNNF::makeGatesBinary(BooleanGate type) } } -double dDNNF::dDNNFProbabilityEvaluation(gate_t root) const +double dDNNF::probabilityEvaluation() const { + if (gates.size() == 0) + return 0.; + // Unfortunately, dDNNFs can be quite deep so we need to simulate // recursion with a heap-based stack, to avoid exhausting the actual // memory stack @@ -384,7 +387,7 @@ std::vector > dDNNF::shapley_alpha(gate_t root) const { return result[root]; } -double dDNNF::shapley(gate_t root, gate_t var) const { +double dDNNF::shapley(gate_t var) const { auto cond_pos = condition(var, true); auto cond_neg = condition(var, false); diff --git a/src/dDNNF.h b/src/dDNNF.h index 5c0c579..7cea3f0 100644 --- a/src/dDNNF.h +++ b/src/dDNNF.h @@ -31,17 +31,20 @@ gate_t root; gate_t getRoot() const { return root; } +void setRoot(gate_t g) { + root=g; +} std::unordered_set vars(gate_t root) const; void makeSmooth(); void makeGatesBinary(BooleanGate type); void simplify(); dDNNF conditionAndSimplify(gate_t var, bool value) const; dDNNF condition(gate_t var, bool value) const; -double dDNNFProbabilityEvaluation(gate_t root) const; -double shapley(gate_t g, gate_t var) const; +double probabilityEvaluation() const; +double shapley(gate_t var) const; friend dDNNFTreeDecompositionBuilder; -friend double BooleanCircuit::compilation(gate_t g, std::string compiler) const; +friend dDNNF BooleanCircuit::compilation(gate_t g, std::string compiler) const; }; #endif /* DDNNF_H */ diff --git a/src/probability_evaluate.cpp b/src/probability_evaluate.cpp index cbef146..a4ac669 100644 --- a/src/probability_evaluate.cpp +++ b/src/probability_evaluate.cpp @@ -80,7 +80,8 @@ static Datum probability_evaluate_internal result = c.possibleWorlds(gate); } else if(method=="compilation") { - result = c.compilation(gate, args); + auto dd = c.compilation(gate, args); + result = dd.probabilityEvaluation(); } else if(method=="weightmc") { result = c.WeightMC(gate, args); } else if(method=="tree-decomposition") { @@ -92,23 +93,13 @@ static Datum probability_evaluate_internal uuid2string(token), td}.build() }; - result = dnnf.dDNNFProbabilityEvaluation(dnnf.getRoot()); + result = dnnf.probabilityEvaluation(); } catch(TreeDecompositionException &) { elog(ERROR, "Treewidth greater than %u", TreeDecomposition::MAX_TREEWIDTH); } } else if(method=="") { - try { - TreeDecomposition td(c); - auto dnnf{ - dDNNFTreeDecompositionBuilder{ - c, - uuid2string(token), - td}.build() - }; - result = dnnf.dDNNFProbabilityEvaluation(dnnf.getRoot()); - } catch(TreeDecompositionException &) { - result = c.compilation(gate, "d4"); - } + auto dd = c.makeDD(gate); + result = dd.probabilityEvaluation(); } else { elog(ERROR, "Wrong method '%s' for probability evaluation", method.c_str()); } diff --git a/src/shapley.cpp b/src/shapley.cpp index ad72cc4..4e26420 100644 --- a/src/shapley.cpp +++ b/src/shapley.cpp @@ -26,31 +26,21 @@ static double shapley_internal if(c.getGateType(c.getGate(uuid2string(variable))) != BooleanGate::IN) return 0.; - dDNNF dnnf; + dDNNF dd = c.makeDD(c.getGate(uuid2string(token))); - try { - TreeDecomposition td(c); - dnnf = dDNNFTreeDecompositionBuilder{ - c, uuid2string(token), td}.build(); - } catch(TreeDecompositionException &) { - elog(ERROR, "Treewidth greater than %u", TreeDecomposition::MAX_TREEWIDTH); - return 0.; - } - - dnnf.makeSmooth(); - dnnf.makeGatesBinary(BooleanGate::AND); + dd.makeSmooth(); + dd.makeGatesBinary(BooleanGate::AND); - auto root=dnnf.getRoot(); - auto var_gate=dnnf.getGate(uuid2string(variable)); + auto var_gate=dd.getGate(uuid2string(variable)); /* std::string filename("/tmp/export.dd"); std::ofstream o(filename.c_str()); - o << dnnf.exportCircuit(root); + o << dd.exportCircuit(root); o.close(); */ - double result = dnnf.shapley(root, var_gate); + double result = dd.shapley(var_gate); // Avoid rounding errors that make expected Shapley value outside of [-1,1] if(result>1.)