A variable state independent decision heuristic favoring variables that were active in recent conflicts. More...

#include <heuristics.h>

Inheritance diagram for Clasp::ClaspVsids_t< ScoreType >:

Classes
struct	CmpScore
Public Member Functions
bool	bump (const Solver &s, const WeightLitVec &lits, double adj)
	Shall bump the activity of literals in lits by lits.second * adj.
	ClaspVsids_t (double d=0.95, const HeuParams &params=HeuParams())
void	endInit (Solver &)
void	newConstraint (const Solver &s, const Literal *first, LitVec::size_type size, ConstraintType t)
void	simplify (const Solver &, LitVec::size_type)
void	startInit (const Solver &s)
void	undoUntil (const Solver &, LitVec::size_type)
void	updateReason (const Solver &s, const LitVec &lits, Literal resolveLit)
void	updateVar (const Solver &s, Var v, uint32 n)
Protected Types
typedef PodVector< int32 >::type	OccVec
typedef PodVector< ScoreType > ::type	ScoreVec
typedef bk_lib::indexed_priority_queue < CmpScore >	VarOrder
Protected Member Functions
Literal	doSelect (Solver &s)
	Implements the actual selection process.
void	incOcc (Literal p)
virtual void	initScores (Solver &s, bool moms)
void	normalize ()
int	occ (Var v) const
Literal	selectRange (Solver &s, const Literal first, const Literal last)
void	updateVarActivity (Var v, double f=1.0)
Protected Attributes
const double	decay_
double	inc_
OccVec	occ_
ScoreVec	score_
TypeSet	types_
VarOrder	vars_

Detailed Description

template<class ScoreType>
class Clasp::ClaspVsids_t< ScoreType >

A variable state independent decision heuristic favoring variables that were active in recent conflicts.

This heuristic combines ideas from VSIDS and BerkMin. Literal Selection works as in VSIDS but var activities are increased as in BerkMin.

See also:: M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik: "Chaff: Engineering an Efficient SAT Solver"; E. Goldberg, Y. Navikov: "BerkMin: a Fast and Robust Sat-Solver"

Note:: The implementation uses the exponential VSIDS scheme from MiniSAT.

Definition at line 260 of file heuristics.h.

Member Typedef Documentation

template<class ScoreType>

typedef PodVector<int32>::type Clasp::ClaspVsids_t< ScoreType >::OccVec [protected]

Definition at line 278 of file heuristics.h.

template<class ScoreType>

typedef PodVector<ScoreType>::type Clasp::ClaspVsids_t< ScoreType >::ScoreVec [protected]

Definition at line 277 of file heuristics.h.

template<class ScoreType>

typedef bk_lib::indexed_priority_queue<CmpScore> Clasp::ClaspVsids_t< ScoreType >::VarOrder [protected]

Definition at line 298 of file heuristics.h.

Constructor & Destructor Documentation

template<class ScoreType >

Clasp::ClaspVsids_t< ScoreType >::ClaspVsids_t	(	double	d = `0.95`,
		const HeuParams &	params = `HeuParams()`
	)		`[explicit]`

Parameters:

d	Set initial inc-factor to 1.0/d.

Definition at line 481 of file heuristics.cpp.

Member Function Documentation

template<class ScoreType >

bool Clasp::ClaspVsids_t< ScoreType >::bump	(	const Solver &	,
		const WeightLitVec &	,
		double
	)		`[virtual]`

Shall bump the activity of literals in lits by lits.second * adj.

The default-implementation is a noop and always returns false.

Returns:: true if heuristic supports activities, false otherwise.

Reimplemented from Clasp::DecisionHeuristic.

Definition at line 583 of file heuristics.cpp.

template<class ScoreType >

Literal Clasp::ClaspVsids_t< ScoreType >::doSelect ( Solver & ) [protected, virtual]

Implements the actual selection process.

Precondition:: s.numFreeVars() > 0, i.e. there is at least one variable to branch on.

Returns:

a literal that is currently free or
a sentinel literal. In that case, the heuristic shall have asserted a literal!

Implements Clasp::DecisionHeuristic.

Reimplemented in Clasp::DomainHeuristic.

Definition at line 599 of file heuristics.cpp.

template<class ScoreType >

void Clasp::ClaspVsids_t< ScoreType >::endInit ( Solver & ) [virtual]

Called once after all problem constraints are known to the solver and the problem was simplified. The default-implementation is a noop.

Parameters:

s	The solver in which this heuristic is used.

Reimplemented from Clasp::DecisionHeuristic.

Definition at line 501 of file heuristics.cpp.

template<class ScoreType>

void Clasp::ClaspVsids_t< ScoreType >::incOcc ( Literal p ) [inline, protected]

Definition at line 288 of file heuristics.h.

template<class ScoreType >

void Clasp::ClaspVsids_t< ScoreType >::initScores	(	Solver &	s,
		bool	moms
	)		`[protected, virtual]`

Reimplemented in Clasp::DomainHeuristic.

Definition at line 522 of file heuristics.cpp.

template<class ScoreType >

void Clasp::ClaspVsids_t< ScoreType >::newConstraint	(	const Solver &	,
		const Literal *	,
		LitVec::size_type	,
		ConstraintType
	)		`[virtual]`

Called whenever a new constraint is added to the solver s. The default-implementation is a noop.

Parameters:

s	The solver to which the constraint is added.
first	First literal of the new constraint.
size	Size of the new constraint.
t	Type of the new constraint.

Note:: first points to an array of size size.

Reimplemented from Clasp::DecisionHeuristic.

Definition at line 564 of file heuristics.cpp.

template<class ScoreType >

void Clasp::ClaspVsids_t< ScoreType >::normalize ( ) [protected]

Definition at line 548 of file heuristics.cpp.

template<class ScoreType>

int Clasp::ClaspVsids_t< ScoreType >::occ ( Var v ) const [inline, protected]

Definition at line 289 of file heuristics.h.

template<class ScoreType >

Literal Clasp::ClaspVsids_t< ScoreType >::selectRange	(	Solver &	,
		const Literal *	first,
		const Literal *
	)		`[protected, virtual]`

Shall select one of the literals in the range [first, last).

Parameters:

s	The solver that needs a new decision variable.
first	Pointer to first literal in range.
last	Pointer to the end of the range.

Precondition:: [first, last) is not empty and all literals in the range are currently unassigned.

Note:: The default implementation returns *first.

Reimplemented from Clasp::DecisionHeuristic.

Definition at line 606 of file heuristics.cpp.

template<class ScoreType >

void Clasp::ClaspVsids_t< ScoreType >::simplify	(	const Solver &	,
		LitVec::size_type
	)		`[virtual]`

Called on decision level 0. Variables that are assigned on this level may be removed from any decision heuristic.

Note:: Whenever the solver returns to dl 0, simplify is only called again if the solver learnt new facts since the last call to simplify.

Parameters:

s	The solver that reached decision level 0.
st	The position in the trail of the first new learnt fact.

Reimplemented from Clasp::DecisionHeuristic.

Definition at line 541 of file heuristics.cpp.

template<class ScoreType >

void Clasp::ClaspVsids_t< ScoreType >::startInit ( const Solver & ) [virtual]

Called once after all problem variables are known to the solver. The default-implementation is a noop.

Parameters:

s	The solver in which this heuristic is used.

Reimplemented from Clasp::DecisionHeuristic.

Reimplemented in Clasp::DomainHeuristic.

Definition at line 493 of file heuristics.cpp.

template<class ScoreType >

void Clasp::ClaspVsids_t< ScoreType >::undoUntil	(	const Solver &	,
		LitVec::size_type
	)		`[virtual]`

Called whenever the solver backracks. Literals in the range [s.trail()[st], s.trail().size()) are subject to backtracking. The default-implementation is a noop.

Parameters:

s	The solver that is about to backtrack.
st	Position in the trail of the first literal that will be backtracked.

Reimplemented from Clasp::DecisionHeuristic.

Definition at line 590 of file heuristics.cpp.

template<class ScoreType >

void Clasp::ClaspVsids_t< ScoreType >::updateReason	(	const Solver &	,
		const LitVec &	,
		Literal
	)		`[virtual]`

Called for each new reason-set that is traversed during conflict analysis. The default-implementation is a noop.

Parameters:

s	The solver in which the conflict is analyzed.
lits	The current reason-set under inspection.
resolveLit	The literal that is currently resolved.

Note:: When a conflict is detected, the solver passes the conflicting literals in lits during the first call to updateReason. On that first call resolveLit is the sentinel-literal.

Reimplemented from Clasp::DecisionHeuristic.

Definition at line 579 of file heuristics.cpp.

template<class ScoreType >

void Clasp::ClaspVsids_t< ScoreType >::updateVar	(	const Solver &	,
		Var	,
		uint32
	)		`[virtual]`

Called if the state of one or more variables changed. A state change is one of:

A previously eliminated variable is resurrected.
A new aux variable was added.
An aux variable was removed.

Parameters:

s	Solver in which the state change occurred.
v	The first variable affected by the change.
n	The range of variables affected, i.e. [v, v+n).

Note:: Use s.validVar(v) and s.auxVar(v) to determine the reason for the update.

Implements Clasp::DecisionHeuristic.

Definition at line 511 of file heuristics.cpp.

template<class ScoreType>

void Clasp::ClaspVsids_t< ScoreType >::updateVarActivity	(	Var	v,
		double	f = `1.0`
	)		`[inline, protected]`

Definition at line 280 of file heuristics.h.

Member Data Documentation

template<class ScoreType>

const double Clasp::ClaspVsids_t< ScoreType >::decay_ [protected]

Definition at line 302 of file heuristics.h.

template<class ScoreType>

double Clasp::ClaspVsids_t< ScoreType >::inc_ [protected]

Definition at line 303 of file heuristics.h.

template<class ScoreType>

OccVec Clasp::ClaspVsids_t< ScoreType >::occ_ [protected]

Definition at line 300 of file heuristics.h.

template<class ScoreType>

ScoreVec Clasp::ClaspVsids_t< ScoreType >::score_ [protected]

Definition at line 299 of file heuristics.h.

template<class ScoreType>

TypeSet Clasp::ClaspVsids_t< ScoreType >::types_ [protected]

Definition at line 304 of file heuristics.h.

template<class ScoreType>

VarOrder Clasp::ClaspVsids_t< ScoreType >::vars_ [protected]

Definition at line 301 of file heuristics.h.

The documentation for this class was generated from the following files:

Classes

Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Detailed Description

template<class ScoreType> class Clasp::ClaspVsids_t< ScoreType >

Member Typedef Documentation

Constructor & Destructor Documentation

Member Function Documentation

Member Data Documentation

template<class ScoreType>
class Clasp::ClaspVsids_t< ScoreType >