kissat分析02_主要功能函数01_propagate

#ifndef _propsearch_h_INCLUDED
#define _propsearch_h_INCLUDED

struct kissat;
struct clause;

struct clause *kissat_search_propagate (struct kissat *);

#endif

#define INLINE_ASSIGN

#include "inline.h"
#include "propsearch.h"
#include "bump.h"

// Keep this 'inlined' file separate:

#include "assign.c"

#define PROPAGATE_LITERAL search_propagate_literal
#define PROPAGATION_TYPE "search"

#include "proplit.h"

static inline void
update_search_propagation_statistics (kissat * solver,
                      unsigned previous_propagated_level)
{
  assert (previous_propagated_level <= solver->propagated);
  const unsigned propagated = solver->propagated - previous_propagated_level;

  LOG ("propagation took %" PRIu64 " propagations", propagated);
  LOG ("propagation took %" PRIu64 " ticks", solver->ticks);

  ADD (propagations, propagated);
  ADD (ticks, solver->ticks);

  ADD (search_propagations, propagated);
  ADD (search_ticks, solver->ticks);

  if (solver->stable)
    {
      ADD (stable_propagations, propagated);
      ADD (stable_ticks, solver->ticks);
    }
  else
    {
      ADD (focused_propagations, propagated);
      ADD (focused_ticks, solver->ticks);
    }
}

static inline void
update_consistently_assigned (kissat * solver)
{
  const unsigned assigned = kissat_assigned (solver);
  if (assigned != solver->consistently_assigned)
    {
      LOG ("updating consistently assigned from %u to %u",
       solver->consistently_assigned, assigned);
      solver->consistently_assigned = assigned;
    }
  else
    LOG ("keeping consistently assigned %u", assigned);
}

static clause *
search_propagate (kissat * solver)
{
  clause *res = 0;
  while (!res && solver->propagated < SIZE_STACK (solver->trail))
    {
      const unsigned lit = PEEK_STACK (solver->trail, solver->propagated);
      res = search_propagate_literal (solver, lit);
      solver->propagated++;
    }
  return res;
}




clause *
kissat_search_propagate (kissat * solver)
{
  assert (!solver->probing);
  assert (solver->watching);
  assert (!solver->inconsistent);

  START (propagate);

  solver->ticks = 0;
  const unsigned propagated = solver->propagated;
  clause *conflict = search_propagate (solver);
  update_search_propagation_statistics (solver, propagated);
  update_consistently_assigned (solver);
  if (conflict)
    INC (conflicts);
  STOP (propagate);

  // CHB
  if(solver->stable && solver->heuristic==1){
      int i = SIZE_STACK (solver->trail) - 1;
      unsigned lit = i>=0?PEEK_STACK (solver->trail, i):0;  
      while(i>=0 && LEVEL(lit)==solver->level){
        lit = PEEK_STACK (solver->trail, i);
            kissat_bump_chb(solver,IDX(lit), conflict? 1.0 : 0.9); 
        i--;        
      }
  }  
  if(solver->stable && solver->heuristic==1 && conflict) kissat_decay_chb(solver);

  return conflict;
}

  1 static inline clause *
  2 PROPAGATE_LITERAL (kissat * solver,
  3 #if defined(HYPER_PROPAGATION) || defined(PROBING_PROPAGATION)
  4            const clause * ignore,
  5 #endif
  6            const unsigned lit)
  7 {
  8   assert (solver->watching);
  9   LOG (PROPAGATION_TYPE " propagating %s", LOGLIT (lit));
 10   assert (VALUE (lit) > 0);
 11   assert (EMPTY_STACK (solver->delayed));
 12 
 13   const word *arena = BEGIN_STACK (solver->arena);
 14   assigned *assigned = solver->assigned;
 15   value *values = solver->values;
 16 
 17   const unsigned not_lit = NOT (lit);
 18 #ifdef HYPER_PROPAGATION
 19   const bool hyper = GET_OPTION (hyper);
 20 #endif
 21   watches *watches = &WATCHES (not_lit);
 22   watch *begin_watches = BEGIN_WATCHES (*watches), *q = begin_watches;
 23   const watch *end_watches = END_WATCHES (*watches), *p = q;
 24   unsigneds *delayed = &solver->delayed;
 25 
 26   uint64_t ticks = kissat_cache_lines (watches->size, sizeof (watch));
 27 
 28   clause *res = 0;
 29 
 30   while (p != end_watches)
 31     {
 32       const watch head = *q++ = *p++;
 33       const unsigned blocking = head.blocking.lit;
 34       assert (VALID_INTERNAL_LITERAL (blocking));
 35       const value blocking_value = values[blocking];
 36       if (head.type.binary)
 37     {
 38       if (blocking_value > 0)
 39         continue;
 40       const bool redundant = head.binary.redundant;
 41       if (blocking_value < 0)
 42         {
 43           res = kissat_binary_conflict (solver, redundant,
 44                         not_lit, blocking);
 45           break;
 46         }
 47       else
 48         {
 49           assert (!blocking_value);
 50           kissat_assign_binary (solver, values, assigned,
 51                     redundant, blocking, not_lit);
 52         }
 53     }
 54       else
 55     {
 56       const watch tail = *q++ = *p++;
 57       if (blocking_value > 0)
 58         continue;
 59       const reference ref = tail.raw;
 60       assert (ref < SIZE_STACK (solver->arena));
 61       clause *c = (clause *) (arena + ref);
 62 #if defined(HYPER_PROPAGATION) || defined(PROBING_PROPAGATION)
 63       if (c == ignore)
 64         continue;
 65 #endif
 66       ticks++;
 67       if (c->garbage)
 68         {
 69           q -= 2;
 70           continue;
 71         }
 72       unsigned *lits = BEGIN_LITS (c);
 73       const unsigned other = lits[0] ^ lits[1] ^ not_lit;
 74       assert (lits[0] != lits[1]);
 75       assert (VALID_INTERNAL_LITERAL (other));
 76       assert (not_lit != other);
 77       assert (lit != other);
 78       const value other_value = values[other];
 79       if (other_value > 0)
 80         q[-2].blocking.lit = other;
 81       else
 82         {
 83           const unsigned *end_lits = lits + c->size;
 84           unsigned *searched = lits + c->searched;
 85           assert (c->lits + 2 <= searched);
 86           assert (searched < end_lits);
 87           unsigned *r, replacement = INVALID_LIT;
 88           value replacement_value = -1;
 89           for (r = searched; r != end_lits; r++)
 90         {
 91           replacement = *r;
 92           assert (VALID_INTERNAL_LITERAL (replacement));
 93           replacement_value = values[replacement];
 94           if (replacement_value >= 0)
 95             break;
 96         }
 97           if (replacement_value < 0)
 98         {
 99           for (r = lits + 2; r != searched; r++)
100             {
101               replacement = *r;
102               assert (VALID_INTERNAL_LITERAL (replacement));
103               replacement_value = values[replacement];
104               if (replacement_value >= 0)
105             break;
106             }
107         }
108 
109           if (replacement_value >= 0)
110         c->searched = r - c->lits;
111 
112           if (replacement_value > 0)
113         {
114           assert (replacement != INVALID_LIT);
115           q[-2].blocking.lit = replacement;
116         }
117           else if (!replacement_value)
118         {
119           assert (replacement != INVALID_LIT);
120           LOGREF (ref, "unwatching %s in", LOGLIT (not_lit));
121           q -= 2;
122           lits[0] = other;
123           lits[1] = replacement;
124           assert (lits[0] != lits[1]);
125           *r = not_lit;
126           kissat_delay_watching_large (solver, delayed,
127                            replacement, other, ref);
128           ticks++;
129         }
130           else if (other_value)
131         {
132           assert (replacement_value < 0);
133           assert (blocking_value < 0);
134           assert (other_value < 0);
135           LOGREF (ref, "conflicting");
136           res = c;
137           break;
138         }
139 #ifdef HYPER_PROPAGATION
140           else if (hyper)
141         {
142           assert (replacement_value < 0);
143           unsigned dom = kissat_find_dominator (solver, other, c);
144           if (dom != INVALID_LIT)
145             {
146               LOGBINARY (dom, other, "hyper binary resolvent");
147 
148               INC (hyper_binary_resolved);
149               INC (clauses_added);
150 
151               INC (hyper_binaries);
152               INC (clauses_redundant);
153 
154               CHECK_AND_ADD_BINARY (dom, other);
155               ADD_BINARY_TO_PROOF (dom, other);
156 
157               kissat_assign_binary (solver, values, assigned,
158                         true, other, dom);
159 
160               delay_watching_hyper (solver, delayed, dom, other);
161               delay_watching_hyper (solver, delayed, other, dom);
162 
163               kissat_delay_watching_large (solver, delayed,
164                            not_lit, other, ref);
165 
166               LOGREF (ref, "unwatching %s in", LOGLIT (not_lit));
167               q -= 2;
168             }
169           else
170             kissat_assign_reference (solver, values,
171                          assigned, other, ref, c);
172         }
173 #endif
174           else
175         {
176           assert (replacement_value < 0);
177           kissat_assign_reference (solver, values,
178                        assigned, other, ref, c);
179         }
180         }
181     }
182     }
183   solver->ticks += ticks;
184 
185   while (p != end_watches)
186     *q++ = *p++;
187   SET_END_OF_WATCHES (*watches, q);
188 
189 #ifdef HYPER_PROPAGATION
190   watch_hyper_delayed (solver, delayed);
191 #else
192   kissat_watch_large_delayed (solver, delayed);
193 #endif
194 
195   return res;
196 }