From f7db522c6c6ba7caba4918a3b5b4cf3963a08002 Mon Sep 17 00:00:00 2001 From: Tiago Gomes Date: Wed, 7 Nov 2012 23:45:43 +0000 Subject: [PATCH] InxExc: improve the code --- packages/CLPBN/horus/LiftedCircuit.cpp | 123 ++++++++++++++++--------- packages/CLPBN/horus/LiftedCircuit.h | 26 +++--- packages/CLPBN/horus/LiftedWCNF.cpp | 14 +-- 3 files changed, 100 insertions(+), 63 deletions(-) diff --git a/packages/CLPBN/horus/LiftedCircuit.cpp b/packages/CLPBN/horus/LiftedCircuit.cpp index d520a51a5..cb7ba75a4 100644 --- a/packages/CLPBN/horus/LiftedCircuit.cpp +++ b/packages/CLPBN/horus/LiftedCircuit.cpp @@ -341,7 +341,7 @@ LiftedCircuit::tryIndependence ( while (finish == false) { finish = true; for (size_t i = 0; i < indepClauses.size(); i++) { - if (isIndependentClause (indepClauses[i], depClauses) == false) { + if (independentClause (indepClauses[i], depClauses) == false) { depClauses.push_back (indepClauses[i]); indepClauses.erase (indepClauses.begin() + i); finish = false; @@ -402,44 +402,58 @@ LiftedCircuit::tryInclusionExclusion ( CircuitNode** follow, Clauses& clauses) { - // TODO compare all subsets with all subsets for (size_t i = 0; i < clauses.size(); i++) { - const Literals& literals = clauses[i].literals(); - for (size_t j = 0; j < literals.size(); j++) { - bool indep = true; - for (size_t k = 0; k < literals.size(); k++) { - LogVarSet intersect = literals[j].logVarSet() - & literals[k].logVarSet(); - if (j != k && intersect.empty() == false) { - indep = false; + Literals depLits = { clauses[i].literals().front() }; + Literals indepLits (clauses[i].literals().begin() + 1, + clauses[i].literals().end()); + bool finish = false; + while (finish == false) { + finish = true; + for (size_t j = 0; j < indepLits.size(); j++) { + if (independentLiteral (indepLits[j], depLits) == false) { + depLits.push_back (indepLits[j]); + indepLits.erase (indepLits.begin() + j); + finish = false; break; } } - if (indep) { - // TODO this should be have to be count normalized too - ConstraintTree really = clauses[i].constr(); - Clause c1 (really.projectedCopy ( - literals[j].logVars())); - c1.addLiteral (literals[j]); - Clause c2 = clauses[i]; - c2.removeLiteral (j); - Clauses plus1Clauses = clauses; - Clauses plus2Clauses = clauses; - Clauses minusClauses = clauses; - plus1Clauses.erase (plus1Clauses.begin() + i); - plus2Clauses.erase (plus2Clauses.begin() + i); - minusClauses.erase (minusClauses.begin() + i); - plus1Clauses.push_back (c1); - plus2Clauses.push_back (c2); - minusClauses.push_back (c1); - minusClauses.push_back (c2); - IncExcNode* ieNode = new IncExcNode (clauses); - compile (ieNode->plus1Branch(), plus1Clauses); - compile (ieNode->plus2Branch(), plus2Clauses); - compile (ieNode->minusBranch(), minusClauses); - *follow = ieNode; - return true; + } + if (indepLits.empty() == false) { + // TODO this should be have to be count normalized too + LogVarSet lvs1; + for (size_t j = 0; j < depLits.size(); j++) { + lvs1 |= depLits[j].logVarSet(); } + LogVarSet lvs2; + for (size_t j = 0; j < indepLits.size(); j++) { + lvs2 |= indepLits[j].logVarSet(); + } + Clause c1 (clauses[i].constr().projectedCopy (lvs1)); + for (size_t j = 0; j < depLits.size(); j++) { + c1.addLiteral (depLits[j]); + } + Clause c2 (clauses[i].constr().projectedCopy (lvs2)); + for (size_t j = 0; j < indepLits.size(); j++) { + c2.addLiteral (indepLits[j]); + } + Clauses plus1Clauses = clauses; + Clauses plus2Clauses = clauses; + Clauses minusClauses = clauses; + plus1Clauses.erase (plus1Clauses.begin() + i); + plus2Clauses.erase (plus2Clauses.begin() + i); + minusClauses.erase (minusClauses.begin() + i); + plus1Clauses.push_back (c1); + plus2Clauses.push_back (c2); + minusClauses.push_back (c1); + minusClauses.push_back (c2); + stringstream explanation; + explanation << " IncExc on clause nº " << i + 1; + IncExcNode* ieNode = new IncExcNode (clauses, explanation.str()); + compile (ieNode->plus1Branch(), plus1Clauses); + compile (ieNode->plus2Branch(), plus2Clauses); + compile (ieNode->minusBranch(), minusClauses); + *follow = ieNode; + return true; } } return false; @@ -651,7 +665,7 @@ LiftedCircuit::shatterCountedLogVarsAux ( bool -LiftedCircuit::isIndependentClause ( +LiftedCircuit::independentClause ( Clause& clause, Clauses& otherClauses) const { @@ -665,6 +679,22 @@ LiftedCircuit::isIndependentClause ( +bool +LiftedCircuit::independentLiteral ( + const Literal& lit, + const Literals& otherLits) const +{ + for (size_t i = 0; i < otherLits.size(); i++) { + if (lit.lid() == otherLits[i].lid() + || (lit.logVarSet() & otherLits[i].logVarSet()).empty() == false) { + return false; + } + } + return true; +} + + + LitLvTypesSet LiftedCircuit::smoothCircuit (CircuitNode* node) { @@ -882,7 +912,7 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os) ss << "n" << nrAuxNodes; string auxNode = ss.str(); nrAuxNodes ++; - + string opStyle = "shape=circle,width=0.7,margin=\"0.0,0.0\"," ; switch (getCircuitNodeType (node)) { @@ -890,7 +920,7 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os) OrNode* casted = dynamic_cast(node); printClauses (casted, os); - os << auxNode << " [label=\"∨\"]" << endl; + os << auxNode << " [" << opStyle << "label=\"∨\"]" << endl; os << escapeNode (node) << " -> " << auxNode; os << " [label=\"" << node->explanation() << "\"]" ; os << endl; @@ -914,7 +944,7 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os) AndNode* casted = dynamic_cast(node); printClauses (casted, os); - os << auxNode << " [label=\"∧\"]" << endl; + os << auxNode << " [" << opStyle << "label=\"∧\"]" << endl; os << escapeNode (node) << " -> " << auxNode; os << " [label=\"" << node->explanation() << "\"]" ; os << endl; @@ -938,7 +968,7 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os) SetOrNode* casted = dynamic_cast(node); printClauses (casted, os); - os << auxNode << " [label=\"∨(X)\"]" << endl; + os << auxNode << " [" << opStyle << "label=\"∨(X)\"]" << endl; os << escapeNode (node) << " -> " << auxNode; os << " [label=\"" << node->explanation() << "\"]" ; os << endl; @@ -956,7 +986,7 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os) SetAndNode* casted = dynamic_cast(node); printClauses (casted, os); - os << auxNode << " [label=\"∧(X)\"]" << endl; + os << auxNode << " [" << opStyle << "label=\"∧(X)\"]" << endl; os << escapeNode (node) << " -> " << auxNode; os << " [label=\"" << node->explanation() << "\"]" ; os << endl; @@ -974,7 +1004,8 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os) IncExcNode* casted = dynamic_cast(node); printClauses (casted, os); - os << auxNode << " [label=\"IncExc\"]" << endl; + os << auxNode << " [" << opStyle << "label=\"+ - +\"]" ; + os << endl; os << escapeNode (node) << " -> " << auxNode; os << " [label=\"" << node->explanation() << "\"]" ; os << endl; @@ -983,17 +1014,17 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os) os << escapeNode (*casted->plus1Branch()); os << " [label=\" " << (*casted->plus1Branch())->weight() << "\"]" ; os << endl; + + os << auxNode << " -> " ; + os << escapeNode (*casted->minusBranch()) << endl; + os << " [label=\" " << (*casted->minusBranch())->weight() << "\"]" ; + os << endl; os << auxNode << " -> " ; os << escapeNode (*casted->plus2Branch()); os << " [label=\" " << (*casted->plus2Branch())->weight() << "\"]" ; os << endl; - os << auxNode << " -> " ; - os << escapeNode (*casted->minusBranch()) << endl; - os << " [label=\" " << (*casted->minusBranch())->weight() << "\"]" ; - os << endl; - exportToGraphViz (*casted->plus1Branch(), os); exportToGraphViz (*casted->plus2Branch(), os); exportToGraphViz (*casted->minusBranch(), os); diff --git a/packages/CLPBN/horus/LiftedCircuit.h b/packages/CLPBN/horus/LiftedCircuit.h index e0adf49f5..073de64fe 100644 --- a/packages/CLPBN/horus/LiftedCircuit.h +++ b/packages/CLPBN/horus/LiftedCircuit.h @@ -54,8 +54,8 @@ class OrNode : public CircuitNode double weight (void) const; private: - CircuitNode* leftBranch_; - CircuitNode* rightBranch_; + CircuitNode* leftBranch_; + CircuitNode* rightBranch_; }; @@ -88,8 +88,8 @@ class AndNode : public CircuitNode double weight (void) const; private: - CircuitNode* leftBranch_; - CircuitNode* rightBranch_; + CircuitNode* leftBranch_; + CircuitNode* rightBranch_; }; @@ -139,8 +139,8 @@ class SetAndNode : public CircuitNode class IncExcNode : public CircuitNode { public: - IncExcNode (const Clauses& clauses) - : CircuitNode (clauses), plus1Branch_(0), + IncExcNode (const Clauses& clauses, string explanation) + : CircuitNode (clauses, explanation), plus1Branch_(0), plus2Branch_(0), minusBranch_(0) { } CircuitNode** plus1Branch (void) { return &plus1Branch_; } @@ -150,9 +150,9 @@ class IncExcNode : public CircuitNode double weight (void) const; private: - CircuitNode* plus1Branch_; - CircuitNode* plus2Branch_; - CircuitNode* minusBranch_; + CircuitNode* plus1Branch_; + CircuitNode* plus2Branch_; + CircuitNode* minusBranch_; }; @@ -198,7 +198,8 @@ class TrueNode : public CircuitNode class CompilationFailedNode : public CircuitNode { public: - CompilationFailedNode (const Clauses& clauses) : CircuitNode (clauses) { } + CompilationFailedNode (const Clauses& clauses) + : CircuitNode (clauses) { } double weight (void) const; }; @@ -243,7 +244,10 @@ class LiftedCircuit bool shatterCountedLogVarsAux (Clauses& clauses, size_t idx1, size_t idx2); - bool isIndependentClause (Clause& clause, Clauses& otherClauses) const; + bool independentClause (Clause& clause, Clauses& otherClauses) const; + + bool independentLiteral (const Literal& lit, + const Literals& otherLits) const; LitLvTypesSet smoothCircuit (CircuitNode* node); diff --git a/packages/CLPBN/horus/LiftedWCNF.cpp b/packages/CLPBN/horus/LiftedWCNF.cpp index f9f47d155..11e8b992b 100644 --- a/packages/CLPBN/horus/LiftedWCNF.cpp +++ b/packages/CLPBN/horus/LiftedWCNF.cpp @@ -377,22 +377,24 @@ LiftedWCNF::LiftedWCNF (const ParfactorList& pfList) */ Literal lit1 (0, {0}); - Literal lit2 (1, {}); - Literal lit3 (2, {}); - Literal lit4 (3, {}); + Literal lit2 (1, {0}); + Literal lit3 (2, {1}); + Literal lit4 (3, {1}); - vector> names = {{"p1"},{"p2"}}; + vector> names = {{"p1","p2"},{"p3","p4"}}; Clause c1 (names); c1.addLiteral (lit1); c1.addLiteral (lit2); - c1.addPosCountedLogVar (0); + c1.addLiteral (lit3); + c1.addLiteral (lit4); + //c1.addPosCountedLogVar (0); clauses_.push_back (c1); Clause c2 (names); c2.addLiteral (lit1); c2.addLiteral (lit3); c2.addNegCountedLogVar (0); - clauses_.push_back (c2); + //clauses_.push_back (c2); /* Clause c3; c3.addLiteral (lit3);