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

重启涉及的物理量

重启涉及的物理量
solver->heuristic
solver->mab
solver->statistics.restarts

limits *limits = &solver->limits;
limits->restart.conflicts

还涉及相关reuse_trail
const unsigned next_idx = kissat_next_decision_variable (solver);
const links *links = solver->links;
const unsigned next_idx_stamp = links[next_idx].stamp;
LOG ("next decision variable stamp %u", next_idx_stamp);

判断重启的条件

 1 bool
 2 kissat_restarting (kissat * solver)
 3 {
 4   assert (solver->unassigned);
 5   if (!GET_OPTION (restart))
 6     return false;
 7   if (!solver->level)
 8     return false;
 9   if (CONFLICTS < solver->limits.restart.conflicts)
10     return false;
11   kissat_switch_search_mode (solver);
12   if (solver->stable)
13     return kissat_reluctant_triggered (&solver->reluctant);
14   const double fast = AVERAGE (fast_glue);
15   const double slow = AVERAGE (slow_glue);
16   const double margin = (100.0 + GET_OPTION (restartmargin)) / 100.0;
17   const double limit = margin * slow;
18   LOG ("restart glue limit %g = %.02f * %g (slow glue) %c %g (fast glue)",
19        limit, margin, slow,
20        (limit > fast ? '>' : limit == fast ? '=' : '<'), fast);
21   return limit <= fast;
22 }

实施重启的函数

 1 void
 2 kissat_restart (kissat * solver)
 3 {
 4   START (restart);  
 5   INC (restarts);
 6   
 7   unsigned old_heuristic = solver->heuristic;
 8   if (solver->stable && solver->mab) 
 9      restart_mab(solver);
10   unsigned new_heuristic = solver->heuristic;
11 
12   unsigned level = old_heuristic==new_heuristic?reuse_trail (solver):0;
13 
14   kissat_extremely_verbose (solver,
15                 "restarting after %" PRIu64 " conflicts"
16                 " (scheduled at %" PRIu64 ")",
17                 CONFLICTS, solver->limits.restart.conflicts);
18   LOG ("restarting to level %u", level);
19 
20   if (solver->stable && solver->mab) solver->heuristic = old_heuristic;
21   kissat_backtrack (solver, level);
22   if (solver->stable && solver->mab) solver->heuristic = new_heuristic;
23 
24   if (!solver->stable)
25     kissat_new_focused_restart_limit (solver);
26 
27   if (solver->stable && solver->mab && old_heuristic!=new_heuristic) 
       kissat_update_scores(solver);
28 
29   REPORT (1, 'R');
30   STOP (restart); 
31 }

其中，restart_mab(solver)实施重启；其余几个函数是辅助功能。

526互联

kissat分析02_主要功能函数03_restart