Target Phase (non-inverted) + Luby restarts + glues

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;
+    }
 };
 
 

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;

src/smtsolvers/CoreSMTSolver.cc

@@ -229,13 +229,15 @@ 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);
     decision .push();
     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<Lit>& 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<Lit>&) (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<Lit>& out_learnt, int& out_btlevel)
+void CoreSMTSolver::analyze(CRef confl, vec<Lit>& 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<Lit>& 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,14 +1483,29 @@ 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++;
             if (decisionLevel() == 0) {
                 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;

src/smtsolvers/CoreSMTSolver.h

@@ -319,6 +319,10 @@ class CoreSMTSolver
     double              var_inc;          // Amount to bump next variable with.
     OccLists<Lit, vec<Watcher>, WatcherDeleted>  watches;          // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
     vec<lbool>          assigns;          // The current assignments (lbool:s stored as char:s).
+    vec<bool>           saved_polar;
+    int                 longest_trail = 0;
+    int longest_flip = 0;;
+    int myinv = 0;
     vec<bool>           var_seen;
     vec<char>           polarity;         // The preferred polarity of each variable.
     vec<char>           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<Lit>& out_learnt, int& out_btlevel);    // (bt = backtrack)
+    void     analyze          (CRef confl, vec<Lit>& out_learnt, int& out_btlevel, uint32_t& oug_glue);    // (bt = backtrack)
+    uint32_t calc_glue(const vec<Lit>& ps);
+    uint64_t MYFLAG = 0;
+    vec<uint64_t> permDiff;
     void     analyzeFinal     (Lit p, vec<Lit>& 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

src/smtsolvers/LookaheadSMTSolver.cc

@@ -84,7 +84,8 @@ lbool LookaheadSMTSolver::laPropagateWrapper() {
 
             vec<Lit> 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);

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<LitLev>& deductions)
     }
 #endif
     return;
-}
+}