decide.c

Go to the documentation of this file.

#include "decide.h"
#include "inlineframes.h"
#include "inlineheap.h"
#include "inlinequeue.h"
#include "print.h"
 
#include <inttypes.h>
 
ABC_NAMESPACE_IMPL_START
 
static unsigned last_enqueued_unassigned_variable (kissat *solver) {
  KISSAT_assert (solver->unassigned);
  const links *const links = solver->links;
  const value *const values = solver->values;
  unsigned res = solver->queue.search.idx;
  if (values[LIT (res)]) {
    do {
      res = links[res].prev;
      KISSAT_assert (!DISCONNECTED (res));
    } while (values[LIT (res)]);
    kissat_update_queue (solver, links, res);
  }
#ifdef LOGGING
  const unsigned stamp = links[res].stamp;
  LOG ("last enqueued unassigned %s stamp %u", LOGVAR (res), stamp);
#endif
#ifdef CHECK_QUEUE
  for (unsigned i = links[res].next; !DISCONNECTED (i); i = links[i].next)
    KISSAT_assert (VALUE (LIT (i)));
#endif
  return res;
}
 
static unsigned largest_score_unassigned_variable (kissat *solver) {
  heap *scores = SCORES;
  unsigned res = kissat_max_heap (scores);
  const value *const values = solver->values;
  while (values[LIT (res)]) {
    kissat_pop_max_heap (solver, scores);
    res = kissat_max_heap (scores);
  }
#if defined(LOGGING) || defined(CHECK_HEAP)
  const double score = kissat_get_heap_score (scores, res);
#endif
  LOG ("largest score unassigned %s score %g", LOGVAR (res), score);
#ifdef CHECK_HEAP
  for (all_variables (idx)) {
    if (!ACTIVE (idx))
      continue;
    if (VALUE (LIT (idx)))
      continue;
    const double idx_score = kissat_get_heap_score (scores, idx);
    KISSAT_assert (score >= idx_score);
  }
#endif
  return res;
}
 
void kissat_start_random_sequence (kissat *solver) {
  if (!GET_OPTION (randec))
    return;
 
  if (solver->stable && !GET_OPTION (randecstable))
    return;
 
  if (!solver->stable && !GET_OPTION (randecfocused))
    return;
 
  if (solver->randec)
    kissat_very_verbose (solver,
                         "continuing random decision sequence "
                         "at %s conflicts",
                         FORMAT_COUNT (CONFLICTS));
  else {
    INC (random_sequences);
    const uint64_t count = solver->statistics_.random_sequences;
    const unsigned length = GET_OPTION (randeclength) * LOGN (count);
    kissat_very_verbose (solver,
                         "starting random decision sequence "
                         "at %s conflicts for %s conflicts",
                         FORMAT_COUNT (CONFLICTS), FORMAT_COUNT (length));
    solver->randec = length;
 
    UPDATE_CONFLICT_LIMIT (randec, random_sequences, LOGN, false);
  }
}
 
static unsigned next_random_decision (kissat *solver) {
  if (!VARS)
    return INVALID_IDX;
 
  if (solver->warming)
    return INVALID_IDX;
 
  if (!GET_OPTION (randec))
    return INVALID_IDX;
 
  if (solver->stable && !GET_OPTION (randecstable))
    return INVALID_IDX;
 
  if (!solver->stable && !GET_OPTION (randecfocused))
    return INVALID_IDX;
 
  if (!solver->randec) {
    KISSAT_assert (solver->level);
    if (solver->level > 1)
      return INVALID_IDX;
 
    uint64_t conflicts = CONFLICTS;
    limits *limits = &solver->limits;
    if (conflicts < limits->randec.conflicts)
      return INVALID_IDX;
 
    kissat_start_random_sequence (solver);
  }
 
  for (;;) {
    unsigned idx = kissat_next_random32 (&solver->random) % VARS;
    if (!ACTIVE (idx))
      continue;
    unsigned lit = LIT (idx);
    if (solver->values[lit])
      continue;
    return idx;
  }
}
 
unsigned kissat_next_decision_variable (kissat *solver) {
#ifdef LOGGING
  const char *type = 0;
#endif
  unsigned res = next_random_decision (solver);
  if (res == INVALID_IDX) {
    if (solver->stable) {
#ifdef LOGGING
      type = "maximum score";
#endif
      res = largest_score_unassigned_variable (solver);
      INC (score_decisions);
    } else {
#ifdef LOGGING
      type = "dequeued";
#endif
      res = last_enqueued_unassigned_variable (solver);
      INC (queue_decisions);
    }
  } else {
#ifdef LOGGING
    type = "random";
#endif
    INC (random_decisions);
  }
  LOG ("next %s decision %s", type, LOGVAR (res));
  return res;
}
 
int kissat_decide_phase (kissat *solver, unsigned idx) {
  bool force = GET_OPTION (forcephase);
 
  value *target;
  if (force)
    target = 0;
  else if (!GET_OPTION (target))
    target = 0;
  else if (solver->stable || GET_OPTION (target) > 1)
    target = solver->phases.target + idx;
  else
    target = 0;
 
  value *saved;
  if (force)
    saved = 0;
  else if (GET_OPTION (phasesaving))
    saved = solver->phases.saved + idx;
  else
    saved = 0;
 
  value res = 0;
 
  if (!solver->stable) {
    switch ((solver->statistics_.switched >> 1) & 7) {
    case 1:
      res = INITIAL_PHASE;
      break;
    case 3:
      res = -INITIAL_PHASE;
      break;
    }
  }
 
  if (!res && target && (res = *target)) {
    LOG ("%s uses target decision phase %d", LOGVAR (idx), (int) res);
    INC (target_decisions);
  }
 
  if (!res && saved && (res = *saved)) {
    LOG ("%s uses saved decision phase %d", LOGVAR (idx), (int) res);
    INC (saved_decisions);
  }
 
  if (!res) {
    res = INITIAL_PHASE;
    LOG ("%s uses initial decision phase %d", LOGVAR (idx), (int) res);
    INC (initial_decisions);
  }
  KISSAT_assert (res);
 
  return res < 0 ? -1 : 1;
}
 
void kissat_decide (kissat *solver) {
  START (decide);
  KISSAT_assert (solver->unassigned);
  if (solver->warming)
    INC (warming_decisions);
  else {
    INC (decisions);
    if (solver->stable)
      INC (stable_decisions);
    else
      INC (focused_decisions);
  }
  solver->level++;
  KISSAT_assert (solver->level != INVALID_LEVEL);
  const unsigned idx = kissat_next_decision_variable (solver);
  const value value = kissat_decide_phase (solver, idx);
  unsigned lit = LIT (idx);
  if (value < 0)
    lit = NOT (lit);
  kissat_push_frame (solver, lit);
  KISSAT_assert (solver->level < SIZE_STACK (solver->frames));
  LOG ("decide literal %s", LOGLIT (lit));
  kissat_assign_decision (solver, lit);
  STOP (decide);
}
 
void kissat_internal_assume (kissat *solver, unsigned lit) {
  KISSAT_assert (solver->unassigned);
  KISSAT_assert (!VALUE (lit));
  solver->level++;
  KISSAT_assert (solver->level != INVALID_LEVEL);
  kissat_push_frame (solver, lit);
  KISSAT_assert (solver->level < SIZE_STACK (solver->frames));
  LOG ("assuming literal %s", LOGLIT (lit));
  kissat_assign_decision (solver, lit);
}
 
ABC_NAMESPACE_IMPL_END