Variable Move To Front decision strategies inspired by Siege. More...

#include <heuristics.h>

Inheritance diagram for Clasp::ClaspVmtf:

Classes
struct	LessLevel
struct	VarInfo
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.
	ClaspVmtf (LitVec::size_type mtf=8, 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 Member Functions
Literal	doSelect (Solver &s)
	Implements the actual selection process.
Private Types
typedef PodVector< VarInfo >::type	Score
typedef std::list< Var >	VarList
typedef VarList::iterator	VarPos
Private Member Functions
Literal	selectRange (Solver &s, const Literal first, const Literal last)
Private Attributes
uint32	decay_
VarPos	front_
const LitVec::size_type	MOVE_TO_FRONT
VarVec	mtf_
Score	score_
TypeSet	types_
VarList	vars_

Detailed Description

Variable Move To Front decision strategies inspired by Siege.

See also:: Lawrence Ryan: "Efficient Algorithms for Clause Learning SAT-Solvers"

Note:

This implementation of VMTF differs from the original implementation in three points:

it optionally moves to the front a selection of variables from learnt loop nogoods
it measures variable activity by using a BerkMin-like score scheme
the initial order of the var list is determined using a MOMs-like score scheme

Definition at line 174 of file heuristics.h.

Member Typedef Documentation

typedef PodVector<VarInfo>::type Clasp::ClaspVmtf::Score [private]

Definition at line 208 of file heuristics.h.

typedef std::list<Var> Clasp::ClaspVmtf::VarList [private]

Definition at line 192 of file heuristics.h.

typedef VarList::iterator Clasp::ClaspVmtf::VarPos [private]

Definition at line 193 of file heuristics.h.

Constructor & Destructor Documentation

Clasp::ClaspVmtf::ClaspVmtf	(	LitVec::size_type	mtf = `8`,
		const HeuParams &	params = `HeuParams()`
	)		`[explicit]`

Parameters:

mtf	The number of literals from constraints used during conflict resolution that are moved to the front.

Definition at line 331 of file heuristics.cpp.

Member Function Documentation

bool Clasp::ClaspVmtf::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 439 of file heuristics.cpp.

Literal Clasp::ClaspVmtf::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.

Definition at line 446 of file heuristics.cpp.

void Clasp::ClaspVmtf::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 345 of file heuristics.cpp.

void Clasp::ClaspVmtf::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 398 of file heuristics.cpp.

Literal Clasp::ClaspVmtf::selectRange	(	Solver &	,
		const Literal *	first,
		const Literal *
	)		`[private, 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 467 of file heuristics.cpp.

void Clasp::ClaspVmtf::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 388 of file heuristics.cpp.

void Clasp::ClaspVmtf::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.

Definition at line 340 of file heuristics.cpp.

void Clasp::ClaspVmtf::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 431 of file heuristics.cpp.

void Clasp::ClaspVmtf::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 435 of file heuristics.cpp.