learn.c File Reference

#include "learn.h"
#include "backtrack.h"
#include "inline.h"
#include "reluctant.h"
#include <inttypes.h>

Include dependency graph for learn.c:

Go to the source code of this file.

Functions
unsigned	kissat_determine_new_level (kissat *solver, unsigned jump)
void	kissat_update_learned (kissat *solver, unsigned glue, unsigned size)
void	kissat_learn_clause (kissat *solver)

Function Documentation

kissat_determine_new_level()

unsigned kissat_determine_new_level	(	kissat *	solver,
		unsigned	jump )

Definition at line 18 of file learn.c.

                                                                    {
  KISSAT_assert (solver->level);
  const unsigned back = solver->level - 1;
  KISSAT_assert (jump <= back);
 
  const unsigned delta = back - jump;
  const unsigned limit = backjump_limit (solver);
 
  unsigned res;
 
  if (!delta) {
    res = jump;
    LOG ("using identical backtrack and jump level %u", res);
  } else if (delta > limit) {
    res = back;
    LOG ("backjumping over %u levels (%u - %u) considered inefficient",
         delta, back, jump);
    LOG ("backtracking chronologically to backtrack level %u", res);
    INC (chronological);
  } else {
    res = jump;
    LOG ("backjumping over %u levels (%u - %u) considered efficient", delta,
         back, jump);
    LOG ("backjumping non-chronologically to jump level %u", res);
  }
  return res;
}

kissat_learn_clause()

void kissat_learn_clause

(

kissat *

solver

)

Definition at line 192 of file learn.c.

                                          {
  const unsigned not_uip = PEEK_STACK (solver->clause, 0);
  const unsigned size = SIZE_STACK (solver->clause);
  const size_t glue = SIZE_STACK (solver->levels);
  KISSAT_assert (glue <= UINT_MAX);
  if (!solver->probing)
    kissat_update_learned (solver, glue, size);
  KISSAT_assert (size > 0);
  reference ref = INVALID_REF;
  if (size == 1)
    learn_unit (solver, not_uip);
  else if (size == 2)
    learn_binary (solver, not_uip);
  else
    ref = learn_reference (solver, not_uip, glue);
  if (GET_OPTION (eagersubsume)) {
    eagerly_subsume_last_learned (solver);
    if (ref != INVALID_REF)
      insert_last_learned (solver, ref);
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

kissat_update_learned()

void kissat_update_learned	(	kissat *	solver,
		unsigned	glue,
		unsigned	size )

Definition at line 120 of file learn.c.

                                                                          {
  KISSAT_assert (!solver->probing);
  INC (clauses_learned);
  LOG ("learned[%" PRIu64 "] clause glue %u size %u", GET (clauses_learned),
       glue, size);
  if (solver->stable)
    kissat_tick_reluctant (&solver->reluctant);
  ADD (literals_learned, size);
#ifndef KISSAT_QUIET
  UPDATE_AVERAGE (size, size);
#endif
  UPDATE_AVERAGE (fast_glue, glue);
  UPDATE_AVERAGE (slow_glue, glue);
}

Here is the call graph for this function:

Here is the caller graph for this function: