码迷,mamicode.com
首页 > 其他好文 > 详细

5.CaDiCal代码解读——CaDiCal的internal相关代码--clause.hpp--clause.cpp

时间:2020-07-29 21:34:34      阅读:76      评论:0      收藏:0      [点我收藏+]

标签:next   factor   orm   gen   计数   alt   size   mem   numbers   

clause.hpp

clause.cpp

 


 

clause.hpp 

声明了常用类型的别名:

 

/*------------------------------------------------------------------------*/

typedef  int *  literal_iterator;
typedef  const int *  const_literal_iterator;

/*------------------------------------------------------------------------*/

   

 

 

定义结构类型Clause、clause_smaller_size、clause_lit_less_than

 
  1 // The ‘Clause‘ data structure is very important. There are usually many
  2 // clauses and accessing them is a hot-spot.  Thus we use common
  3 // optimizations to reduce memory and improve cache usage, even though this
  4 // induces some complexity in understanding the code.
  5 //
  6 // The most important optimization is to ‘embed‘ the actual literals in the
  7 // clause.  This requires a variadic size structure and thus strictly is not
  8 // ‘C‘ conform, but supported by all compilers we used.  The alternative is
  9 // to store the actual literals somewhere else, which not only needs more
 10 // memory but more importantly also requires another memory access and thus
 11 // is very costly.
最重要的优化是在子句中“嵌入”实际的文字。这需要一个可变大小的结构,因此严格来说不符合“C”,
但我们使用的所有编译器都支持它另一种方法是将实际的字面值存储在其他地方,
这不仅需要更多的内存,而且更重要的是还需要另一次内存访问,因此开销非常大。

12 13 struct Clause { 14 #ifdef LOGGING 15 int64_t id; // Only useful for debugging. 16 #endif 17 18 bool conditioned:1; // Tried for globally blocked clause elimination. 19 bool covered:1; // Already considered for covered clause elimination. 20 bool enqueued:1; // Enqueued on backward queue. 21 bool frozen:1; // Temporarily frozen (in covered clause elimination). 22 bool garbage:1; // can be garbage collected unless it is a ‘reason‘ 23 bool gate:1 ; // Clause part of a gate (function definition). 24 bool hyper:1; // redundant hyper binary or ternary resolved 25 bool instantiated:1;// tried to instantiate 26 bool keep:1; // always keep this clause (if redundant) 27 bool moved:1; // moved during garbage collector (‘copy‘ valid) 28 bool reason:1; // reason / antecedent clause can not be collected 29 bool redundant:1; // aka ‘learned‘ so not ‘irredundant‘ (original) 30 bool transred:1; // already checked for transitive reduction 31 bool subsume:1; // not checked in last subsumption round 32 unsigned used:2; // resolved in conflict analysis since last ‘reduce‘ 33 bool vivified:1; // clause already vivified 34 bool vivify:1; // clause scheduled to be vivified 35 36 // The glucose level (‘LBD‘ or short ‘glue‘) is a heuristic value for the 37 // expected usefulness of a learned clause, where smaller glue is consider 38 // more useful. During learning the ‘glue‘ is determined as the number of 39 // decisions in the learned clause. Thus the glue of a clause is a strict 40 // upper limit on the smallest number of decisions needed to make it 41 // propagate. For instance a binary clause will propagate if one of its 42 // literals is set to false. Similarly a learned clause with glue 1 can 43 // propagate after one decision, one with glue 2 after 2 decisions etc. 44 // In some sense the glue is an abstraction of the size of the clause. 45 // 46 // See the IJCAI‘09 paper by Audemard & Simon for more details. We 47 // switched back and forth between keeping the glue stored in a clause and 48 // using it only initially to determine whether it is kept, that is 49 // survives clause reduction. The latter strategy is not bad but also 50 // does not allow to use glue values for instance in ‘reduce‘. 51 // 52 // More recently we also update the glue and promote clauses to lower 53 // level tiers during conflict analysis. The idea of using three tiers is 54 // also due to Chanseok Oh and thus used in all recent ‘Maple...‘ solvers. 55 // Tier one are the always kept clauses with low glue at most 56 // ‘opts.reducetier1glue‘ (default ‘2‘). The second tier contains all 57 // clauses with glue larger than ‘opts.reducetier1glue‘ but smaller or 58 // equal than ‘opts.reducetier2glue‘ (default ‘6‘). The third tier 59 // consists of clauses with glue larger than ‘opts.reducetier2glue‘. 60 // 61 // Clauses in tier one are not deleted in ‘reduce‘. Clauses in tier 62 // two require to be unused in two consecutive ‘reduce‘ intervals before 63 // being collected while for clauses in tier three not being used since 64 // the last ‘reduce‘ call makes them deletion candidates. Clauses derived 65 // by hyper binary or ternary resolution (even though small and thus with 66 // low glue) are always removed if they remain unused during one interval. 67 // See ‘mark_useless_redundant_clauses_as_garbage‘ in ‘reduce.cpp‘ and 68 // ‘bump_clause‘ in ‘analyze.cpp‘. 69 // 70 int glue; 71 72 int size; // Actual size of ‘literals‘ (at least 2). 73 int pos; // Position of last watch replacement [Gent‘13]. 74 75 union { 76 77 int literals[2]; // Of variadic ‘size‘ (shrunken if strengthened). 78 79 Clause * copy; // Only valid if ‘moved‘, then that‘s where to. 80 // 81 // The ‘copy‘ field is only valid for ‘moved‘ clauses in the moving 82 // garbage collector ‘copy_non_garbage_clauses‘ for keeping clauses 83 // compactly in a contiguous memory arena. Otherwise, most of 84 // the time, ‘literals‘ is valid. See ‘collect.cpp‘ for details. 85 }; 86 87 literal_iterator begin () { return literals; } 88 literal_iterator end () { return literals + size; } 89 90 const_literal_iterator begin () const { return literals; } 91 const_literal_iterator end () const { return literals + size; } 92 93 static size_t bytes (int size) { 94 95 // Memory sanitizer insists that clauses put into consecutive memory in 96 // the arena are still 8 byte aligned. We could also allocate 8 byte 97 // aligned memory there. However, assuming the real memory foot print 98 // of a clause is 8 bytes anyhow, we just allocate 8 byte aligned memory 99 // all the time (even if allocated outside of the arena). 100 // 101 assert (size > 1); 102 return align ((size - 2) * sizeof (int) + sizeof (Clause), 8); 103 } 104 105 size_t bytes () const { return bytes (size); } 106 107 // Check whether this clause is ready to be collected and deleted. The 108 // ‘reason‘ flag is only there to protect reason clauses in ‘reduce‘, 109 // which does not backtrack to the root level. If garbage collection is 110 // triggered from a preprocessor, which backtracks to the root level, then 111 // ‘reason‘ is false for sure. We want to use the same garbage collection 112 // code though for both situations and thus hide here this variance. 113 // 114 bool collect () const { return !reason && garbage; } 115 };

 

   
 
1 struct clause_smaller_size {
2   bool operator () (const Clause * a, const Clause * b) {
3     return a->size < b->size;
4   }
5 };
   
 
 1 // Place literals over the same variable close to each other.  This would
 2 // allow eager removal of identical literals and detection of tautological
 3 // clauses but is only currently used for better logging (see also
 4 // ‘opts.logsort‘ in ‘logging.cpp‘).
 5 
 6 struct clause_lit_less_than {
 7   bool operator () (int a, int b) const {
 8     int s = abs (a), t = abs (b);
 9     return s < t || (s == t && a < b);
10   }
11 };
   

 

关于Clause属性的解读

一、 布尔型的数据成员——记录子句的状态
 

1.

bool conditioned:1; // Tried for globally blocked clause elimination.

尝试消除全局阻塞子句

 

2.
bool covered:1; // Already considered for covered clause elimination.

已考虑消除

 

3.
bool enqueued:1; // Enqueued on backward queue.

在回溯队列中排队

 

4.
bool frozen:1; // Temporarily frozen (in covered clause elimination).

冻结(适用子句消除)。

 

5.
bool garbage:1; // can be garbage collected unless it is a ‘reason‘

可以被垃圾收集,除非是“reason”子句

 

6.
bool gate:1 ; // Clause part of a gate (function definition).

译文:门的子句(函数定义)

 

7.
bool hyper:1; // redundant hyper binary or ternary resolved

译文:冗余超二进制或三元分解

 

8.
bool instantiated:1;// tried to instantiate

试图实例化

 

9.
bool keep:1; // always keep this clause (if redundant)

总是保留这个条款(如果多余的话)

 

10.
bool moved:1; // moved during garbage collector (‘copy‘ valid)

在垃圾回收期间移动(‘copy‘有效)

 

11.
bool reason:1; // reason / antecedent clause can not be collected

译文:原因/先行条款不能收取

 

12.
bool redundant:1; // aka ‘learned‘ so not ‘irredundant‘ (original)

译文:也就是" learned "而不是" irredundant "(原文)

 

13.
bool transred:1; // already checked for transitive reduction

译文:已检查传递约简

 

14.
bool subsume:1; // not checked in last subsumption round

译文:上一轮归结没有登记

 

15.
unsigned used:2; // resolved in conflict analysis since last ‘reduce‘

 

16.
bool vivified:1; // clause already vivified
bool vivify:1;   // clause scheduled to be vivified

   
 二、 表示具体数值的数据成员------表示状态的计数等 
 

1.
unsigned used:2; // resolved in conflict analysis since last ‘reduce‘

译文:在冲突分析中解决,自上次“减少”以来

 

2.

int glue;

 

3.

int size; // Actual size of ‘literals‘ (at least 2).

 

4.
int pos; // Position of last watch replacement [Gent‘13].

   
 三、  子句中相关文字的数据成员
   

union {

int literals[2]; // Of variadic ‘size‘ (shrunken if strengthened).

                         可变尺寸(增强后缩小)

Clause * copy; // Only valid if ‘moved‘, then that‘s where to.
//
// The ‘copy‘ field is only valid for ‘moved‘ clauses in the moving
// garbage collector ‘copy_non_garbage_clauses‘ for keeping clauses
// compactly in a contiguous memory arena. Otherwise, most of
// the time, ‘literals‘ is valid. See ‘collect.cpp‘ for details.

“copy”字段仅对移动垃圾收集器“copy_non_garbage_clauses”中的“moved”子句有效,用于将子句紧凑地保存在一个连续的内存竞技场中。否则,大多数时候,“literals”是有效的。细节见‘collect.cpp‘ .


};

   

 

关于Clause类型的操作函数的解读

       注: Clause类型有很多数据成员,缺没有针对他们的访问操作函数;也没有声明一个友元类?——结构体默认公有访问权限

 

   

literal_iterator begin () { return literals; }
literal_iterator end () { return literals + size; }

const_literal_iterator begin () const { return literals; }
const_literal_iterator end () const { return literals + size; }

以上访问子句中文字所在位置,用整型指针表示;

   
 2

两个重载的函数bytes

 

static size_t bytes (int size) {

// Memory sanitizer insists that clauses put into consecutive memory in
// the arena are still 8 byte aligned. We could also allocate 8 byte
// aligned memory there. However, assuming the real memory foot print
// of a clause is 8 bytes anyhow, we just allocate 8 byte aligned memory
// all the time (even if allocated outside of the arena).
//
assert (size > 1);
return align ((size - 2) * sizeof (int) + sizeof (Clause), 8);
}

该函数返回子句的字节数;调用宏align,按8或8的倍数对齐计算,

如7则按8算;13则按16算;

 

size_t bytes () const { return bytes (size); }

// Check whether this clause is ready to be collected and deleted. The
// ‘reason‘ flag is only there to protect reason clauses in ‘reduce‘,
// which does not backtrack to the root level. If garbage collection is
// triggered from a preprocessor, which backtracks to the root level, then
// ‘reason‘ is false for sure. We want to use the same garbage collection
// code though for both situations and thus hide here this variance.
//

   
3 bool collect () const { return !reason && garbage; }
   

 


 

Clause.cpp函数并不对应类型声明的定义代码,这里收集了关于子句被操作的函数,这些函数是分属于不同的类的成员函数。

 

1.完整函数代码

          10-26行中的若干for语句很雷人!!!

 
  1 #include "internal.hpp"
  2 
  3 namespace CaDiCaL {
  4 
  5 /*------------------------------------------------------------------------*/
  6 
  7 // Signed marking or unmarking of a clause or the global ‘clause‘.
  8 
  9 void Internal::mark (Clause * c) {
 10   for (const auto & lit : *c) mark (lit);
 11 }
 12 
 13 void Internal::mark2 (Clause * c) {
 14   for (const auto & lit : *c) mark2 (lit);
 15 }
 16 
 17 void Internal::unmark (Clause * c) {
 18   for (const auto & lit : *c) unmark (lit);
 19 }
 20 
 21 void Internal::mark_clause () {
 22   for (const auto & lit : clause) mark (lit);
 23 }
 24 
 25 void Internal::unmark_clause () {
 26   for (const auto & lit : clause) unmark (lit);
 27 }
 28 
 29 /*------------------------------------------------------------------------*/
 30 
 31 // Mark the variables of an irredundant clause to ‘have been removed‘, which
 32 // will trigger these variables to be considered again in the next bounded
 33 // variable elimination phase.  This is called from ‘mark_garbage‘ below.
 34 // Note that ‘mark_removed (int lit)‘ will also mark the blocking flag of
 35 // ‘-lit‘ to trigger reconsidering blocking clauses on ‘-lit‘.
 36 
 37 void Internal::mark_removed (Clause * c, int except) {
 38   LOG (c, "marking removed");
 39   assert (!c->redundant);
 40   for (const auto & lit : *c)
 41     if (lit != except)
 42       mark_removed (lit);
 43 }
 44 
 45 // Mark the variables of a (redundant or irredundant) clause to ‘have been
 46 // added‘, which triggers clauses with such a variables, to be considered
 47 // both as a subsumed or subsuming clause in the next subsumption phase.
 48 // This function is called from ‘new_clause‘ below as well as in situations
 49 // where a clause is shrunken (and thus needs to be at least considered
 50 // again to subsume a larger clause).  We also use this to tell
 51 // ‘ternary‘ preprocessing reconsider clauses on an added literal as well as
 52 // trying to block clauses on it.
 53 
 54 inline void Internal::mark_added (int lit, int size, bool redundant) {
 55   mark_subsume (lit);
 56   if (size == 3)
 57     mark_ternary (lit);
 58   if (!redundant)
 59     mark_block (lit);
 60 }
 61 
 62 void Internal::mark_added (Clause * c) {
 63   LOG (c, "marking added");
 64   assert (likely_to_be_kept_clause (c));
 65   for (const auto & lit : *c)
 66     mark_added (lit, c->size, c->redundant);
 67 }
 68 
 69 /*------------------------------------------------------------------------*/
 70 
 71 Clause * Internal::new_clause (bool red, int glue) {
 72 
 73   assert (clause.size () <= (size_t) INT_MAX);
 74   const int size = (int) clause.size ();
 75   assert (size >= 2);
 76 
 77   if (glue > size) glue = size;
 78 
 79   // Determine whether this clauses should be kept all the time.
 80   //
 81   bool keep;
 82   if (!red) keep = true;
 83   else if (glue <= opts.reducetier1glue) keep = true;
 84   else keep = false;
 85 
 86   size_t bytes = Clause::bytes (size);
 87   Clause * c = (Clause *) new char[bytes];
 88 
 89   stats.added.total++;
 90 #ifdef LOGGING
 91   c->id = stats.added.total;
 92 #endif
 93 
 94   c->conditioned = false;
 95   c->covered = false;
 96   c->enqueued = false;
 97   c->frozen = false;
 98   c->garbage = false;
 99   c->gate = false;
100   c->hyper = false;
101   c->instantiated = false;
102   c->keep = keep;
103   c->moved = false;
104   c->reason = false;
105   c->redundant = red;
106   c->transred = false;
107   c->subsume = false;
108   c->vivified = false;
109   c->vivify = false;
110   c->used = 0;
111 
112   c->glue = glue;
113   c->size = size;
114   c->pos = 2;
115 
116   for (int i = 0; i < size; i++) c->literals[i] = clause[i];
117 
118   // Just checking that we did not mess up our sophisticated memory layout.
119   // This might be compiler dependent though. Crucial for correctness.
120   //
121   assert (c->bytes () == bytes);
122 
123   stats.current.total++;
124   stats.added.total++;
125 
126   if (red) {
127     stats.current.redundant++;
128     stats.added.redundant++;
129   } else {
130     stats.irrbytes += bytes;
131     stats.current.irredundant++;
132     stats.added.irredundant++;
133   }
134 
135   clauses.push_back (c);
136   LOG (c, "new pointer %p", c);
137 
138   if (likely_to_be_kept_clause (c)) mark_added (c);
139 
140   return c;
141 }
142 
143 /*------------------------------------------------------------------------*/
144 
145 void Internal::promote_clause (Clause * c, int new_glue) {
146   assert (c->redundant);
147   if (c->keep) return;
148   if (c->hyper) return;
149   int old_glue = c->glue;
150   if (new_glue >= old_glue) return;
151   if (!c->keep && new_glue <= opts.reducetier1glue) {
152     LOG (c, "promoting with new glue %d to tier1", new_glue);
153     stats.promoted1++;
154     c->keep = true;
155   } else if (old_glue > opts.reducetier2glue &&
156              new_glue <= opts.reducetier2glue) {
157     LOG (c, "promoting with new glue %d to tier2", new_glue);
158     stats.promoted2++;
159     c->used = 2;
160   } else if (c->keep)
161     LOG (c, "keeping with new glue %d in tier1", new_glue);
162   else if (old_glue <= opts.reducetier2glue)
163     LOG (c, "keeping with new glue %d in tier2", new_glue);
164   else
165     LOG (c, "keeping with new glue %d in tier3", new_glue);
166   stats.improvedglue++;
167   c->glue = new_glue;
168 }
169 
170 /*------------------------------------------------------------------------*/
171 
172 // Shrinking a clause, e.g., removing one or more literals, requires to fix
173 // the ‘pos‘ field, if it exists and points after the new last literal, has
174 // to adjust the global statistics counter of allocated bytes for
175 // irredundant clauses, and also adjust the glue value of redundant clauses
176 // if the size becomes smaller than the glue.  Also mark the literals in the
177 // resulting clause as ‘added‘.  The result is the number of (aligned)
178 // removed bytes, resulting from shrinking the clause.
179 //
180 size_t Internal::shrink_clause (Clause * c, int new_size) {
181 
182   assert (new_size >= 2);
183   assert (new_size < c->size);
184 #ifndef NDEBUG
185   for (int i = c->size; i < new_size; i++)
186     c->literals[i] = 0;
187 #endif
188 
189   if (c->pos >= new_size) c->pos = 2;
190 
191   size_t old_bytes = c->bytes ();
192   c->size = new_size;
193   size_t new_bytes = c->bytes ();
194   size_t res = old_bytes - new_bytes;
195 
196   if (c->redundant) promote_clause (c, min (c->size-1, c->glue));
197   else if (old_bytes > new_bytes) {
198     assert (stats.irrbytes >= (int64_t) res);
199     stats.irrbytes -= res;
200   }
201 
202   if (likely_to_be_kept_clause (c)) mark_added (c);
203 
204   return res;
205 }
206 
207 // This is the ‘raw‘ deallocation of a clause.  If the clause is in the
208 // arena nothing happens.  If the clause is not in the arena its memory is
209 // reclaimed immediately.
210 
211 void Internal::deallocate_clause (Clause * c) {
212   char * p = (char*) c;
213   if (arena.contains (p)) return;
214   LOG (c, "deallocate pointer %p", c);
215   delete [] p;
216 }
217 
218 void Internal::delete_clause (Clause * c) {
219   LOG (c, "delete pointer %p", c);
220   size_t bytes = c->bytes ();
221   stats.collected += bytes;
222   if (c->garbage) {
223     assert (stats.garbage >= (int64_t) bytes);
224     stats.garbage -= bytes;
225 
226     // See the discussion in ‘propagate‘ on avoiding to eagerly trace binary
227     // clauses as deleted (produce ‘d ...‘ lines) as soon they are marked
228     // garbage.  We avoid this and only trace them as deleted when they are
229     // actually deleted here.  This allows the solver to propagate binary
230     // garbage clauses without producing incorrect ‘d‘ lines.  The effect
231     // from the proof perspective is that the deletion of these binary
232     // clauses occurs later in the proof file.
233     //
234     if (proof && c->size == 2)
235       proof->delete_clause (c);
236   }
237   deallocate_clause (c);
238 }
239 
240 // We want to eagerly update statistics as soon clauses are marked garbage.
241 // Otherwise ‘report‘ for instance gives wrong numbers after ‘subsume‘
242 // before the next ‘reduce‘.  Thus we factored out marking and accounting
243 // for garbage clauses.
244 //
245 // Eagerly deleting clauses instead is problematic, since references to these
246 // clauses need to be flushed, which is too costly to do eagerly.
247 //
248 // We also update garbage statistics at this point.  This helps to
249 // determine whether the garbage collector should be called during for
250 // instance bounded variable elimination, which usually generates lots of
251 // garbage clauses.
252 //
253 // In order not to miss any update to these clause statistics we call
254 // ‘check_clause_stats‘ after garbage collection in debugging mode.
255 //
256 void Internal::mark_garbage (Clause * c) {
257 
258   assert (!c->garbage);
259 
260   // Delay tracing deletion of binary clauses.  See the discussion above in
261   // ‘delete_clause‘ and also in ‘propagate‘.
262   //
263   if (proof && c->size != 2)
264     proof->delete_clause (c);
265 
266   assert (stats.current.total > 0);
267   stats.current.total--;
268 
269   size_t bytes = c->bytes ();
270   if (c->redundant) {
271     assert (stats.current.redundant > 0);
272     stats.current.redundant--;
273   } else {
274     assert (stats.current.irredundant > 0);
275     stats.current.irredundant--;
276     assert (stats.irrbytes >= (int64_t) bytes);
277     stats.irrbytes -= bytes;
278     mark_removed (c);
279   }
280   stats.garbage += bytes;
281   c->garbage = true;
282   c->used = 0;
283 
284   LOG (c, "marked garbage pointer %p", c);
285 }
286 
287 /*------------------------------------------------------------------------*/
288 
289 // Almost the same function as ‘search_assign‘ except that we do not pretend
290 // to learn a new unit clause (which was confusing in log files).
291 
292 void Internal::assign_original_unit (int lit) {
293   assert (!level);
294   const int idx = vidx (lit);
295   assert (!vals[idx]);
296   assert (!flags (idx).eliminated ());
297   Var & v = var (idx);
298   v.level = level;
299   v.trail = (int) trail.size ();
300   v.reason = 0;
301   const signed char tmp = sign (lit);
302   vals[idx] = tmp;
303   vals[-idx] = -tmp;
304   assert (val (lit) > 0);
305   assert (val (-lit) < 0);
306   trail.push_back (lit);
307   LOG ("original unit assign %d", lit);
308   mark_fixed (lit);
309   if (propagate ()) return;
310   LOG ("propagation of original unit results in conflict");
311   learn_empty_clause ();
312 }
313 
314 // New clause added through the API, e.g., while parsing a DIMACS file.
315 //
316 void Internal::add_new_original_clause () {
317   if (level) backtrack ();
318   LOG (original, "original clause");
319   bool skip = false;
320   if (unsat) {
321     LOG ("skipping clause since formula already inconsistent");
322     skip = true;
323   } else {
324     assert (clause.empty ());
325     for (const auto & lit : original) {
326       int tmp = marked (lit);
327       if (tmp > 0) {
328         LOG ("removing duplicated literal %d", lit);
329       } else if (tmp < 0) {
330         LOG ("tautological since both %d and %d occur", -lit, lit);
331         skip = true;
332       } else {
333         mark (lit);
334         tmp = val (lit);
335         if (tmp < 0) {
336           LOG ("removing falsified literal %d", lit);
337         } else if (tmp > 0) {
338           LOG ("satisfied since literal %d true", lit);
339           skip = true;
340         } else {
341           clause.push_back (lit);
342           assert (flags (lit).status != Flags::UNUSED);
343         }
344       }
345     }
346     for (const auto & lit : original)
347       unmark (lit);
348   }
349   if (skip) {
350     if (proof) proof->delete_clause (original);
351   } else {
352     size_t size = clause.size ();
353     if (!size) {
354       if (!unsat) {
355         if (!original.size ()) VERBOSE (1, "found empty original clause");
356         else MSG ("found falsified original clause");
357         unsat = true;
358       }
359     } else if (size == 1) {
360       assign_original_unit (clause[0]);
361     } else {
362       Clause * c = new_clause (false);
363       watch_clause (c);
364     }
365     if (original.size () > size) {
366       external->check_learned_clause ();
367       if (proof) {
368         proof->add_derived_clause (clause);
369         proof->delete_clause (original);
370       }
371     }
372   }
373   clause.clear ();
374 }
375 
376 // Add learned new clause during conflict analysis and watch it. Requires
377 // that the clause is at least of size 2, and the first two literals
378 // are assigned at the highest decision level.
379 //
380 Clause * Internal::new_learned_redundant_clause (int glue) {
381   assert (clause.size () > 1);
382 #ifndef NDEBUG
383   for (size_t i = 2; i < clause.size (); i++)
384     assert (var (clause[0]).level >= var (clause[i]).level),
385     assert (var (clause[1]).level >= var (clause[i]).level);
386 #endif
387   external->check_learned_clause ();
388   Clause * res = new_clause (true, glue);
389   if (proof) proof->add_derived_clause (res);
390   assert (watching ());
391   watch_clause (res);
392   return res;
393 }
394 
395 // Add hyper binary resolved clause during ‘probing‘.
396 //
397 Clause * Internal::new_hyper_binary_resolved_clause (bool red, int glue) {
398   external->check_learned_clause ();
399   Clause * res = new_clause (red, glue);
400   if (proof) proof->add_derived_clause (res);
401   assert (watching ());
402   watch_clause (res);
403   return res;
404 }
405 
406 // Add hyper ternary resolved clause during ‘ternary‘.
407 //
408 Clause * Internal::new_hyper_ternary_resolved_clause (bool red) {
409   external->check_learned_clause ();
410   size_t size = clause.size ();
411   Clause * res = new_clause (red, size);
412   if (proof) proof->add_derived_clause (res);
413   assert (!watching ());
414   return res;
415 }
416 
417 // Add a new clause with same glue and redundancy as ‘orig‘ but literals are
418 // assumed to be in ‘clause‘ in ‘decompose‘ and ‘vivify‘.
419 //
420 Clause * Internal::new_clause_as (const Clause * orig) {
421   external->check_learned_clause ();
422   const int new_glue = orig->glue;
423   Clause * res = new_clause (orig->redundant, new_glue);
424   assert (!orig->redundant || !orig->keep || res->keep);
425   if (proof) proof->add_derived_clause (res);
426   assert (watching ());
427   watch_clause (res);
428   return res;
429 }
430 
431 // Add resolved clause during resolution, e.g., bounded variable
432 // elimination, but do not connect its occurrences here.
433 //
434 Clause * Internal::new_resolved_irredundant_clause () {
435   external->check_learned_clause ();
436   Clause * res = new_clause (false);
437   if (proof) proof->add_derived_clause (res);
438   assert (!watching ());
439   return res;
440 }
441 
442 }

 

   

 

2.分段解析

 

一、 有关子句mark操作函数
 
/*------------------------------------------------------------------------*/

// Signed marking or unmarking of a clause or the global ‘clause‘.

void Internal::mark (Clause * c) {
  for (const auto & lit : *c) mark (lit);
}

void Internal::mark2 (Clause * c) {
  for (const auto & lit : *c) mark2 (lit);
}

void Internal::unmark (Clause * c) {
  for (const auto & lit : *c) unmark (lit);
}

void Internal::mark_clause () {
  for (const auto & lit : clause) mark (lit);
}

void Internal::unmark_clause () {
  for (const auto & lit : clause) unmark (lit);
}

/*------------------------------------------------------------------------*/

// Mark the variables of an irredundant clause to ‘have been removed‘, which
// will trigger these variables to be considered again in the next bounded
// variable elimination phase.  This is called from ‘mark_garbage‘ below.
// Note that ‘mark_removed (int lit)‘ will also mark the blocking flag of
// ‘-lit‘ to trigger reconsidering blocking clauses on ‘-lit‘.

void Internal::mark_removed (Clause * c, int except) {
  LOG (c, "marking removed");
  assert (!c->redundant);
  for (const auto & lit : *c)
    if (lit != except)
      mark_removed (lit);
}

// Mark the variables of a (redundant or irredundant) clause to ‘have been
// added‘, which triggers clauses with such a variables, to be considered
// both as a subsumed or subsuming clause in the next subsumption phase.
// This function is called from ‘new_clause‘ below as well as in situations
// where a clause is shrunken (and thus needs to be at least considered
// again to subsume a larger clause).  We also use this to tell
// ‘ternary‘ preprocessing reconsider clauses on an added literal as well as
// trying to block clauses on it.

inline void Internal::mark_added (int lit, int size, bool redundant) {
  mark_subsume (lit);
  if (size == 3)
    mark_ternary (lit);
  if (!redundant)
    mark_block (lit);
}

void Internal::mark_added (Clause * c) {
  LOG (c, "marking added");
  assert (likely_to_be_kept_clause (c));
  for (const auto & lit : *c)
    mark_added (lit, c->size, c->redundant);
}

/*------------------------------------------------------------------------*/

 

   
二、 子句构建
 
 1 Clause * Internal::new_clause (bool red, int glue) {
 2 
 3   assert (clause.size () <= (size_t) INT_MAX);  
// Internal数据成员clause中包含从cnf文件读入的子句
4 const int size = (int) clause.size (); 5 assert (size >= 2); 6 7 if (glue > size) glue = size; 8 9 // Determine whether this clauses should be kept all the time. 10 // 译文:确定这些条款是否应该一直保留 11 bool keep; 12 if (!red) keep = true; 13 else if (glue <= opts.reducetier1glue) keep = true; 14 else keep = false; 15 16 size_t bytes = Clause::bytes (size); 17 Clause * c = (Clause *) new char[bytes]; 18 19 stats.added.total++; 20 #ifdef LOGGING 21 c->id = stats.added.total; 22 #endif 23 24 c->conditioned = false; 25 c->covered = false; 26 c->enqueued = false; 27 c->frozen = false; 28 c->garbage = false; 29 c->gate = false; 30 c->hyper = false; 31 c->instantiated = false; 32 c->keep = keep; 33 c->moved = false; 34 c->reason = false; 35 c->redundant = red;//参数red标定该子句是否是学习子句 36 c->transred = false; 37 c->subsume = false; 38 c->vivified = false; 39 c->vivify = false; 40 c->used = 0; 41 42 c->glue = glue; 43 c->size = size; 44 c->pos = 2; 45 46 for (int i = 0; i < size; i++) c->literals[i] = clause[i]; 47 48 // Just checking that we did not mess up our sophisticated memory layout. 49 // This might be compiler dependent though. Crucial for correctness. 50 // 51 assert (c->bytes () == bytes); 52 53 stats.current.total++; 54 stats.added.total++; 55 56 if (red) { 57 stats.current.redundant++; 58 stats.added.redundant++; 59 } else { 60 stats.irrbytes += bytes; 61 stats.current.irredundant++; 62 stats.added.irredundant++; 63 } 64 65 clauses.push_back (c); 66 LOG (c, "new pointer %p", c); 67 68 if (likely_to_be_kept_clause (c)) mark_added (c); 69 70 return c; 71 }

 

   
 三 子句提升、沉降 和 删除与内存释放
   
 1 void Internal::promote_clause (Clause * c, int new_glue) {
 2   assert (c->redundant);
 3   if (c->keep) return;
 4   if (c->hyper) return;
 5   int old_glue = c->glue;
 6   if (new_glue >= old_glue) return;
 7   if (!c->keep && new_glue <= opts.reducetier1glue) {
 8     LOG (c, "promoting with new glue %d to tier1", new_glue);
 9     stats.promoted1++;
10     c->keep = true;
11   } else if (old_glue > opts.reducetier2glue &&
12              new_glue <= opts.reducetier2glue) {
13     LOG (c, "promoting with new glue %d to tier2", new_glue);
14     stats.promoted2++;
15     c->used = 2;
16   } else if (c->keep)
17     LOG (c, "keeping with new glue %d in tier1", new_glue);
18   else if (old_glue <= opts.reducetier2glue)
19     LOG (c, "keeping with new glue %d in tier2", new_glue);
20   else
21     LOG (c, "keeping with new glue %d in tier3", new_glue);
22   stats.improvedglue++;
23   c->glue = new_glue;
24 }

 

   
   
 1 // Shrinking a clause, e.g., removing one or more literals, requires to fix
 2 // the ‘pos‘ field, if it exists and points after the new last literal, has
 3 // to adjust the global statistics counter of allocated bytes for
 4 // irredundant clauses, and also adjust the glue value of redundant clauses
 5 // if the size becomes smaller than the glue.  Also mark the literals in the
 6 // resulting clause as ‘added‘.  The result is the number of (aligned)
 7 // removed bytes, resulting from shrinking the clause.
 8 //
 9 size_t Internal::shrink_clause (Clause * c, int new_size) {
10 
11   assert (new_size >= 2);
12   assert (new_size < c->size);
13 #ifndef NDEBUG
14   for (int i = c->size; i < new_size; i++)
15     c->literals[i] = 0;
16 #endif
17 
18   if (c->pos >= new_size) c->pos = 2;
19 
20   size_t old_bytes = c->bytes ();
21   c->size = new_size;
22   size_t new_bytes = c->bytes ();
23   size_t res = old_bytes - new_bytes;
24 
25   if (c->redundant) promote_clause (c, min (c->size-1, c->glue));
26   else if (old_bytes > new_bytes) {
27     assert (stats.irrbytes >= (int64_t) res);
28     stats.irrbytes -= res;
29   }
30 
31   if (likely_to_be_kept_clause (c)) mark_added (c);
32 
33   return res;
34 }

 

   
   
 1 // This is the ‘raw‘ deallocation of a clause.  If the clause is in the
 2 // arena nothing happens.  If the clause is not in the arena its memory is
 3 // reclaimed immediately.
 4 
 5 void Internal::deallocate_clause (Clause * c) {
 6   char * p = (char*) c;
 7   if (arena.contains (p)) return;
 8   LOG (c, "deallocate pointer %p", c);
 9   delete [] p;
10 }
11 
12 void Internal::delete_clause (Clause * c) {
13   LOG (c, "delete pointer %p", c);
14   size_t bytes = c->bytes ();
15   stats.collected += bytes;
16   if (c->garbage) {
17     assert (stats.garbage >= (int64_t) bytes);
18     stats.garbage -= bytes;
19 
20     // See the discussion in ‘propagate‘ on avoiding to eagerly trace binary
21     // clauses as deleted (produce ‘d ...‘ lines) as soon they are marked
22     // garbage.  We avoid this and only trace them as deleted when they are
23     // actually deleted here.  This allows the solver to propagate binary
24     // garbage clauses without producing incorrect ‘d‘ lines.  The effect
25     // from the proof perspective is that the deletion of these binary
26     // clauses occurs later in the proof file.
27     //
28     if (proof && c->size == 2)
29       proof->delete_clause (c);
30   }
31   deallocate_clause (c);
32 }
33 
34 // We want to eagerly update statistics as soon clauses are marked garbage.
35 // Otherwise ‘report‘ for instance gives wrong numbers after ‘subsume‘
36 // before the next ‘reduce‘.  Thus we factored out marking and accounting
37 // for garbage clauses.
38 //
39 // Eagerly deleting clauses instead is problematic, since references to these
40 // clauses need to be flushed, which is too costly to do eagerly.
41 //
42 // We also update garbage statistics at this point.  This helps to
43 // determine whether the garbage collector should be called during for
44 // instance bounded variable elimination, which usually generates lots of
45 // garbage clauses.
46 //
47 // In order not to miss any update to these clause statistics we call
48 // ‘check_clause_stats‘ after garbage collection in debugging mode.
49 //
50 void Internal::mark_garbage (Clause * c) {
51 
52   assert (!c->garbage);
53 
54   // Delay tracing deletion of binary clauses.  See the discussion above in
55   // ‘delete_clause‘ and also in ‘propagate‘.
56   //
57   if (proof && c->size != 2)
58     proof->delete_clause (c);
59 
60   assert (stats.current.total > 0);
61   stats.current.total--;
62 
63   size_t bytes = c->bytes ();
64   if (c->redundant) {
65     assert (stats.current.redundant > 0);
66     stats.current.redundant--;
67   } else {
68     assert (stats.current.irredundant > 0);
69     stats.current.irredundant--;
70     assert (stats.irrbytes >= (int64_t) bytes);
71     stats.irrbytes -= bytes;
72     mark_removed (c);
73   }
74   stats.garbage += bytes;
75   c->garbage = true;
76   c->used = 0;
77 
78   LOG (c, "marked garbage pointer %p", c);
79 }

 

   
原始子句相关操作
 
 1 // Almost the same function as ‘search_assign‘ except that we do not pretend
 2 // to learn a new unit clause (which was confusing in log files).
 3 
 4 void Internal::assign_original_unit (int lit) {
 5   assert (!level);
 6   const int idx = vidx (lit);
 7   assert (!vals[idx]);
 8   assert (!flags (idx).eliminated ());
 9   Var & v = var (idx);
10   v.level = level;
11   v.trail = (int) trail.size ();
12   v.reason = 0;
13   const signed char tmp = sign (lit);
14   vals[idx] = tmp;
15   vals[-idx] = -tmp;
16   assert (val (lit) > 0);
17   assert (val (-lit) < 0);
18   trail.push_back (lit);
19   LOG ("original unit assign %d", lit);
20   mark_fixed (lit);
21   if (propagate ()) return;
22   LOG ("propagation of original unit results in conflict");
23   learn_empty_clause ();
24 }

 

   
 
 1 // New clause added through the API, e.g., while parsing a DIMACS file.
 2 //
 3 void Internal::add_new_original_clause () {
 4   if (level) backtrack ();
 5   LOG (original, "original clause");
 6   bool skip = false;
 7   if (unsat) {
 8     LOG ("skipping clause since formula already inconsistent");
 9     skip = true;
10   } else {
11     assert (clause.empty ());
12     for (const auto & lit : original) {
13       int tmp = marked (lit);
14       if (tmp > 0) {
15         LOG ("removing duplicated literal %d", lit);
16       } else if (tmp < 0) {
17         LOG ("tautological since both %d and %d occur", -lit, lit);
18         skip = true;
19       } else {
20         mark (lit);
21         tmp = val (lit);
22         if (tmp < 0) {
23           LOG ("removing falsified literal %d", lit);
24         } else if (tmp > 0) {
25           LOG ("satisfied since literal %d true", lit);
26           skip = true;
27         } else {
28           clause.push_back (lit);
29           assert (flags (lit).status != Flags::UNUSED);
30         }
31       }
32     }
33     for (const auto & lit : original)
34       unmark (lit);
35   }
36   if (skip) {
37     if (proof) proof->delete_clause (original);
38   } else {
39     size_t size = clause.size ();
40     if (!size) {
41       if (!unsat) {
42         if (!original.size ()) VERBOSE (1, "found empty original clause");
43         else MSG ("found falsified original clause");
44         unsat = true;
45       }
46     } else if (size == 1) {
47       assign_original_unit (clause[0]);
48     } else {
49       Clause * c = new_clause (false);
50       watch_clause (c);
51     }
52     if (original.size () > size) {
53       external->check_learned_clause ();
54       if (proof) {
55         proof->add_derived_clause (clause);
56         proof->delete_clause (original);
57       }
58     }
59   }
60   clause.clear ();
61 }

 

   
 
 1 // Add learned new clause during conflict analysis and watch it. Requires
 2 // that the clause is at least of size 2, and the first two literals
 3 // are assigned at the highest decision level.
 4 //
 5 Clause * Internal::new_learned_redundant_clause (int glue) {
 6   assert (clause.size () > 1);
 7 #ifndef NDEBUG
 8   for (size_t i = 2; i < clause.size (); i++)
 9     assert (var (clause[0]).level >= var (clause[i]).level),
10     assert (var (clause[1]).level >= var (clause[i]).level);
11 #endif
12   external->check_learned_clause ();
13   Clause * res = new_clause (true, glue);
14   if (proof) proof->add_derived_clause (res);
15   assert (watching ());
16   watch_clause (res);
17   return res;
18 }

 

   
 
 1 // Add hyper binary resolved clause during ‘probing‘.
 2 //
 3 Clause * Internal::new_hyper_binary_resolved_clause (bool red, int glue) {
 4   external->check_learned_clause ();
 5   Clause * res = new_clause (red, glue);
 6   if (proof) proof->add_derived_clause (res);
 7   assert (watching ());
 8   watch_clause (res);
 9   return res;
10 }

 

   
 
 1 // Add hyper ternary resolved clause during ‘ternary‘.
 2 //
 3 Clause * Internal::new_hyper_ternary_resolved_clause (bool red) {
 4   external->check_learned_clause ();
 5   size_t size = clause.size ();
 6   Clause * res = new_clause (red, size);
 7   if (proof) proof->add_derived_clause (res);
 8   assert (!watching ());
 9   return res;
10 }

 

   
 
 1 // Add a new clause with same glue and redundancy as ‘orig‘ but literals are
 2 // assumed to be in ‘clause‘ in ‘decompose‘ and ‘vivify‘.
 3 //
 4 Clause * Internal::new_clause_as (const Clause * orig) {
 5   external->check_learned_clause ();
 6   const int new_glue = orig->glue;
 7   Clause * res = new_clause (orig->redundant, new_glue);
 8   assert (!orig->redundant || !orig->keep || res->keep);
 9   if (proof) proof->add_derived_clause (res);
10   assert (watching ());
11   watch_clause (res);
12   return res;
13 }

 

   
 
 1 // Add resolved clause during resolution, e.g., bounded variable
 2 // elimination, but do not connect its occurrences here.
 3 //
 4 Clause * Internal::new_resolved_irredundant_clause () {
 5   external->check_learned_clause ();
 6   Clause * res = new_clause (false);
 7   if (proof) proof->add_derived_clause (res);
 8   assert (!watching ());
 9   return res;
10 }

 

   

5.CaDiCal代码解读——CaDiCal的internal相关代码--clause.hpp--clause.cpp

标签:next   factor   orm   gen   计数   alt   size   mem   numbers   

原文地址:https://www.cnblogs.com/yuweng1689/p/13399372.html

(0)
(0)
   
举报
评论 一句话评论(0
登录后才能评论!
© 2014 mamicode.com 版权所有  联系我们:gaon5@hotmail.com
迷上了代码!