CaDiCaL::Walker Struct Reference

Collaboration diagram for CaDiCaL::Walker:

Public Member Functions
double	score (unsigned)
	Walker (Internal *, double size, int64_t limit)

Public Attributes
Internal *	internal
Random	random
int64_t	propagations
int64_t	limit
vector< Clause * >	broken
double	epsilon
vector< double >	table
vector< double >	scores

Detailed Description

Definition at line 13 of file cadical_walk.cpp.

Constructor & Destructor Documentation

Walker()

CaDiCaL::Walker::Walker	(	Internal *	i,
		double	size,
		int64_t	limit )

Definition at line 67 of file cadical_walk.cpp.

    : internal (i), random (internal->opts.seed), // global random seed
      propagations (0), limit (l) {
  random += internal->stats.walk.count; // different seed every time
 
  // This is the magic constant in ProbSAT (also called 'CB'), which we pick
  // according to the average size every second invocation and otherwise
  // just the default '2.0', which turns into the base '0.5'.
  //
  const bool use_size_based_cb = (internal->stats.walk.count & 1);
  const double cb = use_size_based_cb ? fitcbval (size) : 2.0;
  CADICAL_assert (cb);
  const double base = 1 / cb; // scores are 'base^0,base^1,base^2,...
 
  double next = 1;
  for (epsilon = next; next; next = epsilon * base)
    table.push_back (epsilon = next);
 
  PHASE ("walk", internal->stats.walk.count,
         "CB %.2f with inverse %.2f as base and table size %zd", cb, base,
         table.size ());
}

Member Function Documentation

score()

double CaDiCaL::Walker::score ( unsigned i )

inline

Definition at line 92 of file cadical_walk.cpp.

                                       {
  const double res = (i < table.size () ? table[i] : epsilon);
  LOG ("break %u mapped to score %g", i, res);
  return res;
}

Member Data Documentation

broken

vector<Clause *> CaDiCaL::Walker::broken

Definition at line 20 of file cadical_walk.cpp.

epsilon

double CaDiCaL::Walker::epsilon

Definition at line 21 of file cadical_walk.cpp.

internal

Internal* CaDiCaL::Walker::internal

Definition at line 15 of file cadical_walk.cpp.

limit

int64_t CaDiCaL::Walker::limit

Definition at line 19 of file cadical_walk.cpp.

propagations

int64_t CaDiCaL::Walker::propagations

Definition at line 18 of file cadical_walk.cpp.

random

Random CaDiCaL::Walker::random

Definition at line 17 of file cadical_walk.cpp.

scores

vector<double> CaDiCaL::Walker::scores

Definition at line 23 of file cadical_walk.cpp.

table

vector<double> CaDiCaL::Walker::table

Definition at line 22 of file cadical_walk.cpp.

---

The documentation for this struct was generated from the following file:

• src/sat/cadical/cadical_walk.cpp