Reduce strategy used during solving. More...

Public Types
enum	Algorithm { reduce_linear = 0, reduce_stable = 1, reduce_sort = 2, reduce_heap = 3 }
	Reduction algorithm to use during solving. More...
enum	EstimateSize { est_dynamic = 0, est_con_complexity = 1, est_num_constraints = 2, est_num_vars = 3 }
enum	Score { score_act = 0, score_lbd = 1, score_both = 2 }
	Score to measure "activity" of learnt constraints. More...
Public Member Functions
	ReduceStrategy ()
Static Public Member Functions
static uint32	asScore (Score sc, const Clasp::Activity &act)
static int	compare (Score sc, const Clasp::Activity &lhs, const Clasp::Activity &rhs)
static uint32	scoreAct (const Activity &act)
static uint32	scoreBoth (const Activity &act)
static uint32	scoreLbd (const Activity &act)
Public Attributes
uint32	algo: 2
uint32	estimate: 2
uint32	fReduce: 7
uint32	fRestart: 7
uint32	glue: 8
uint32	noGlue: 1
uint32	score: 2

Detailed Description

Reduce strategy used during solving.

A reduce strategy mainly consists of an algorithm and a scoring scheme for measuring "activity" of learnt constraints.

Definition at line 220 of file solver_strategies.h.

Member Enumeration Documentation

Reduction algorithm to use during solving.

Enumerator:

reduce_linear	Linear algorithm from clasp-1.3.x.
reduce_stable	Sort constraints by score but keep order in learnt db.
reduce_sort	Sort learnt db by score and remove fraction with lowest score.
reduce_heap	Similar to reduce_sort but only partially sorts learnt db.

Definition at line 222 of file solver_strategies.h.

Enumerator:

Definition at line 234 of file solver_strategies.h.

Score to measure "activity" of learnt constraints.

Enumerator:

score_act	Activity only: how often constraint is used during conflict analysis.
score_lbd	Use literal block distance as activity.
score_both	Use activity and lbd together.