restart.c File Reference

#include "restart.h"
#include "backtrack.h"
#include "bump.h"
#include "decide.h"
#include "internal.h"
#include "kimits.h"
#include "logging.h"
#include "print.h"
#include "reluctant.h"
#include "report.h"
#include <inttypes.h>

Include dependency graph for restart.c:

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START bool	kissat_restarting (kissat *solver)
void	kissat_update_focused_restart_limit (kissat *solver)
void	kissat_restart (kissat *solver)

Function Documentation

kissat_restart()

void kissat_restart

(

kissat *

solver

)

Definition at line 114 of file restart.c.

                                     {
  START (restart);
  INC (restarts);
  ADD (restarts_levels, solver->level);
  if (solver->stable)
    INC (stable_restarts);
  else
    INC (focused_restarts);
  unsigned level = reuse_trail (solver);
  kissat_extremely_verbose (solver,
                            "restarting after %" PRIu64 " conflicts"
                            " (limit %" PRIu64 ")",
                            CONFLICTS, solver->limits.restart.conflicts);
  LOG ("restarting to level %u", level);
  kissat_backtrack_in_consistent_state (solver, level);
  if (!solver->stable)
    kissat_update_focused_restart_limit (solver);
  REPORT (1, 'R');
  STOP (restart);
}

Here is the call graph for this function:

Here is the caller graph for this function:

kissat_restarting()

ABC_NAMESPACE_IMPL_START bool kissat_restarting

(

kissat *

solver

)

Definition at line 16 of file restart.c.

                                        {
  KISSAT_assert (solver->unassigned);
  if (!GET_OPTION (restart))
    return false;
  if (!solver->level)
    return false;
  if (CONFLICTS < solver->limits.restart.conflicts)
    return false;
  if (solver->stable)
    return kissat_reluctant_triggered (&solver->reluctant);
  const double fast = AVERAGE (fast_glue);
  const double slow = AVERAGE (slow_glue);
  const double margin = (100.0 + GET_OPTION (restartmargin)) / 100.0;
  const double limit = margin * slow;
  kissat_extremely_verbose (solver,
                            "restart glue limit %g = "
                            "%.02f * %g (slow glue) %c %g (fast glue)",
                            limit, margin, slow,
                            (limit > fast    ? '>'
                             : limit == fast ? '='
                                             : '<'),
                            fast);
  return (limit <= fast);
}

Here is the caller graph for this function:

kissat_update_focused_restart_limit()

void kissat_update_focused_restart_limit

(

kissat *

solver

)

Definition at line 41 of file restart.c.

                                                          {
  KISSAT_assert (!solver->stable);
  limits *limits = &solver->limits;
  uint64_t restarts = solver->statistics_.restarts;
  uint64_t delta = GET_OPTION (restartint);
  if (restarts)
    delta += kissat_logn (restarts) - 1;
  limits->restart.conflicts = CONFLICTS + delta;
  kissat_extremely_verbose (solver,
                            "focused restart limit at %" PRIu64
                            " after %" PRIu64 " conflicts ",
                            limits->restart.conflicts, delta);
}

Here is the call graph for this function:

Here is the caller graph for this function: