From 879f57ac2ed6e8bc4dd8de64177857a03b1b6e1d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antti=20Hyv=C3=A4rinen?= Date: Mon, 4 Apr 2022 22:32:15 +0200 Subject: [PATCH 1/7] CoreSMTSolver: sticky polarities --- src/smtsolvers/CoreSMTSolver.cc | 10 +++++++++- src/smtsolvers/CoreSMTSolver.h | 2 ++ 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/src/smtsolvers/CoreSMTSolver.cc b/src/smtsolvers/CoreSMTSolver.cc index 847e2b7eb..40433814a 100644 --- a/src/smtsolvers/CoreSMTSolver.cc +++ b/src/smtsolvers/CoreSMTSolver.cc @@ -236,6 +236,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 +407,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]); @@ -570,7 +577,8 @@ Lit CoreSMTSolver::choosePolarity(Var next) { } switch ( polarity_mode ) { case polarity_true: - sign = false; +// sign = false; + sign = saved_polar[next]; break; case polarity_false: sign = true; diff --git a/src/smtsolvers/CoreSMTSolver.h b/src/smtsolvers/CoreSMTSolver.h index 7bbf691b4..b092b5f0d 100644 --- a/src/smtsolvers/CoreSMTSolver.h +++ b/src/smtsolvers/CoreSMTSolver.h @@ -319,6 +319,8 @@ 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; 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. From 6c94cb6261db7fd929ec88a96211067e4683f8c9 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Tue, 5 Apr 2022 09:59:40 +0200 Subject: [PATCH 2/7] Adding LBD+luby+target phases --- src/minisat/core/SolverTypes.h | 1 + src/options/SMTConfig.cc | 2 +- src/smtsolvers/CoreSMTSolver.cc | 49 +++++++++++++++++----------- src/smtsolvers/CoreSMTSolver.h | 5 ++- src/smtsolvers/LookaheadSMTSolver.cc | 4 ++- src/smtsolvers/TheoryIF.cc | 6 ++-- 6 files changed, 43 insertions(+), 24 deletions(-) diff --git a/src/minisat/core/SolverTypes.h b/src/minisat/core/SolverTypes.h index de38262e6..48d238349 100644 --- a/src/minisat/core/SolverTypes.h +++ b/src/minisat/core/SolverTypes.h @@ -165,6 +165,7 @@ class Clause { } public: + uint32_t glue; void calcAbstraction() { assert(header.has_extra); uint32_t abstraction = 0; 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 40433814a..9a954f5b5 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); @@ -575,23 +576,8 @@ Lit CoreSMTSolver::choosePolarity(Var next) { return mkLit(next, sign); } } - switch ( polarity_mode ) { - case polarity_true: -// sign = false; - sign = saved_polar[next]; - 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]; return mkLit(next, sign); } @@ -616,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 >= 1000) { + return nblevels; + } + } + } + return nblevels; +} + /*_________________________________________________________________________________________________ | | analyze : (confl : CRef) (out_learnt : vec&) (out_btlevel : int&) -> [void] @@ -634,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()); @@ -821,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: // @@ -1199,6 +1203,10 @@ struct reduceDB_lt reduceDB_lt(ClauseAllocator& ca_) : ca(ca_) {} bool operator () (CRef x, CRef y) { + if (ca[x].glue <= 3 && ca[x].glue > 3) return true; + if (ca[x].glue > 3 && ca[x].glue <= 3) return false; + if (ca[x].glue <= 3 && ca[x].glue <= 3) return false; + return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); } }; @@ -1426,6 +1434,7 @@ void CoreSMTSolver::learntSizeAdjust() { |________________________________________________________________________________________________@*/ lbool CoreSMTSolver::search(int nof_conflicts, int nof_learnts) { + std::cout << "Starting search conflicts: " << conflicts << " will go: " << nof_conflicts << std::endl; // Time my executionto search_timer // opensmt::StopWatch stopwatch = opensmt::StopWatch(search_timer); #ifdef VERBOSE_SAT @@ -1480,7 +1489,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); @@ -1500,6 +1510,7 @@ lbool CoreSMTSolver::search(int nof_conflicts, int nof_learnts) all_learnts ++; CRef cr = ca.alloc(learnt_clause, true); + ca[cr].glue = glue; if (logsProofForInterpolation()) { proof->endChain(cr); diff --git a/src/smtsolvers/CoreSMTSolver.h b/src/smtsolvers/CoreSMTSolver.h index b092b5f0d..a231ef6a1 100644 --- a/src/smtsolvers/CoreSMTSolver.h +++ b/src/smtsolvers/CoreSMTSolver.h @@ -383,7 +383,10 @@ 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. diff --git a/src/smtsolvers/LookaheadSMTSolver.cc b/src/smtsolvers/LookaheadSMTSolver.cc index d55a1b4a7..3e208ed26 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].glue = 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..e53e91f6f 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].glue = glue; if (logsProofForInterpolation()) { proof->endChain(cr); @@ -417,4 +419,4 @@ void CoreSMTSolver::deduceTheory(vec& deductions) } #endif return; -} \ No newline at end of file +} From 66023e67f6ce87afea527d9d2589447b47c88a75 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Tue, 5 Apr 2022 10:44:36 +0200 Subject: [PATCH 3/7] Better glue usage --- src/smtsolvers/CoreSMTSolver.cc | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/src/smtsolvers/CoreSMTSolver.cc b/src/smtsolvers/CoreSMTSolver.cc index 9a954f5b5..74f62d0c2 100644 --- a/src/smtsolvers/CoreSMTSolver.cc +++ b/src/smtsolvers/CoreSMTSolver.cc @@ -1203,10 +1203,6 @@ struct reduceDB_lt reduceDB_lt(ClauseAllocator& ca_) : ca(ca_) {} bool operator () (CRef x, CRef y) { - if (ca[x].glue <= 3 && ca[x].glue > 3) return true; - if (ca[x].glue > 3 && ca[x].glue <= 3) return false; - if (ca[x].glue <= 3 && ca[x].glue <= 3) return false; - return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); } }; @@ -1221,7 +1217,8 @@ void CoreSMTSolver::reduceDB() 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.glue << std::endl; + if (c.glue > 3 && c.size() > 2 && !locked(c) && (i < learnts.size() / 2 || c.activity() < extra_lim)) removeClause(learnts[i]); else learnts[j++] = learnts[i]; From ceb70f4a1a2f77cb0c33e6789dc5839f1529dc8d Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Tue, 5 Apr 2022 10:47:15 +0200 Subject: [PATCH 4/7] Removing debug code --- src/smtsolvers/CoreSMTSolver.cc | 1 - 1 file changed, 1 deletion(-) diff --git a/src/smtsolvers/CoreSMTSolver.cc b/src/smtsolvers/CoreSMTSolver.cc index 74f62d0c2..6772a4774 100644 --- a/src/smtsolvers/CoreSMTSolver.cc +++ b/src/smtsolvers/CoreSMTSolver.cc @@ -1217,7 +1217,6 @@ void CoreSMTSolver::reduceDB() for (i = j = 0; i < learnts.size(); i++) { Clause& c = ca[learnts[i]]; - std::cout << "c.glue: " << c.glue << std::endl; if (c.glue > 3 && c.size() > 2 && !locked(c) && (i < learnts.size() / 2 || c.activity() < extra_lim)) removeClause(learnts[i]); else From fd9288a0ef351d1dd1d292d5a44c6189832ae64e Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Tue, 5 Apr 2022 11:10:13 +0200 Subject: [PATCH 5/7] Don't use more memory for glues --- src/minisat/core/SolverTypes.h | 11 +++++++++-- src/smtsolvers/CoreSMTSolver.cc | 9 +++++---- src/smtsolvers/LookaheadSMTSolver.cc | 2 +- src/smtsolvers/TheoryIF.cc | 2 +- 4 files changed, 16 insertions(+), 8 deletions(-) diff --git a/src/minisat/core/SolverTypes.h b/src/minisat/core/SolverTypes.h index 48d238349..440462472 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; @@ -165,7 +166,6 @@ class Clause { } public: - uint32_t glue; void calcAbstraction() { assert(header.has_extra); uint32_t abstraction = 0; @@ -198,6 +198,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/smtsolvers/CoreSMTSolver.cc b/src/smtsolvers/CoreSMTSolver.cc index 6772a4774..fe378e165 100644 --- a/src/smtsolvers/CoreSMTSolver.cc +++ b/src/smtsolvers/CoreSMTSolver.cc @@ -611,7 +611,7 @@ uint32_t CoreSMTSolver::calc_glue(const vec& ps) if (l != 0 && permDiff[l] != MYFLAG) { permDiff[l] = MYFLAG; nblevels++; - if (nblevels >= 1000) { + if (nblevels >= 10) { return nblevels; } } @@ -1217,7 +1217,8 @@ void CoreSMTSolver::reduceDB() for (i = j = 0; i < learnts.size(); i++) { Clause& c = ca[learnts[i]]; - if (c.glue > 3 && 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 && c.size() > 2 && !locked(c) && (i < learnts.size() / 2 || c.activity() < extra_lim)) removeClause(learnts[i]); else learnts[j++] = learnts[i]; @@ -1430,7 +1431,7 @@ void CoreSMTSolver::learntSizeAdjust() { |________________________________________________________________________________________________@*/ lbool CoreSMTSolver::search(int nof_conflicts, int nof_learnts) { - std::cout << "Starting search conflicts: " << conflicts << " will go: " << nof_conflicts << std::endl; +// std::cout << "Starting search conflicts: " << conflicts << " will go: " << nof_conflicts << std::endl; // Time my executionto search_timer // opensmt::StopWatch stopwatch = opensmt::StopWatch(search_timer); #ifdef VERBOSE_SAT @@ -1506,7 +1507,7 @@ lbool CoreSMTSolver::search(int nof_conflicts, int nof_learnts) all_learnts ++; CRef cr = ca.alloc(learnt_clause, true); - ca[cr].glue = glue; + ca[cr].setglue(glue); if (logsProofForInterpolation()) { proof->endChain(cr); diff --git a/src/smtsolvers/LookaheadSMTSolver.cc b/src/smtsolvers/LookaheadSMTSolver.cc index 3e208ed26..25a4bf561 100644 --- a/src/smtsolvers/LookaheadSMTSolver.cc +++ b/src/smtsolvers/LookaheadSMTSolver.cc @@ -95,7 +95,7 @@ lbool LookaheadSMTSolver::laPropagateWrapper() { uncheckedEnqueue(out_learnt[0]); } else { CRef crd = ca.alloc(out_learnt, true); - ca[crd].glue = glue; + 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 e53e91f6f..230d2c068 100644 --- a/src/smtsolvers/TheoryIF.cc +++ b/src/smtsolvers/TheoryIF.cc @@ -328,7 +328,7 @@ CoreSMTSolver::handleUnsat() all_learnts ++; CRef cr = ca.alloc(learnt_clause, true); - ca[cr].glue = glue; + ca[cr].setglue(glue); if (logsProofForInterpolation()) { proof->endChain(cr); From e73b9123ad3a516a209681cd1e7cbc6eb30f8e62 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Tue, 5 Apr 2022 15:35:01 +0200 Subject: [PATCH 6/7] Maybe better now --- src/minisat/core/SolverTypes.h | 1 + src/smtsolvers/CoreSMTSolver.cc | 37 +++++++++++++++++++++++---------- src/smtsolvers/CoreSMTSolver.h | 5 ++++- 3 files changed, 31 insertions(+), 12 deletions(-) diff --git a/src/minisat/core/SolverTypes.h b/src/minisat/core/SolverTypes.h index 440462472..55befe991 100644 --- a/src/minisat/core/SolverTypes.h +++ b/src/minisat/core/SolverTypes.h @@ -154,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]; diff --git a/src/smtsolvers/CoreSMTSolver.cc b/src/smtsolvers/CoreSMTSolver.cc index fe378e165..49c95379e 100644 --- a/src/smtsolvers/CoreSMTSolver.cc +++ b/src/smtsolvers/CoreSMTSolver.cc @@ -577,7 +577,7 @@ Lit CoreSMTSolver::choosePolarity(Var next) { } } sign = false; - sign = not saved_polar[next]; + sign = not saved_polar[next] ^ myinv; return mkLit(next, sign); } @@ -1214,14 +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]]; // std::cout << "c.glue: " << c.getglue() << std::endl; - if (c.getglue() > 3 && c.size() > 2 && !locked(c) && (i < learnts.size() / 2 || c.activity() < extra_lim)) + 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(); @@ -1429,9 +1434,8 @@ 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) { -// std::cout << "Starting search conflicts: " << conflicts << " will go: " << nof_conflicts << std::endl; // Time my executionto search_timer // opensmt::StopWatch stopwatch = opensmt::StopWatch(search_timer); #ifdef VERBOSE_SAT @@ -1479,6 +1483,15 @@ lbool CoreSMTSolver::search(int nof_conflicts, int nof_learnts) CRef confl = propagate(); if (confl != CRef_Undef) { + + if (conflicts > longest_flip) { + longest_flip+=10000; + myinv ^= 1; + if (myinv == 0) { +// longest_trail = 0; + } + } + // CONFLICT conflicts++; conflictC++; @@ -1497,6 +1510,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; } @@ -1538,9 +1552,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 @@ -1755,7 +1770,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; @@ -1795,15 +1810,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; } } @@ -1914,7 +1929,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 a231ef6a1..71761b0b0 100644 --- a/src/smtsolvers/CoreSMTSolver.h +++ b/src/smtsolvers/CoreSMTSolver.h @@ -321,6 +321,8 @@ class CoreSMTSolver 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. @@ -389,7 +391,8 @@ class CoreSMTSolver 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 From 4f1a5220d9be97915f2819c4058414392d4c562b Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Tue, 5 Apr 2022 15:44:23 +0200 Subject: [PATCH 7/7] Do inverted less than non-inverted --- src/smtsolvers/CoreSMTSolver.cc | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/smtsolvers/CoreSMTSolver.cc b/src/smtsolvers/CoreSMTSolver.cc index 49c95379e..af1967d8b 100644 --- a/src/smtsolvers/CoreSMTSolver.cc +++ b/src/smtsolvers/CoreSMTSolver.cc @@ -1485,8 +1485,13 @@ lbool CoreSMTSolver::search(int nof_conflicts) if (confl != CRef_Undef) { if (conflicts > longest_flip) { - longest_flip+=10000; myinv ^= 1; + if (myinv == 1) { + longest_flip+=1000; + } else { + longest_flip+=10000; + } + if (myinv == 0) { // longest_trail = 0; }