1 #include "internal.hpp"
  2 
  3 namespace CaDiCaL {
  4 
  5 /*------------------------------------------------------------------------*/
  6 
  7 // In incremental solving after a first call to 'solve' has finished and
  8 // before calling the internal 'solve' again incrementally we have to
  9 // restore clauses which have the negation of a literal as a witness literal
 10 // on the extension stack, which was added as original literal in a new
 11 // clause or in an assumption.  This procedure has to be applied
 12 // recursively, i.e., the literals of restored clauses are treated in the
 13 // same way as literals of a new original clause.
 14 //
 15 // To figure out whether literals are such witnesses we have a 'witness'
 16 // bit for each external literal, which is set in 'block', 'elim', and
 17 // 'decompose' if a clause is pushed on the extension stack.  The witness
 18 // bits are recomputed after restoring clauses.
 19 //
 20 // We further mark in the external solver newly internalized external
 21 // literals in 'add' and 'assume' since the last call to 'solve' as tainted
 22 // if they occur negated as a witness literal on the extension stack.  Then
 23 // we go through the extension stack and restore all clauses which have a
 24 // tainted literal (and its negation a marked as witness).
 25 //
 26 // Since the API contract disallows to call 'val' and 'failed' in an
 27 // 'UNKNOWN' state. We do not have to internalize literals there.
 28 //
 29 // In order to have tainted literals accepted by the internal solver they
 30 // have to be active and thus we might need to 'reactivate' them before
 31 // restoring clauses if they are inactive. In case they have completely
 32 // been eliminated and removed from the internal solver in 'compact', then
 33 // we just use a new internal variable.  This is performed in 'internalize'
 34 // during marking external literals as tainted.
 35 //
 36 // To check that this approach is correct the external solver can maintain a
 37 // stack of original clauses and current assumptions both in terms of
 38 // external literals.  Whenever 'solve' determines that the current
 39 // incremental call is satisfiable we check that the (extended) witness does
 40 // satisfy the saved original clauses, as well as all the assumptions. To
 41 // enable these checks set 'opts.check' as well as 'opts.checkwitness' and
 42 // 'opts.checkassumptions' all to 'true'.  The model based tester actually
 43 // prefers to enable the 'opts.check' option and the other two are 'true' by
 44 // default anyhow.
 45 //
 46 // See our SAT'19 paper [FazekasBiereScholl-SAT'19] for more details.
 47 
 48 /*------------------------------------------------------------------------*/
 49 
 50 void External::restore_clause (
 51   const vector<int>::const_iterator & begin,
 52   const vector<int>::const_iterator & end) {
 53   LOG (begin, end, "restoring external clause");
 54   for (auto p = begin; p != end; p++) {
 55     int ilit = internalize (*p);
 56     internal->add_original_lit (ilit);
 57     internal->stats.restoredlits++;
 58   }
 59   internal->add_original_lit (0);
 60   internal->stats.restored++;
 61 }
 62 
 63 /*------------------------------------------------------------------------*/
 64 
 65 void External::restore_clauses () {
 66 
 67   assert (internal->opts.restoreall == 2 || !tainted.empty ());
 68 
 69   START (restore);
 70   internal->stats.restorations++;
 71 
 72   struct { int64_t weakened, satisfied, restored, removed; } clauses;
 73   memset (&clauses, 0, sizeof clauses);
 74 
 75   if (internal->opts.restoreall && tainted.empty ())
 76     PHASE ("restore", internal->stats.restorations,
 77       "forced to restore all clauses");
 78 
 79   unsigned numtainted = 0;
 80   for (const auto & b : tainted)
 81     if (b) numtainted++;
 82 
 83   PHASE ("restore", internal->stats.restorations,
 84     "starting with %zd tainted literals %.0f%%",
 85     numtainted, percent (numtainted, 2u*max_var));
 86 
 87   auto end_of_extension = extension.end ();
 88   auto p = extension.begin (), q = p;
 89 
 90   // Go over all witness labelled clauses on the extension stack, restore
 91   // those necessary, remove restored and flush satisfied clauses.
 92   //
 93   while (p != end_of_extension) {
 94 
 95     clauses.weakened++;
 96 
 97     assert (!*p);
 98     const auto saved = q;                       // Save old start.
 99     *q++ = *p++;                                // Copy zero '0'.
100 
101     // Copy witness part and try to find a tainted witness literal in it.
102     //
103     int tlit = 0;                               // Negation tainted.
104     int elit;
105     //
106     assert (p != end_of_extension);
107     //
108     while ((elit = *q++ = *p++)) {
109 
110       if (marked (tainted, -elit)) {
111         tlit = elit;
112         LOG ("negation of witness literal %d tainted", tlit);
113       }
114 
115       assert (p != end_of_extension);
116     }
117 
118     // Now find 'end_of_clause' (clause starts at 'p') and at the same time
119     // figure out whether the clause is actually root level satisfied.
120     //
121     int satisfied = 0;
122     auto end_of_clause = p;
123     while (end_of_clause != end_of_extension && (elit = *end_of_clause)) {
124       if (!satisfied && fixed (elit) > 0)
125         satisfied = elit;
126       end_of_clause++;
127     }
128 
129     // Do not apply our 'FLUSH' rule to remove satisfied (implied) clauses
130     // if the corresponding option is set simply by resetting 'satisfied'.
131     //
132     if (satisfied && !internal->opts.restoreflush) {
133       LOG (p, end_of_clause,
134         "forced to not remove %d satisfied", satisfied);
135       satisfied = 0;
136     }
137 
138     if (satisfied || tlit || internal->opts.restoreall) {
139 
140       if (satisfied) {
141         LOG (p, end_of_clause,
142           "flushing implied clause satisfied by %d from extension stack",
143           satisfied);
144         clauses.satisfied++;
145       } else {
146         restore_clause (p, end_of_clause);      // Might taint literals.
147         clauses.restored++;
148       }
149 
150       clauses.removed++;
151       p = end_of_clause;
152       q = saved;
153 
154     } else {
155 
156       LOG (p, end_of_clause, "keeping clause on extension stack");
157 
158       while (p != end_of_clause)                // Copy clause too.
159         *q++ = *p++;
160     }
161   }
162 
163   extension.resize (q - extension.begin ());
164   shrink_vector (extension);
165 
166 #ifndef QUIET
167   if (clauses.satisfied)
168     PHASE ("restore", internal->stats.restorations,
169       "removed %" PRId64 " satisfied %.0f%% of %" PRId64 " weakened clauses",
170       clauses.satisfied,
171       percent (clauses.satisfied, clauses.weakened),
172       clauses.weakened);
173   else
174     PHASE ("restore", internal->stats.restorations,
175       "no satisfied clause removed out of %" PRId64 " weakened clauses",
176       clauses.weakened);
177 
178   if (clauses.restored)
179     PHASE ("restore", internal->stats.restorations,
180       "restored %" PRId64 " clauses %.0f%% out of %" PRId64 " weakened clauses",
181       clauses.restored,
182       percent (clauses.restored, clauses.weakened),
183       clauses.weakened);
184   else
185     PHASE ("restore", internal->stats.restorations,
186       "no clause restored out of %" PRId64 " weakened clauses",
187       clauses.weakened);
188 #endif
189 
190   numtainted = 0;
191   for (const auto & b : tainted)
192     if (b) numtainted++;
193 
194   PHASE ("restore", internal->stats.restorations,
195     "finishing with %zd tainted literals %.0f%%",
196     numtainted, percent (numtainted, 2u*max_var));
197 
198   LOG ("extension stack clean");
199   tainted.clear ();
200 
201   // Finally recompute the witness bits.
202   //
203   witness.clear ();
204   const auto begin_of_extension = extension.begin ();
205   p = extension.end ();
206   while (p != begin_of_extension) {
207     while (*--p)
208       assert (p != begin_of_extension);
209     int elit;
210     assert (p != begin_of_extension);
211     while ((elit = *--p)) {
212       mark (witness, elit);
213       assert (p != begin_of_extension);
214     }
215   }
216 
217   STOP (restore);
218 }
219 
220 }