diff --git a/src/minisat/core/SolverTypes.h b/src/minisat/core/SolverTypes.h index de38262e6..55befe991 100644 --- a/src/minisat/core/SolverTypes.h +++ b/src/minisat/core/SolverTypes.h @@ -140,7 +140,8 @@ class Clause { unsigned learnt : 1; unsigned has_extra : 1; unsigned reloced : 1; - unsigned size : 27; } header; + unsigned glue : 4; + unsigned size : 23; } header; union { Lit lit; float act; uint32_t abs; CRef rel; } data[0]; friend class ClauseAllocator; @@ -153,6 +154,7 @@ class Clause { header.has_extra = use_extra; header.reloced = 0; header.size = ps.size(); + header.glue = 15; for (unsigned i = 0; i < (unsigned)ps.size(); i++) data[i].lit = ps[i]; @@ -197,6 +199,13 @@ class Clause { Lit subsumes (const Clause& other) const; void strengthen (Lit p); + uint32_t getglue() const { + return header.glue; + } + void setglue(const uint32_t glue) { + assert(glue < 16); + header.glue = glue; + } }; diff --git a/src/options/SMTConfig.cc b/src/options/SMTConfig.cc index 23dfecdfe..90c1ea1d1 100644 --- a/src/options/SMTConfig.cc +++ b/src/options/SMTConfig.cc @@ -554,7 +554,7 @@ SMTConfig::initializeConfig( ) sat_polarity_mode = 0; sat_initial_skip_step = 1; sat_skip_step_factor = 1; - sat_use_luby_restart = 0; + sat_use_luby_restart = 1; sat_learn_up_to_size = 0; sat_temporary_learn = 1; sat_preprocess_booleans = 1; diff --git a/src/smtsolvers/CoreSMTSolver.cc b/src/smtsolvers/CoreSMTSolver.cc index 847e2b7eb..af1967d8b 100644 --- a/src/smtsolvers/CoreSMTSolver.cc +++ b/src/smtsolvers/CoreSMTSolver.cc @@ -229,6 +229,7 @@ Var CoreSMTSolver::newVar(bool sign, bool dvar) watches .init(mkLit(v, true)); assigns .push(l_Undef); vardata .push(mkVarData(CRef_Undef, 0)); + permDiff.push(0); activity .push(rnd_init_act ? drand(random_seed) * 0.00001 : 0); seen .push(0); polarity .push(sign); @@ -236,6 +237,7 @@ Var CoreSMTSolver::newVar(bool sign, bool dvar) trail .capacity(v+1); setDecisionVar(v, dvar); polarity .push((char)sign); + saved_polar.push(true); #if CACHE_POLARITY prev_polarity.push(toInt(l_Undef)); @@ -406,6 +408,12 @@ void CoreSMTSolver::cancelUntil(int level) { if (decisionLevel() > level) { + if (trail.size() > longest_trail) { + for (auto p : trail) { + saved_polar[var(p)] = not sign(p); + } + longest_trail = trail.size(); + } for (int c = trail.size()-1; c >= trail_lim[level]; c--) { Var x = var(trail[c]); @@ -568,22 +576,8 @@ Lit CoreSMTSolver::choosePolarity(Var next) { return mkLit(next, sign); } } - switch ( polarity_mode ) { - case polarity_true: - sign = false; - break; - case polarity_false: - sign = true; - break; - case polarity_user: - sign = polarity[next]; - break; - case polarity_rnd: - sign = irand(random_seed, 2); - break; - default: - assert(false); - } + sign = false; + sign = not saved_polar[next] ^ myinv; return mkLit(next, sign); } @@ -608,6 +602,23 @@ Lit CoreSMTSolver::pickBranchLit() } +uint32_t CoreSMTSolver::calc_glue(const vec& ps) +{ + MYFLAG++; + uint32_t nblevels = 0; + for (Lit lit: ps) { + int l = vardata[var(lit)].level; + if (l != 0 && permDiff[l] != MYFLAG) { + permDiff[l] = MYFLAG; + nblevels++; + if (nblevels >= 10) { + return nblevels; + } + } + } + return nblevels; +} + /*_________________________________________________________________________________________________ | | analyze : (confl : CRef) (out_learnt : vec&) (out_btlevel : int&) -> [void] @@ -626,7 +637,7 @@ Lit CoreSMTSolver::pickBranchLit() | Will undo part of the trail, upto but not beyond the assumption of the current decision level. |________________________________________________________________________________________________@*/ -void CoreSMTSolver::analyze(CRef confl, vec& out_learnt, int& out_btlevel) +void CoreSMTSolver::analyze(CRef confl, vec& out_learnt, int& out_btlevel, uint32_t& out_glue) { bool logsProofForInterpolation = this->logsProofForInterpolation(); assert(!logsProofForInterpolation || !proof->hasOpenChain()); @@ -813,6 +824,7 @@ void CoreSMTSolver::analyze(CRef confl, vec& out_learnt, int& out_btlevel) max_literals += out_learnt.size(); out_learnt.shrink(i - j); tot_literals += out_learnt.size(); + out_glue = calc_glue(out_learnt); // Find correct backtrack level: // @@ -1202,13 +1214,19 @@ void CoreSMTSolver::reduceDB() sort(learnts, reduceDB_lt(ca)); // Don't delete binary or locked clauses. From the rest, delete clauses from the first half // and clauses with activity smaller than 'extra_lim': + int extra = 0; for (i = j = 0; i < learnts.size(); i++) { Clause& c = ca[learnts[i]]; - if (c.size() > 2 && !locked(c) && (i < learnts.size() / 2 || c.activity() < extra_lim)) +// std::cout << "c.glue: " << c.getglue() << std::endl; + if (c.getglue() <= 3) { + extra++; + } + if (c.getglue() > 3 && c.size() > 2 && !locked(c) && (i+extra < learnts.size() / 2)) { removeClause(learnts[i]); - else + }else{ learnts[j++] = learnts[i]; + } } learnts.shrink(i - j); checkGarbage(); @@ -1416,7 +1434,7 @@ void CoreSMTSolver::learntSizeAdjust() { | all variables are decision variables, this means that the clause set is satisfiable. 'l_False' | if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached. |________________________________________________________________________________________________@*/ -lbool CoreSMTSolver::search(int nof_conflicts, int nof_learnts) +lbool CoreSMTSolver::search(int nof_conflicts) { // Time my executionto search_timer // opensmt::StopWatch stopwatch = opensmt::StopWatch(search_timer); @@ -1465,6 +1483,20 @@ lbool CoreSMTSolver::search(int nof_conflicts, int nof_learnts) CRef confl = propagate(); if (confl != CRef_Undef) { + + if (conflicts > longest_flip) { + myinv ^= 1; + if (myinv == 1) { + longest_flip+=1000; + } else { + longest_flip+=10000; + } + + if (myinv == 0) { +// longest_trail = 0; + } + } + // CONFLICT conflicts++; conflictC++; @@ -1472,7 +1504,8 @@ lbool CoreSMTSolver::search(int nof_conflicts, int nof_learnts) return zeroLevelConflictHandler(); } learnt_clause.clear(); - analyze(confl, learnt_clause, backtrack_level); + uint32_t glue; + analyze(confl, learnt_clause, backtrack_level, glue); cancelUntil(backtrack_level); @@ -1482,6 +1515,7 @@ lbool CoreSMTSolver::search(int nof_conflicts, int nof_learnts) CRef reason = CRef_Undef; if (logsProofForInterpolation()) { CRef cr = ca.alloc(learnt_clause, false); + ca[cr].setglue(glue); proof->endChain(cr); reason = cr; } @@ -1492,6 +1526,7 @@ lbool CoreSMTSolver::search(int nof_conflicts, int nof_learnts) all_learnts ++; CRef cr = ca.alloc(learnt_clause, true); + ca[cr].setglue(glue); if (logsProofForInterpolation()) { proof->endChain(cr); @@ -1522,9 +1557,10 @@ lbool CoreSMTSolver::search(int nof_conflicts, int nof_learnts) // Two ways of reducing the clause. The latter one seems to be working // better (not running proper tests since the cluster is down...) // if ((learnts.size()-nAssigns()) >= max_learnts) - if (nof_learnts >= 0 && learnts.size()-nAssigns() >= nof_learnts) { + if (nof_learnts >= 0 && learnts.size() >= nof_learnts) { // Reduce the set of learnt clauses: reduceDB(); + nof_learnts *= 1.1; } // Early Pruning Call @@ -1739,7 +1775,7 @@ lbool CoreSMTSolver::solve_() solves++; double nof_conflicts = restart_first; - double nof_learnts = nClauses() * learntsize_factor; + //double nof_learnts = nClauses() * learntsize_factor; max_learnts = nClauses() * learntsize_factor; learntsize_adjust_confl = learntsize_adjust_start_confl; learntsize_adjust_cnt = (int)learntsize_adjust_confl; @@ -1779,15 +1815,15 @@ lbool CoreSMTSolver::solve_() } // XXX - status = search((int)nof_conflicts, (int)nof_learnts); + status = search((int)nof_conflicts); nof_conflicts = restartNextLimit(nof_conflicts); if (config.sat_use_luby_restart) { if (last_luby_k != luby_k) { - nof_learnts *= 1.215; +// nof_learnts *= learntsize_inc;//1.215; } last_luby_k = luby_k; } else { - nof_learnts *= learntsize_inc; +// nof_learnts *= learntsize_inc; } } @@ -1898,7 +1934,7 @@ int CoreSMTSolver::restartNextLimit ( int nof_conflicts ) else luby_previous.push_back( luby_previous[luby_i - (1 << (luby_k - 1))]); - return luby_previous.back() * restart_first; + return luby_previous.back() * 120; } // Standard restart return nof_conflicts * restart_inc; diff --git a/src/smtsolvers/CoreSMTSolver.h b/src/smtsolvers/CoreSMTSolver.h index 7bbf691b4..71761b0b0 100644 --- a/src/smtsolvers/CoreSMTSolver.h +++ b/src/smtsolvers/CoreSMTSolver.h @@ -319,6 +319,10 @@ class CoreSMTSolver double var_inc; // Amount to bump next variable with. OccLists, WatcherDeleted> watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). vec assigns; // The current assignments (lbool:s stored as char:s). + vec saved_polar; + int longest_trail = 0; + int longest_flip = 0;; + int myinv = 0; vec var_seen; vec polarity; // The preferred polarity of each variable. vec decision; // Declares if a variable is eligible for selection in the decision heuristic. @@ -381,10 +385,14 @@ class CoreSMTSolver bool enqueue (Lit p, CRef from = CRef_Undef); // Test if fact 'p' contradicts current state, enqueue otherwise. CRef propagate (); // Perform unit propagation. Returns possibly conflicting clause. virtual void cancelUntil (int level); // Backtrack until a certain level. - void analyze (CRef confl, vec& out_learnt, int& out_btlevel); // (bt = backtrack) + void analyze (CRef confl, vec& out_learnt, int& out_btlevel, uint32_t& oug_glue); // (bt = backtrack) + uint32_t calc_glue(const vec& ps); + uint64_t MYFLAG = 0; + vec permDiff; void analyzeFinal (Lit p, vec& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION? bool litRedundant (Lit p, uint32_t abstract_levels); // (helper method for 'analyze()') - lbool search (int nof_conflicts, int nof_learnts); // Search for a given number of conflicts. + lbool search (int nof_conflicts); // Search for a given number of conflicts. + int nof_learnts = 40000; virtual bool okContinue () const; // Check search termination conditions virtual ConsistencyAction notifyConsistency() { return ConsistencyAction::NoOp; } // Called when the search has reached a consistent point virtual void notifyEnd() { } // Called at the end of the search loop diff --git a/src/smtsolvers/LookaheadSMTSolver.cc b/src/smtsolvers/LookaheadSMTSolver.cc index d55a1b4a7..25a4bf561 100644 --- a/src/smtsolvers/LookaheadSMTSolver.cc +++ b/src/smtsolvers/LookaheadSMTSolver.cc @@ -84,7 +84,8 @@ lbool LookaheadSMTSolver::laPropagateWrapper() { vec out_learnt; int out_btlevel; - analyze(cr, out_learnt, out_btlevel); + uint32_t glue; + analyze(cr, out_learnt, out_btlevel, glue); #ifdef LADEBUG printf("Conflict: I would need to backtrack from %d to %d\n", decisionLevel(), out_btlevel); #endif @@ -94,6 +95,7 @@ lbool LookaheadSMTSolver::laPropagateWrapper() { uncheckedEnqueue(out_learnt[0]); } else { CRef crd = ca.alloc(out_learnt, true); + ca[crd].setglue(glue); learnts.push(crd); attachClause(crd); uncheckedEnqueue(out_learnt[0], crd); diff --git a/src/smtsolvers/TheoryIF.cc b/src/smtsolvers/TheoryIF.cc index ea106a1f2..230d2c068 100644 --- a/src/smtsolvers/TheoryIF.cc +++ b/src/smtsolvers/TheoryIF.cc @@ -299,7 +299,8 @@ CoreSMTSolver::handleUnsat() if (logsProofForInterpolation()) { proof->newTheoryClause(confl); } - analyze( confl, learnt_clause, backtrack_level ); + uint32_t glue; + analyze( confl, learnt_clause, backtrack_level, glue); if (!logsProofForInterpolation()) { // Get rid of the temporary lemma @@ -327,6 +328,7 @@ CoreSMTSolver::handleUnsat() all_learnts ++; CRef cr = ca.alloc(learnt_clause, true); + ca[cr].setglue(glue); if (logsProofForInterpolation()) { proof->endChain(cr); @@ -417,4 +419,4 @@ void CoreSMTSolver::deduceTheory(vec& deductions) } #endif return; -} \ No newline at end of file +}