kissat分析02_主要功能函数02_reduce

海阔凭鱼跃越 / 2023-05-03 / 原文

涉及search.c、reduce.c、collect.c、clause.c等多个文件

//search.c主程序调用功能函数的流程框架

 1 int
 2 kissat_search (kissat * solver)
 3 {
 4   start_search (solver);
 5 
 6   int res = kissat_walk_initially (solver);
 7 
 8   while (!res)
 9     {
10       clause *conflict = kissat_search_propagate (solver);
11       if (conflict)
12     res = kissat_analyze (solver, conflict);
13       else if (solver->iterating)
14     iterate (solver);
15       else if (!solver->unassigned)
16     res = 10;
17       else if (TERMINATED (11))
18     break;
19       else if (conflict_limit_hit (solver))
20     break;
21       else if (kissat_reducing (solver))
22     res = kissat_reduce (solver);
23       else if (kissat_restarting (solver))
24     kissat_restart (solver);
25       else if (kissat_rephasing (solver))
26     kissat_rephase (solver);
27       else if (kissat_eliminating (solver))
28     res = kissat_eliminate (solver);
29       else if (kissat_probing (solver))
30     res = kissat_probe (solver);
31       else if (!solver->level && solver->unflushed)
32     kissat_flush_trail (solver);
33       else if (decision_limit_hit (solver))
34     break;
35       else
36     kissat_decide (solver);
37     }
38 
39   stop_search (solver, res);
40 
41   return res;
42 }

reduce.c

//判断是否达到子句集删除条件

 1 bool
 2 kissat_reducing (kissat * solver)
 3 {
 4   if (!GET_OPTION (reduce))
 5     return false;
 6   if (!solver->statistics.clauses_redundant)
 7     return false;
 8   if (CONFLICTS < solver->limits.reduce.conflicts)
 9     return false;
10   return true;
11 }

//实施删除子句

 1 int
 2 kissat_reduce (kissat * solver)
 3 {
 4   START (reduce);
 5   INC (reductions);   LOG ("beginreduce");
 6   kissat_phase (solver, "reduce", GET (reductions),
 7         "reduce limit %" PRIu64 " hit after %" PRIu64
 8         " conflicts", solver->limits.reduce.conflicts, CONFLICTS);
 9   force_restart_before_reduction (solver);
10   bool compact = compacting (solver);
11   reference start = compact ? 0 : solver->first_reducible; 
12   if (start != INVALID_REF)
13     {
14 #ifndef QUIET
15       size_t arena_size = SIZE_STACK (solver->arena);
16       size_t words_to_sweep = arena_size - start;
17       size_t bytes_to_sweep = sizeof (word) * words_to_sweep;
18       kissat_phase (solver, "reduce", GET (reductions),
19             "reducing clauses after offset %zu in arena", start);
20       kissat_phase (solver, "reduce", GET (reductions),
21             "sweeping %zu words %s %.0f%%",
22             words_to_sweep, FORMAT_BYTES (bytes_to_sweep),
23             kissat_percent (words_to_sweep, arena_size)); 
24 #endif
25       if (kissat_flush_and_mark_reason_clauses (solver, start))
26     {
27       reducibles reds;
28       INIT_STACK (reds);
29       if (collect_reducibles (solver, &reds, start))
30         {
31           sort_reducibles (solver, &reds);
32           mark_less_useful_clauses_as_garbage (solver, &reds);
33           RELEASE_STACK (reds); 
34           kissat_sparse_collect (solver, compact, start); 
35         }
36       else if (compact) 
37         kissat_sparse_collect (solver, compact, start); 
38       else 
39         kissat_unmark_reason_clauses (solver, start); 
40     }
41       else
42     assert (solver->inconsistent);
43     }
44   else
45     kissat_phase (solver, "reduce", GET (reductions), "nothing to reduce");
46   UPDATE_CONFLICT_LIMIT (reduce, reductions, NDIVLOGN, false); 
47   REPORT (0, '-');
48   STOP (reduce);
49   return solver->inconsistent ? 20 : 0;
50 }

//collect.c

void
kissat_sparse_collect (kissat * solver, bool compact, reference start)
{
  assert (solver->watching);
  START (collect);
  INC (garbage_collections);
  INC (sparse_garbage_collections);
  REPORT (1, 'G');
  unsigned vars, mfixed;     
  if (compact)
    vars = kissat_compact_literals (solver, &mfixed);
  else
    {
      vars = solver->vars;
      mfixed = INVALID_LIT;
    }      
  flush_all_watched_clauses (solver, compact, start); 
  reference move = sparse_sweep_garbage_clauses (solver, compact, start);
  if (compact)
    kissat_finalize_compacting (solver, vars, mfixed);  
  if (move != INVALID_REF)
    move_redundant_clauses_to_the_end (solver, move); 
 
  rewatch_clauses (solver, start);  
  REPORT (1, 'C');
  kissat_check_statistics (solver);
  STOP (collect);
}

//clause.c

static void
mark_clause_as_garbage (kissat * solver, clause * c)
{
  assert (!c->garbage);
  LOGCLS (c, "garbage");
  if (!c->redundant)
    kissat_mark_removed_literals (solver, c->size, c->lits);
  REMOVE_CHECKER_CLAUSE (c);
  DELETE_CLAUSE_FROM_PROOF (c);
  if (c->hyper)
    {
      assert (c->size == 3);
      assert (c->redundant);
      DEC (hyper_ternaries);
    }
  dec_clause (solver, c->redundant);
  c->garbage = true;
}


void
kissat_mark_clause_as_garbage (kissat * solver, clause * c)
{
  assert (!c->garbage);
  mark_clause_as_garbage (solver, c);
  size_t bytes = kissat_actual_bytes_of_clause (c);
  ADD (arena_garbage, bytes);
}


clause *
kissat_delete_clause (kissat * solver, clause * c)
{
  LOGCLS (c, "delete");
  assert (c->size > 2);
  assert (c->garbage);
  size_t bytes = kissat_actual_bytes_of_clause (c);
  SUB (arena_garbage, bytes);
  INC (clauses_deleted);
  return (clause *) ((char *) c + bytes);
}


void
kissat_delete_binary (kissat * solver,
              bool redundant, bool hyper, unsigned a, unsigned b)
{
  LOGBINARY (a, b, "delete");
  if (!redundant)
    {
      kissat_mark_removed_literal (solver, a);
      kissat_mark_removed_literal (solver, b);
    }
  else if (hyper)
    DEC (hyper_binaries);
  REMOVE_CHECKER_BINARY (a, b);
  DELETE_BINARY_FROM_PROOF (a, b);
  dec_clause (solver, redundant);
  INC (clauses_deleted);
}