|
观察序列中二值观察元放在前部 void Internal::sort_watches () watch.cpp文件 1 #include "internal.hpp" 2 3 namespace CaDiCaL { 4 5 void Internal::init_watches () { 6 assert (wtab.empty ()); 7 if (wtab.size () < 2*vsize) 8 wtab.resize (2*vsize, Watches ()); 9 LOG ("initialized watcher tables"); 10 } 11 12 void Internal::clear_watches () { 13 for (auto lit : lits) 14 watches (lit).clear (); 15 } 16 17 void Internal::reset_watches () { 18 assert (!wtab.empty ()); 19 erase_vector (wtab); 20 LOG ("reset watcher tables"); 21 } 22 23 // This can be quite costly since lots of memory is accessed in a rather 24 // random fashion, and thus we optionally profile it. 25 26 void Internal::connect_watches (bool irredundant_only) { 27 START (connect); 28 assert (watching ()); 29 30 LOG ("watching all %sclauses", irredundant_only ? "irredundant " : ""); 31 32 // First connect binary clauses. 33 // 34 for (const auto & c : clauses) { 35 if (irredundant_only && c->redundant) continue; 36 if (c->garbage || c->size > 2) continue; 37 watch_clause (c); 38 } 39 40 // Then connect non-binary clauses. 41 // 42 for (const auto & c : clauses) { 43 if (irredundant_only && c->redundant) continue; 44 if (c->garbage || c->size == 2) continue; 45 watch_clause (c); 46 if (!level) { 47 const int lit0 = c->literals[0]; 48 const int lit1 = c->literals[1]; 49 const signed char tmp0 = val (lit0); 50 const signed char tmp1 = val (lit1); 51 if (tmp0 > 0) continue; 52 if (tmp1 > 0) continue; 53 if (tmp0 < 0) { 54 const size_t pos0 = var (lit0).trail; 55 if (pos0 < propagated) { 56 propagated = pos0; 57 LOG ("literal %d resets propagated to %zd", lit0, pos0); 58 } 59 } 60 if (tmp1 < 0) { 61 const size_t pos1 = var (lit1).trail; 62 if (pos1 < propagated) { 63 propagated = pos1; 64 LOG ("literal %d resets propagated to %zd", lit1, pos1); 65 } 66 } 67 } 68 } 69 70 STOP (connect); 71 } 72 73 void Internal::sort_watches () { 74 assert (watching ()); 75 LOG ("sorting watches"); 76 Watches saved; 77 for (auto lit : lits) { 78 Watches & ws = watches (lit); 79 80 const const_watch_iterator end = ws.end (); 81 watch_iterator j = ws.begin (); 82 const_watch_iterator i; 83 84 assert (saved.empty ()); 85 86 for (i = j; i != end; i++) { 87 const Watch w = *i; 88 if (w.binary ()) *j++ = w; 89 else saved.push_back (w); 90 } 91 92 std::copy (saved.cbegin (), saved.cend (), j); 93 94 saved.clear (); 95 } 96 } 97 98 }
涉及void Internal::sort_watches () 使用的函数 lookahead.cpp中 lookahead_probing() 1 // We run probing on all literals with some differences: 2 // 3 // * no limit on the number of propagations. We rely on terminating to stop() 4 // * we run only one round 5 // 6 // The run can be expensive, so we actually first run the cheaper 7 // occurrence version and only then run lookahead. 8 // 我们对所有不同的字面量运行探测: 对传播次数没有限制。我们依靠终止来停止()。 我们只运行一轮，这个运行可能很昂贵，所以我们实际上首先运行便宜的发生版本，然后才运行向前看。 9 int Internal::lookahead_probing() { 10 11 if (!active ()) 12 return 0; 13 14 MSG ("lookahead-probe-round %" PRId64 15 " without propagations limit and %zu assumptions", 16 stats.probingrounds, assumptions.size()); 17 18 termination_forced = false; 19 20 #ifndef QUIET 21 int old_failed = stats.failed; 22 int64_t old_probed = stats.probed; 23 #endif 24 int64_t old_hbrs = stats.hbrs; 25 26 if (unsat) return INT_MIN; 27 if (level) backtrack (); 28 if (!propagate ()) { 29 MSG ("empty clause before probing"); 30 learn_empty_clause (); 31 return INT_MIN; 32 } 33 34 if (terminating_asked()) 35 return most_occurring_literal(); 36 37 decompose (); 38 39 if (ternary ()) // If we derived a binary clause 40 decompose (); // then start another round of ELS. 41 42 // Remove duplicated binary clauses and perform in essence hyper unary 43 // resolution, i.e., derive the unit '2' from '1 2' and '-1 2'. 44 // 45 mark_duplicated_binary_clauses_as_garbage (); 46 47 lim.conflicts = -1; 48 49 if (!probes.empty ()) lookahead_flush_probes (); 50 51 // We reset 'propfixed' since there was at least another conflict thus 52 // a new learned clause, which might produce new propagations (and hyper 53 // binary resolvents). During 'generate_probes' we keep the old value. 54 // 55 for (int idx = 1; idx <= max_var; idx++) 56 propfixed (idx) = propfixed (-idx) = -1; 57 58 assert (unsat || propagated == trail.size ()); 59 propagated = propagated2 = trail.size (); 60 61 int probe; 62 int res = most_occurring_literal(); 63 int max_hbrs = -1; 64 65 set_mode (PROBE); 66 67 MSG("unsat = %d, terminating_asked () = %d ", unsat, terminating_asked ()); 68 while (!unsat && 69 !terminating_asked () && 70 (probe = lookahead_next_probe ())) { 71 stats.probed++; 72 int hbrs; 73 74 probe_assign_decision (probe); 75 if (probe_propagate ()) 76 hbrs = trail.size(), backtrack(); 77 else hbrs = 0, failed_literal (probe); 78 if (max_hbrs < hbrs || 79 (max_hbrs == hbrs && 80 internal->bumped(probe) > internal->bumped(res))) { 81 res = probe; 82 max_hbrs = hbrs; 83 } 84 } 85 86 reset_mode (PROBE); 87 88 if (unsat) { 89 MSG ("probing derived empty clause"); 90 res = INT_MIN; 91 } 92 else if (propagated < trail.size ()) { 93 MSG ("probing produced %zd units", 94 (size_t)(trail.size () - propagated)); 95 if (!propagate ()) { 96 MSG ("propagating units after probing results in empty clause"); 97 learn_empty_clause (); 98 res = INT_MIN; 99 } else sort_watches (); 100 } 101 102 #ifndef QUIET 103 int failed = stats.failed - old_failed; 104 int64_t probed = stats.probed - old_probed; 105 #endif 106 int64_t hbrs = stats.hbrs - old_hbrs; 107 108 MSG ("lookahead-probe-round %" PRId64 " probed %" PRId64 109 " and found %d failed literals", 110 stats.probingrounds, 111 probed, failed); 112 113 if (hbrs) 114 PHASE ("lookahead-probe-round", stats.probingrounds, 115 "found %" PRId64 " hyper binary resolvents", hbrs); 116 117 MSG ("lookahead literal %d with %d\n", res, max_hbrs); 118 119 return res; 120 }
|
|