From 82e81e00d928b3bd8079a80704607fe3ef3cb539 Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Fri, 16 Feb 2018 00:30:17 +0100 Subject: [PATCH 01/13] pcasso: try to avoid local data structures Move vector initialization 2 loops out, to reduce the number of re-alloactions. --- pcasso-src/SolverPT.cc | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/pcasso-src/SolverPT.cc b/pcasso-src/SolverPT.cc index 59001c4..bc289e2 100644 --- a/pcasso-src/SolverPT.cc +++ b/pcasso-src/SolverPT.cc @@ -1435,6 +1435,7 @@ void SolverPT::push_learnts() bool sharedSuccess = false; bool fullPool = false; + vec c_lits; for (unsigned int i = 0; i < learnts_indeces.size(); i++) { davide::LevelPool* pool = previous_pools[i]; @@ -1453,7 +1454,7 @@ void SolverPT::push_learnts() Clause& c = ca[learnts[learnts_indeces[i][j]]]; c.setShared(); - vec c_lits; + c_lits.clear(); // memory consumption optimization for (unsigned j = 0; j < c.size(); j++) { //creating vector of literals present in the clause c_lits.push(c[j]); } From 275cf182e1617c9d15a73d0f5ccb61c49d6a97f5 Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Fri, 16 Feb 2018 00:32:58 +0100 Subject: [PATCH 02/13] pcasso: get learnts_indeces right When using an index to point into the learnts vector, make sure the items in that vector are valid, or in release mode are dropped to not crash the solver. This was found when using LCM which modified the learnts vector. --- pcasso-src/SolverPT.cc | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/pcasso-src/SolverPT.cc b/pcasso-src/SolverPT.cc index bc289e2..da8b0fb 100644 --- a/pcasso-src/SolverPT.cc +++ b/pcasso-src/SolverPT.cc @@ -1451,7 +1451,12 @@ void SolverPT::push_learnts() pool->levelPoolLock.wLock(); } for (unsigned int j = 0; j < learnts_indeces[i].size(); j++) { - Clause& c = ca[learnts[learnts_indeces[i][j]]]; + int lc_index = learnts_indeces[i][j]; + if (lc_index >= learnts.size()) { + assert(lc_index < learnts.size() && "indexes to learned clauses to share have to be in bounds"); + continue; + } + Clause& c = ca[learnts[lc_index]]; c.setShared(); c_lits.clear(); // memory consumption optimization From 96359f92da858b647959c905bafe266b2c2d8822 Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Fri, 16 Feb 2018 00:43:07 +0100 Subject: [PATCH 03/13] pcasso.sh: actually read tmp dir The tmp dir variable has been read from $3, while $2 was the actual aim. --- scripts/pcasso.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/pcasso.sh b/scripts/pcasso.sh index bcdcdb4..d4086c1 100755 --- a/scripts/pcasso.sh +++ b/scripts/pcasso.sh @@ -42,7 +42,7 @@ simplifier="$DIR/coprocessor" # file=$1 # first argument is CNF instance to be solved shift 1 -tmpDir=$2 # directory to write the temporary files to +tmpDir=$1 # directory to write the temporary files to shift 1 # reduce the parameters, removed the very first one. remaining $@ parameters are arguments # in case no tmpDir has been specified, create one and trap for deletion on exit From bc4d5afbcdc6ea8586dfe038eb9ddde79c973044 Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Tue, 20 Feb 2018 22:50:30 +0100 Subject: [PATCH 04/13] splitting: use var based index In the old version, the wrong variable has been used as index value, leading to out of bound errors. --- pcasso-src/LookaheadSplitting.cc | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/pcasso-src/LookaheadSplitting.cc b/pcasso-src/LookaheadSplitting.cc index fcf2455..73beb0d 100644 --- a/pcasso-src/LookaheadSplitting.cc +++ b/pcasso-src/LookaheadSplitting.cc @@ -1192,8 +1192,9 @@ Lit LookaheadSplitting::pickBranchLiteral(vec* > **valid) sizePositiveLookahead = trail.size() - initTrailSize; for (int j = initTrailSize; j < trail.size(); j++) { //fprintf(stderr, "Watcher size = %d\n", watches[trail[j]].size()); - sizeWatcherPositiveLookahead += sign(trail[j]) ? watcherNegLitSize[bestKList[i]] : watcherPosLitSize[bestKList[i]]; - binClausePositiveLookahead += sign(trail[j]) ? numPosLitTerClause[var(trail[j])] : numNegLitTerClause[var(trail[j])]; + const Var v = var(trail[j]); + sizeWatcherPositiveLookahead += sign(trail[j]) ? watcherNegLitSize[v] : watcherPosLitSize[v]; + binClausePositiveLookahead += sign(trail[j]) ? numPosLitTerClause[v] : numNegLitTerClause[v]; } //check if solution found if (checkSolution()) { @@ -1267,8 +1268,9 @@ Lit LookaheadSplitting::pickBranchLiteral(vec* > **valid) } sizeNegativeLookahead = trail.size() - initTrailSize; for (int j = initTrailSize; j < trail.size(); j++) { - sizeWatcherNegativeLookahead += sign(trail[j]) ? watcherNegLitSize[bestKList[i]] : watcherPosLitSize[bestKList[i]]; - binClauseNegativeLookahead += sign(trail[j]) ? numPosLitTerClause[var(trail[j])] : numNegLitTerClause[var(trail[j])]; + const Var v = var(trail[j]); + sizeWatcherNegativeLookahead += sign(trail[j]) ? watcherNegLitSize[v] : watcherPosLitSize[v]; + binClauseNegativeLookahead += sign(trail[j]) ? numPosLitTerClause[v] : numNegLitTerClause[v]; } //check if to perform double lookahead if (opt_double_lookahead) { From 797ae6a5e9e7a9f5139e3421ccec5c05a2e80d52 Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Tue, 20 Feb 2018 22:51:32 +0100 Subject: [PATCH 05/13] splitting: only compute score for candidates If there are no candidate literals to compute a score for, stop the computation, and skip. --- pcasso-src/LookaheadSplitting.cc | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/pcasso-src/LookaheadSplitting.cc b/pcasso-src/LookaheadSplitting.cc index 73beb0d..b400e03 100644 --- a/pcasso-src/LookaheadSplitting.cc +++ b/pcasso-src/LookaheadSplitting.cc @@ -1427,10 +1427,12 @@ Lit LookaheadSplitting::pickBranchLiteral(vec* > **valid) jump: cancelUntil(decLev); - for (int i = 0; i < score.size(); i++) { - if (score[i] > 0 && score[i] > bestVarScore && value(bestKList[i]) == l_Undef) { - bestVarScore = score[i]; - bestVarIndex = i; + if (bestKList.size() > 0) { + for (int i = 0; i < score.size(); i++) { + if (score[i] > 0 && score[i] > bestVarScore && value(bestKList[i]) == l_Undef) { + bestVarScore = score[i]; + bestVarIndex = i; + } } } From 892cf063c050034263db4e28f3d299c0d9119e83 Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Tue, 20 Feb 2018 22:52:37 +0100 Subject: [PATCH 06/13] splitting: handle no-split case The split variable next has to be initialized, such that in case of failures during computing the candidates, e.g. due to too small formulas, there lit_Undef value can still be returned. Consequently, make sure nobody consumes lit_Undef as an index. --- pcasso-src/LookaheadSplitting.cc | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/pcasso-src/LookaheadSplitting.cc b/pcasso-src/LookaheadSplitting.cc index b400e03..c946b48 100644 --- a/pcasso-src/LookaheadSplitting.cc +++ b/pcasso-src/LookaheadSplitting.cc @@ -337,6 +337,8 @@ lbool LookaheadSplitting::produceSplitting(vec* >* > **splits, vec< } else if (next == lit_Undef) { if (checkSolution()) { return l_True; + } else { + assert(false && "this case should be handled, a split is required"); } } @@ -509,6 +511,8 @@ lbool LookaheadSplitting::produceSplitting(vec* >* > **splits, vec< if (next == lit_Undef) { if (checkSolution()) { return l_True; + } else { + assert(false && "this case should be handled, a split is required"); } } if (decisionLevel() == 0 && splitting->size() == 0) { @@ -1449,7 +1453,7 @@ Lit LookaheadSplitting::pickBranchLiteral(vec* > **valid) } } - Lit next; + Lit next = lit_Undef; if (bestVarIndex != var_Undef) { bool pol = false; @@ -1583,7 +1587,7 @@ Lit LookaheadSplitting::pickBranchLiteral(vec* > **valid) *///if(opt_var_eq>0) //fprintf(stderr, "splitter: Var Equivalence \t\t\t = %d \n", varEq.size()/2); //fprintf(stderr, "splitter: Best Var Index = %d\n",bestVarIndex); - if (opt_tabu) { + if (opt_tabu && next != lit_Undef) { tabuList[var(next)] = true; } From 10133b0515656d8f8ab3913abbe6a23598972ebf Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Tue, 20 Feb 2018 22:54:17 +0100 Subject: [PATCH 07/13] master: allow getting stuck more often As getting stuck might be due to a race condition, allow the solver to see this condition more often before actually aborting the search. On the other hand, make sure we assert before exit, so that debugging would be doable, and the problem can be identified during fuzzing. --- pcasso-src/Master.cc | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/pcasso-src/Master.cc b/pcasso-src/Master.cc index 1008f5e..a83aa35 100644 --- a/pcasso-src/Master.cc +++ b/pcasso-src/Master.cc @@ -196,6 +196,7 @@ int Master::run() // check the state of the tree // solve the next node in the tree if (MSverbosity > 0) { fprintf(stderr, "M: start main loop\n"); } + int stuck = 0; while (!done) { int idles = 0; // important, because this indicates that there can be done more in the next round! @@ -371,7 +372,13 @@ int Master::run() for (; i < threads; ++i) { if (threadData[i].s == splitting) { break; } // TODO SHOULDN'T BE IDLE ?? DAVIDE> if (threadData[i].s == working) { break; } // do not stop if some worker is doing something + if (threadData[i].s == unclean) { break; } // do not stop if some worker is not cleaned up yet } + + // allow the solver 16 times reaching this before we actually stop working + stuck ++; + if (stuck < 16) { continue; } + // if there is a thread that is still doing something, we did not run out of work! if (i == threads) { fprintf(stderr, "\n***\n*** RUN OUT OF WORK - return unknown?\n***\n\n"); @@ -384,7 +391,9 @@ int Master::run() else if (threadData[i].s == unclean) { uncleans++; } } - fprintf(stderr, "c idle: %d working: %d splitting: %d unclean: %d\n", idles, workers, splitters, uncleans); + fprintf(stderr, "c (after %d iterations): idle: %d working: %d splitting: %d unclean: %d\n", stuck, idles, workers, splitters, uncleans); + // for debugging purposes, stop here. we assume, there is a solution but nobody told us, so let's check + assert(false && "this should not be reached"); exit(0); } From 1c1cbc364824721f264ec6a4100981a28184d3c4 Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Tue, 20 Feb 2018 22:55:19 +0100 Subject: [PATCH 08/13] master: do not blindly set to unknown When multiple slaves work on the same node, make sure they do not overwrite the state of each other. Only set a state to unknown, if the node actually has an unknown state. --- pcasso-src/Master.cc | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/pcasso-src/Master.cc b/pcasso-src/Master.cc index a83aa35..a80b86a 100644 --- a/pcasso-src/Master.cc +++ b/pcasso-src/Master.cc @@ -880,7 +880,7 @@ Master::solveInstance(void* data) } else { // result of solver is "unknown" if (master.plainpart) { tData.nodeToSolve->setState(TreeNode::retry); } - else { tData.nodeToSolve->setState(TreeNode::unknown); } + else { if (tData.nodeToSolve->getState() == TreeNode::retry) tData.nodeToSolve->setState(TreeNode::unknown); } if (keepToplevelUnits > 0) { int toplevelVariables = 0; @@ -942,7 +942,7 @@ Master::splitInstance(void* data) if (Portfolio && tData.nodeToSolve->getLevel() < PortfolioLevel) { // perform portfolio only until this level! master.lock(); // ********************* START CRITICAL *********************** childConstraints.push_back(new vector*>); - tData.nodeToSolve->setState(TreeNode::unknown); + if (tData.nodeToSolve->getState() == TreeNode::retry) { tData.nodeToSolve->setState(TreeNode::unknown); } // only modify, if it's retry tData.nodeToSolve->expand(childConstraints); master.addNode(tData.nodeToSolve->getChild(0)); tData.result = ret; @@ -1149,7 +1149,7 @@ Master::splitInstance(void* data) // shut down all threads that are running below that node (necessary?) } else { // simply set the node to the unknown state - tData.nodeToSolve->setState(TreeNode::unknown); + if (tData.nodeToSolve->getState() == TreeNode::retry) { tData.nodeToSolve->setState(TreeNode::unknown); } for (unsigned int i = 0; i < validConstraints.size(); i++) { tData.nodeToSolve->addNodeConstraint(validConstraints[i]); } From 3abccb42da8238bac4245a18825921329fa1d7f6 Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Tue, 20 Feb 2018 22:58:59 +0100 Subject: [PATCH 09/13] master: always write unsat result Currently, the stopUnsatChilds option had to be set to write the unsat state for a node. However, the state should always be written. Hence, the check for the option is moved closer to actually running the related algorithm. --- pcasso-src/Master.cc | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/pcasso-src/Master.cc b/pcasso-src/Master.cc index a80b86a..1648520 100644 --- a/pcasso-src/Master.cc +++ b/pcasso-src/Master.cc @@ -209,12 +209,15 @@ int Master::run() if (threadData[i].s == unclean) { // Davide> Free memory - if (threadData[i].result == 20 && stopUnsatChilds) { + if (threadData[i].result == 20) { // The children are NOT running, so I can delete every pool lock(); threadData[i].nodeToSolve->setState(TreeNode::unsat, true); + // fprintf(stderr, "c root node state: %d\n", root.getState()); unlock(); - killUnsatChildren(i); + if (stopUnsatChilds) { + killUnsatChildren(i); + } } uncleans++; From a21fc3433deac2e1a2e04f31c26cbb63fc70136d Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Fri, 16 Feb 2018 00:34:01 +0100 Subject: [PATCH 10/13] pcasso: clear clauses to share before reduceDB In the reduceDB, new clauses are added to the clauses to be shared, but no clauses are removed. This way, faulty pointers might be used, as the clauses that are shared might become invalid, or wrong indexes are used. --- pcasso-src/SolverPT.cc | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/pcasso-src/SolverPT.cc b/pcasso-src/SolverPT.cc index da8b0fb..d846631 100644 --- a/pcasso-src/SolverPT.cc +++ b/pcasso-src/SolverPT.cc @@ -1779,6 +1779,10 @@ void SolverPT::reduceDB() int limit = learnts.size() / 2; + for (int i = 0; i < learnts_indeces.size(); ++i) { + learnts_indeces[i].clear(); + } + for (i = j = 0; i < learnts.size(); i++) { Clause& c = ca[learnts[i]]; //assert(c.getPTLevel() Date: Fri, 9 Mar 2018 16:46:46 +0100 Subject: [PATCH 11/13] levelpool: inisist on more restrictions --- pcasso-src/LevelPool.cc | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/pcasso-src/LevelPool.cc b/pcasso-src/LevelPool.cc index 94a5ed2..5bcc8af 100644 --- a/pcasso-src/LevelPool.cc +++ b/pcasso-src/LevelPool.cc @@ -29,6 +29,9 @@ bool LevelPool::add_shared(vec& lits, unsigned int nodeID, bool disable_dup temp[0] = toLit(nodeID); + assert(toInt(temp[0]) >= 0 && "the number to identify the node should be positive"); + assert(writeP == 0 || shared_clauses[writeP-1] == lit_Undef); // the pointer should point at the end of a clause + assert(temp.size() < shared_clauses.size()); if (writeP + temp.size() < shared_clauses.size() - 2) { // Space for the ending lit_Undef @@ -38,7 +41,7 @@ bool LevelPool::add_shared(vec& lits, unsigned int nodeID, bool disable_dup writeP += temp.size(); int k = writeP; ++writeP; - while (shared_clauses[k] != lit_Undef) { + while (shared_clauses[k] != lit_Undef && k < endP) { // clean the whole vector, or until the next end of a clause shared_clauses[k++] = lit_Undef; } if (writeP > endP) { endP = writeP; } @@ -54,7 +57,7 @@ bool LevelPool::add_shared(vec& lits, unsigned int nodeID, bool disable_dup } int k = writeP; ++writeP; - while (shared_clauses[k] != lit_Undef) { + while (shared_clauses[k] != lit_Undef && k < endP) { shared_clauses[k++] = lit_Undef; } assert(endP > writeP); @@ -68,10 +71,11 @@ LevelPool::getChunk(int readP, vec& chunk) if (readP >= endP) { return; } - if (((readP != 0 && shared_clauses[readP - 1] == lit_Undef) || readP == 0)) { + if (( (readP != 0 && shared_clauses[readP - 1] == lit_Undef) || readP == 0)) { if (readP <= writeP) { chunk.growTo(writeP - readP); int j = 0; + assert(readP == 0 || toInt(shared_clauses[readP]) >= 0); // the first literal indicates the ID of the node that shared the clause for (int i = readP; i < writeP; ++i) { assert(writeP - readP == chunk.size()); assert(j < chunk.size()); @@ -82,6 +86,7 @@ LevelPool::getChunk(int readP, vec& chunk) } else { chunk.growTo((endP - readP) + writeP); int j = 0; + assert(readP == 0 || toInt(shared_clauses[readP]) >= 0); // the first literal indicates the ID of the node that shared the clause for (int i = readP; i < endP; ++i) { assert(j < chunk.size()); chunk[j++] = shared_clauses[i]; @@ -96,6 +101,7 @@ LevelPool::getChunk(int readP, vec& chunk) } else { chunk.growTo(writeP); int j = 0; + assert(writeP == 0 || toInt(shared_clauses[0]) > 0); // the first literal indicates the ID of the node that shared the clause for (int i = 0; i < writeP; ++i) { assert(j < chunk.size()); chunk[j++] = shared_clauses[i]; From b6262a055cc810bd8febf28b1bde04da493e7c2e Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Fri, 9 Mar 2018 16:52:18 +0100 Subject: [PATCH 12/13] solverpt: do not share eagerly When we know a level does not have clauses to share, do not lock the level, but instead skip the level right away. --- pcasso-src/SolverPT.cc | 1 + 1 file changed, 1 insertion(+) diff --git a/pcasso-src/SolverPT.cc b/pcasso-src/SolverPT.cc index d846631..400401e 100644 --- a/pcasso-src/SolverPT.cc +++ b/pcasso-src/SolverPT.cc @@ -1437,6 +1437,7 @@ void SolverPT::push_learnts() vec c_lits; for (unsigned int i = 0; i < learnts_indeces.size(); i++) { + if(learnts_indeces[i].size() == 0) continue; // nothing to share for this level, skip it! davide::LevelPool* pool = previous_pools[i]; if (pool == 0) { continue; } From b05be71be784d4f44debd6b811d6f3324bb08e25 Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Fri, 6 Mar 2020 23:12:39 +0100 Subject: [PATCH 13/13] solverpt: assertions and volatile --- pcasso-src/SolverPT.cc | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/pcasso-src/SolverPT.cc b/pcasso-src/SolverPT.cc index 400401e..6a1b5f1 100644 --- a/pcasso-src/SolverPT.cc +++ b/pcasso-src/SolverPT.cc @@ -1466,6 +1466,7 @@ void SolverPT::push_learnts() } + assert(c.getPTLevel() >= i && "cannot share clause more upwards than its PT level allows"); sharedSuccess = pool->add_shared(c_lits, tnode->id(), disable_dupl_removal, disable_dupl_check); fullPool = pool->isFull(); @@ -1552,7 +1553,7 @@ void SolverPT::pull_learnts(int curr_restarts) } pool->levelPoolLock.rLock(); // Davide> START CRITICAL } - int readP = shared_indeces[i]; + volatile int readP = shared_indeces[i]; pool->getChunk(readP, chunk);