Skip to content

Commit

Permalink
Simple procedure to try and interpret a circuit as dD if possible
Browse files Browse the repository at this point in the history
  • Loading branch information
PierreSenellart committed Nov 7, 2023
1 parent f828b7b commit 3dab908
Show file tree
Hide file tree
Showing 7 changed files with 115 additions and 41 deletions.
91 changes: 87 additions & 4 deletions src/BooleanCircuit.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ extern "C" {
#include <sstream>
#include <stack>

#include "dDNNF.h"
#include "dDNNFTreeDecompositionBuilder.h"

// "provsql_utils.h"
#ifdef TDKC
Expand Down Expand Up @@ -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";

Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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 {
Expand Down Expand Up @@ -746,3 +748,84 @@ void BooleanCircuit::rewriteMultivaluedGates()
rewriteMultivaluedGatesRec(muls, cumulated_probs, 0, n-1, prefix);
}
}

gate_t BooleanCircuit::interpretAsDDInternal(gate_t g, std::set<gate_t> &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<gate_t> 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;
}
6 changes: 5 additions & 1 deletion src/BooleanCircuit.h
Original file line number Diff line number Diff line change
Expand Up @@ -10,11 +10,13 @@
#include "Circuit.hpp"

enum class BooleanGate { UNDETERMINED, AND, OR, NOT, IN, MULIN, MULVAR };
class dDNNF;

class BooleanCircuit : public Circuit<BooleanGate> {
private:
bool evaluate(gate_t g, const std::unordered_set<gate_t> &sampled) const;
std::string Tseytin(gate_t g, bool display_prob) const;
gate_t interpretAsDDInternal(gate_t g, std::set<gate_t> &seen, dDNNF &dd) const;
double independentEvaluationInternal(gate_t g, std::set<gate_t> &seen) const;
void rewriteMultivaluedGatesRec(
const std::vector<gate_t> &muls,
Expand Down Expand Up @@ -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;
Expand Down
2 changes: 1 addition & 1 deletion src/TreeDecompositionKnowledgeCompiler.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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&) {
Expand Down
7 changes: 5 additions & 2 deletions src/dDNNF.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -384,7 +387,7 @@ std::vector<std::vector<double> > 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);

Expand Down
9 changes: 6 additions & 3 deletions src/dDNNF.h
Original file line number Diff line number Diff line change
Expand Up @@ -31,17 +31,20 @@ gate_t root;
gate_t getRoot() const {
return root;
}
void setRoot(gate_t g) {
root=g;
}
std::unordered_set<gate_t> 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 */
19 changes: 5 additions & 14 deletions src/probability_evaluate.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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") {
Expand All @@ -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());
}
Expand Down
22 changes: 6 additions & 16 deletions src/shapley.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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.)
Expand Down

0 comments on commit 3dab908

Please sign in to comment.