make independent partial ground suck less
This commit is contained in:
parent
c2b1434969
commit
324ea1a96c
@ -329,35 +329,52 @@ LiftedCircuit::tryIndepPartialGrounding (
|
|||||||
// assumes that all literals have logical variables
|
// assumes that all literals have logical variables
|
||||||
// else, shannon decomp was possible
|
// else, shannon decomp was possible
|
||||||
|
|
||||||
LogVarSet lvs = clauses[0].constr().logVarSet();
|
vector<unsigned> lvIndices;
|
||||||
lvs -= clauses[0].ipgLogVars();
|
LogVarSet lvs = clauses[0].ipgCandidates();
|
||||||
for (unsigned i = 0; i < lvs.size(); i++) {
|
for (size_t i = 0; i < lvs.size(); i++) {
|
||||||
LogVar X = lvs[i];
|
lvIndices.clear();
|
||||||
|
lvIndices.push_back (i);
|
||||||
ConstraintTree ct = clauses[0].constr();
|
ConstraintTree ct = clauses[0].constr();
|
||||||
ct.project ({X});
|
ct.project ({lvs[i]});
|
||||||
for (size_t j = 0; j < clauses.size(); j++) {
|
if (tryIndepPartialGroundingAux (clauses, ct, lvIndices)) {
|
||||||
if (clauses[j].constr().logVars().size() == 1) {
|
|
||||||
if (ct.tupleSet() != clauses[j].constr().tupleSet()) {
|
|
||||||
return false;
|
|
||||||
}
|
|
||||||
} else {
|
|
||||||
return false;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
// 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]);
|
LogVar lv = clauses[i].ipgCandidates()[lvIndices[i]];
|
||||||
|
newClauses[i].addIpgLogVar (lv);
|
||||||
}
|
}
|
||||||
|
SetAndNode* node = new SetAndNode (ct.size(), clauses);
|
||||||
// FIXME
|
|
||||||
SetAndNode* node = new SetAndNode (2, clauses);
|
|
||||||
*follow = node;
|
*follow = node;
|
||||||
compile (node->follow(), newClauses);
|
compile (node->follow(), newClauses);
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
|
}
|
||||||
|
return false;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
bool
|
||||||
|
LiftedCircuit::tryIndepPartialGroundingAux (
|
||||||
|
Clauses& clauses,
|
||||||
|
ConstraintTree& ct,
|
||||||
|
vector<unsigned>& lvIndices)
|
||||||
|
{
|
||||||
|
for (size_t j = 1; j < clauses.size(); j++) {
|
||||||
|
LogVarSet lvs2 = clauses[j].ipgCandidates();
|
||||||
|
for (size_t k = 0; k < lvs2.size(); k++) {
|
||||||
|
ConstraintTree ct2 = clauses[j].constr();
|
||||||
|
ct2.project ({lvs2[k]});
|
||||||
|
if (ct.tupleSet() == ct2.tupleSet()) {
|
||||||
|
lvIndices.push_back (k);
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
if (lvIndices.size() != j+1) {
|
||||||
|
return false;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
@ -414,8 +431,8 @@ LiftedCircuit::smoothCircuit (CircuitNode* node)
|
|||||||
}
|
}
|
||||||
SmoothNode* smoothNode = new SmoothNode (clauses);
|
SmoothNode* smoothNode = new SmoothNode (clauses);
|
||||||
CircuitNode** prev = casted->leftBranch();
|
CircuitNode** prev = casted->leftBranch();
|
||||||
string explanation = " smoothing" ;
|
AndNode* andNode = new AndNode ((*prev)->clauses(),
|
||||||
AndNode* andNode = new AndNode ((*prev)->clauses(), smoothNode, *prev, explanation);
|
smoothNode, *prev, " smoothing");
|
||||||
*prev = andNode;
|
*prev = andNode;
|
||||||
}
|
}
|
||||||
if (missingRight.empty() == false) {
|
if (missingRight.empty() == false) {
|
||||||
@ -427,8 +444,8 @@ LiftedCircuit::smoothCircuit (CircuitNode* node)
|
|||||||
}
|
}
|
||||||
SmoothNode* smoothNode = new SmoothNode (clauses);
|
SmoothNode* smoothNode = new SmoothNode (clauses);
|
||||||
CircuitNode** prev = casted->rightBranch();
|
CircuitNode** prev = casted->rightBranch();
|
||||||
string explanation = " smoothing" ;
|
AndNode* andNode = new AndNode ((*prev)->clauses(), smoothNode,
|
||||||
AndNode* andNode = new AndNode ((*prev)->clauses(), smoothNode, *prev, explanation);
|
*prev, " smoothing");
|
||||||
*prev = andNode;
|
*prev = andNode;
|
||||||
}
|
}
|
||||||
propagatingLids |= lids1;
|
propagatingLids |= lids1;
|
||||||
|
@ -109,7 +109,7 @@ class SetAndNode : public CircuitNode
|
|||||||
{
|
{
|
||||||
public:
|
public:
|
||||||
SetAndNode (unsigned nrGroundings, const Clauses& clauses)
|
SetAndNode (unsigned nrGroundings, const Clauses& clauses)
|
||||||
: CircuitNode (clauses, ""), nrGroundings_(nrGroundings),
|
: CircuitNode (clauses, "IPG"), nrGroundings_(nrGroundings),
|
||||||
follow_(0) { }
|
follow_(0) { }
|
||||||
|
|
||||||
double weight (void) const;
|
double weight (void) const;
|
||||||
@ -191,6 +191,8 @@ class LiftedCircuit
|
|||||||
bool tryIndependence (CircuitNode** follow, Clauses& clauses);
|
bool tryIndependence (CircuitNode** follow, Clauses& clauses);
|
||||||
bool tryShannonDecomp (CircuitNode** follow, Clauses& clauses);
|
bool tryShannonDecomp (CircuitNode** follow, Clauses& clauses);
|
||||||
bool tryIndepPartialGrounding (CircuitNode** follow, Clauses& clauses);
|
bool tryIndepPartialGrounding (CircuitNode** follow, Clauses& clauses);
|
||||||
|
bool tryIndepPartialGroundingAux (Clauses& clauses, ConstraintTree& ct,
|
||||||
|
vector<unsigned>& indices);
|
||||||
bool tryGrounding (CircuitNode** follow, Clauses& clauses);
|
bool tryGrounding (CircuitNode** follow, Clauses& clauses);
|
||||||
|
|
||||||
TinySet<LiteralId> smoothCircuit (CircuitNode* node);
|
TinySet<LiteralId> smoothCircuit (CircuitNode* node);
|
||||||
|
@ -136,6 +136,29 @@ Clause::removeNegativeLiterals (LiteralId lid)
|
|||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
LogVarSet
|
||||||
|
Clause::ipgCandidates (void) const
|
||||||
|
{
|
||||||
|
LogVarSet candidates;
|
||||||
|
LogVarSet allLvs = constr_.logVarSet();
|
||||||
|
allLvs -= ipgLogVars_;
|
||||||
|
for (size_t i = 0; i < allLvs.size(); i++) {
|
||||||
|
bool valid = true;
|
||||||
|
for (size_t j = 0; j < literals_.size(); j++) {
|
||||||
|
if (Util::contains (literals_[j].logVars(), allLvs[i]) == false) {
|
||||||
|
valid = false;
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
if (valid) {
|
||||||
|
candidates.insert (allLvs[i]);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
return candidates;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
TinySet<LiteralId>
|
TinySet<LiteralId>
|
||||||
Clause::lidSet (void) const
|
Clause::lidSet (void) const
|
||||||
{
|
{
|
||||||
|
@ -90,6 +90,8 @@ class Clause
|
|||||||
|
|
||||||
void addIpgLogVar (LogVar X) { ipgLogVars_.insert (X); }
|
void addIpgLogVar (LogVar X) { ipgLogVars_.insert (X); }
|
||||||
|
|
||||||
|
LogVarSet ipgCandidates (void) const;
|
||||||
|
|
||||||
TinySet<LiteralId> lidSet (void) const;
|
TinySet<LiteralId> lidSet (void) const;
|
||||||
|
|
||||||
friend std::ostream& operator<< (ostream &os, const Clause& clause);
|
friend std::ostream& operator<< (ostream &os, const Clause& clause);
|
||||||
|
Reference in New Issue
Block a user