show weights in dot file and add support for smoothing set-and nodes

This commit is contained in:
Tiago Gomes 2012-10-29 15:39:56 +00:00
parent fbc44ba17d
commit c2b1434969
2 changed files with 76 additions and 41 deletions

View File

@ -8,6 +8,7 @@ OrNode::weight (void) const
{ {
double lw = leftBranch_->weight(); double lw = leftBranch_->weight();
double rw = rightBranch_->weight(); double rw = rightBranch_->weight();
cout << ">>>> OR NODE res = " << lw << " + " << rw << endl;
return Globals::logDomain ? Util::logSum (lw, rw) : lw + rw; return Globals::logDomain ? Util::logSum (lw, rw) : lw + rw;
} }
@ -38,9 +39,10 @@ double
SetAndNode::weight (void) const SetAndNode::weight (void) const
{ {
unsigned nrGroundings = 2; // FIXME unsigned nrGroundings = 2; // FIXME
double w = follow_->weight();
return Globals::logDomain return Globals::logDomain
? follow_->weight() * nrGroundings ? w * nrGroundings
: std::pow (follow_->weight(), nrGroundings); : std::pow (w, nrGroundings);
} }
@ -52,14 +54,14 @@ LeafNode::weight (void) const
assert (clauses()[0].isUnit()); assert (clauses()[0].isUnit());
Clause c = clauses()[0]; Clause c = clauses()[0];
double weight = c.literals()[0].weight(); double weight = c.literals()[0].weight();
unsigned nrGroundings = c.constr().size(); LogVarSet lvs = c.constr().logVarSet() - c.ipgLogVars();
unsigned nrGroundings = 1;
if (lvs.empty() == false) {
ConstraintTree ct = c.constr();
ct.project (lvs);
nrGroundings = ct.size();
}
assert (nrGroundings != 0); assert (nrGroundings != 0);
double www = Globals::logDomain
? weight * nrGroundings
: std::pow (weight, nrGroundings);
cout << "leaf weight(" << clauses()[0].literals()[0] << "): " << www << endl;
return Globals::logDomain return Globals::logDomain
? weight * nrGroundings ? weight * nrGroundings
: std::pow (weight, nrGroundings); : std::pow (weight, nrGroundings);
@ -325,29 +327,33 @@ LiftedCircuit::tryIndepPartialGrounding (
Clauses& clauses) Clauses& clauses)
{ {
// assumes that all literals have logical variables // assumes that all literals have logical variables
LogVar X = clauses[0].constr().logVars()[0]; // else, shannon decomp was possible
ConstraintTree ct = clauses[0].constr();
// FIXME this is so weak ... LogVarSet lvs = clauses[0].constr().logVarSet();
ct.project ({X}); lvs -= clauses[0].ipgLogVars();
for (size_t i = 0; i < clauses.size(); i++) { for (unsigned i = 0; i < lvs.size(); i++) {
if (clauses[i].constr().logVars().size() == 1) { LogVar X = lvs[i];
if (ct.tupleSet() != clauses[i].constr().tupleSet()) { ConstraintTree ct = clauses[0].constr();
ct.project ({X});
for (size_t j = 0; j < clauses.size(); j++) {
if (clauses[j].constr().logVars().size() == 1) {
if (ct.tupleSet() != clauses[j].constr().tupleSet()) {
return false;
}
} else {
return false; return false;
} }
} else {
return false;
} }
} }
// FIXME this is so broken ... // FIXME this is so broken ...
Clauses newClauses = clauses; Clauses newClauses = clauses;
for (size_t i = 0; i < clauses.size(); i++) { for (size_t i = 0; i < clauses.size(); i++) {
newClauses[i].addIpgLogVar (clauses[i].constr().logVars()[0]); newClauses[i].addIpgLogVar (clauses[i].constr().logVars()[0]);
} }
string explanation = " IPG" ; // FIXME
SetAndNode* node = new SetAndNode (clauses, explanation); SetAndNode* node = new SetAndNode (2, clauses);
*follow = node; *follow = node;
compile (node->follow(), newClauses); compile (node->follow(), newClauses);
return true; return true;
@ -357,8 +363,8 @@ LiftedCircuit::tryIndepPartialGrounding (
bool bool
LiftedCircuit::tryGrounding ( LiftedCircuit::tryGrounding (
CircuitNode** follow, CircuitNode**,
Clauses& clauses) Clauses&)
{ {
return false; return false;
/* /*
@ -440,15 +446,18 @@ LiftedCircuit::smoothCircuit (CircuitNode* node)
} }
case CircuitNodeType::SET_OR_NODE: { case CircuitNodeType::SET_OR_NODE: {
// TODO break;
} }
case CircuitNodeType::SET_AND_NODE: { case CircuitNodeType::SET_AND_NODE: {
// TODO SetAndNode* casted = dynamic_cast<SetAndNode*>(node);
propagatingLids = smoothCircuit (*casted->follow());
break;
} }
case CircuitNodeType::INC_EXC_NODE: { case CircuitNodeType::INC_EXC_NODE: {
// TODO // TODO
break;
} }
case CircuitNodeType::LEAF_NODE: { case CircuitNodeType::LEAF_NODE: {
@ -524,21 +533,30 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os)
OrNode* casted = dynamic_cast<OrNode*>(node); OrNode* casted = dynamic_cast<OrNode*>(node);
const Clauses& clauses = node->clauses(); const Clauses& clauses = node->clauses();
if (clauses.empty() == false) { if (clauses.empty() == false) {
os << escapeNode (node) << " [shape=box,label=\"" ; os << escapeNode (node) << " [shape=box,label=\"" ;
for (size_t i = 0; i < clauses.size(); i++) { for (size_t i = 0; i < clauses.size(); i++) {
if (i != 0) os << "\\n" ; if (i != 0) os << "\\n" ;
os << clauses[i]; os << clauses[i];
} }
os << "\"]" ; os << "\"]" ;
os << endl; os << endl;
} }
os << auxNode << " [label=\"\"]" << endl; os << auxNode << " [label=\"\"]" << endl;
os << escapeNode (node) << " -> " << auxNode; os << escapeNode (node) << " -> " << auxNode;
os << " [label=\"" << node->explanation() << "\"]" << endl; os << " [label=\"" << node->explanation() << "\"]" ;
os << endl;
os << auxNode << " -> " ; os << auxNode << " -> " ;
os << escapeNode (*casted->leftBranch()) << endl; os << escapeNode (*casted->leftBranch());
os << " [label=\" " << (*casted->leftBranch())->weight() << "\"]" ;
os << endl;
os << auxNode << " -> " ; os << auxNode << " -> " ;
os << escapeNode (*casted->rightBranch()) << endl; os << escapeNode (*casted->rightBranch());
os << " [label=\" " << (*casted->rightBranch())->weight() << "\"]" ;
os << endl;
exportToGraphViz (*casted->leftBranch(), os); exportToGraphViz (*casted->leftBranch(), os);
exportToGraphViz (*casted->rightBranch(), os); exportToGraphViz (*casted->rightBranch(), os);
break; break;
@ -554,13 +572,22 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os)
} }
os << "\"]" ; os << "\"]" ;
os << endl; os << endl;
os << auxNode << " [label=\"\"]" << endl; os << auxNode << " [label=\"\"]" << endl;
os << escapeNode (node) << " -> " << auxNode; os << escapeNode (node) << " -> " << auxNode;
os << " [label=\"" << node->explanation() << "\"]" << endl; os << " [label=\"" << node->explanation() << "\"]" ;
os << endl;
os << auxNode << " -> " ; os << auxNode << " -> " ;
os << escapeNode (*casted->leftBranch()) << endl; os << escapeNode (*casted->leftBranch());
os << " [label=\" " << (*casted->leftBranch())->weight() << "\"]" ;
os << endl;
os << auxNode << " -> " ; os << auxNode << " -> " ;
os << escapeNode (*casted->rightBranch()) << endl; os << escapeNode (*casted->rightBranch()) << endl;
os << " [label=\" " << (*casted->rightBranch())->weight() << "\"]" ;
os << endl;
exportToGraphViz (*casted->leftBranch(), os); exportToGraphViz (*casted->leftBranch(), os);
exportToGraphViz (*casted->rightBranch(), os); exportToGraphViz (*casted->rightBranch(), os);
break; break;
@ -580,11 +607,17 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os)
} }
os << "\"]" ; os << "\"]" ;
os << endl; os << endl;
os << auxNode << " [label=\"∧(X)\"]" << endl; os << auxNode << " [label=\"∧(X)\"]" << endl;
os << escapeNode (node) << " -> " << auxNode; os << escapeNode (node) << " -> " << auxNode;
os << " [label=\"" << node->explanation() << "\"]" << endl; os << " [label=\"" << node->explanation() << "\"]" ;
os << endl;
os << auxNode << " -> " ; os << auxNode << " -> " ;
os << escapeNode (*casted->follow()) << endl; os << escapeNode (*casted->follow());
os << " [label=\" " << (*casted->follow())->weight() << "\"]" ;
os << endl;
exportToGraphViz (*casted->follow(), os); exportToGraphViz (*casted->follow(), os);
break; break;
} }

View File

@ -108,13 +108,15 @@ class SetOrNode : public CircuitNode
class SetAndNode : public CircuitNode class SetAndNode : public CircuitNode
{ {
public: public:
SetAndNode (const Clauses& clauses, string explanation = "") SetAndNode (unsigned nrGroundings, const Clauses& clauses)
: CircuitNode (clauses, explanation), follow_(0) { } : CircuitNode (clauses, ""), nrGroundings_(nrGroundings),
follow_(0) { }
double weight (void) const; double weight (void) const;
CircuitNode** follow (void) { return &follow_; } CircuitNode** follow (void) { return &follow_; }
private: private:
unsigned nrGroundings_;
CircuitNode* follow_; CircuitNode* follow_;
}; };