Base class for decision heuristics to be used in a Solver. More...

#include <solver.h>

Inheritance diagram for Clasp::DecisionHeuristic:

Public Member Functions
virtual bool	bump (const Solver &, const WeightLitVec &, double)
	Shall bump the activity of literals in lits by lits.second * adj.
	DecisionHeuristic ()
virtual Literal	doSelect (Solver &)=0
	Implements the actual selection process.
virtual void	endInit (Solver &)
virtual void	newConstraint (const Solver &, const Literal *, LitVec::size_type, ConstraintType)
bool	select (Solver &s)
virtual Literal	selectRange (Solver &, const Literal first, const Literal )
virtual void	simplify (const Solver &, LitVec::size_type)
virtual void	startInit (const Solver &)
virtual void	undoUntil (const Solver &, LitVec::size_type)
virtual void	updateReason (const Solver &, const LitVec &, Literal)
virtual void	updateVar (const Solver &, Var, uint32)=0
virtual	~DecisionHeuristic ()
Static Public Member Functions
static Literal	defaultLiteral (Solver &s, Var v)
static Literal	selectLiteral (Solver &s, Var v, int signScore)
Private Member Functions
	DecisionHeuristic (const DecisionHeuristic &)
DecisionHeuristic &	operator= (const DecisionHeuristic &)

Detailed Description

Base class for decision heuristics to be used in a Solver.

During search the decision heuristic is used whenever the DPLL-procedure must pick a new variable to branch on. Each concrete decision heuristic can implement a different algorithm for selecting the next decision variable.

Definition at line 915 of file solver.h.

Constructor & Destructor Documentation

Clasp::DecisionHeuristic::DecisionHeuristic ( ) [inline]

Definition at line 917 of file solver.h.

Clasp::DecisionHeuristic::~DecisionHeuristic ( ) [virtual]

Definition at line 28 of file solver.cpp.

Clasp::DecisionHeuristic::DecisionHeuristic ( const DecisionHeuristic & ) [private]

Member Function Documentation

virtual bool Clasp::DecisionHeuristic::bump	(	const Solver &	,
		const WeightLitVec &	,
		double
	)		`[inline, 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 in Clasp::Restricted, Clasp::ClaspVsids_t< ScoreType >, Clasp::ClaspVsids_t< DomScore >, Clasp::ClaspVmtf, and Clasp::ClaspBerkmin.

Definition at line 996 of file solver.h.

static Literal Clasp::DecisionHeuristic::defaultLiteral	(	Solver &	s,
		Var	v
	)		`[inline, static]`

Definition at line 1040 of file solver.h.

virtual Literal Clasp::DecisionHeuristic::doSelect ( Solver & ) [pure 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!

Implemented in Clasp::SelectFirst, Clasp::Restricted, Clasp::DomainHeuristic, Clasp::ClaspVsids_t< ScoreType >, Clasp::ClaspVsids_t< DomScore >, Clasp::UnitHeuristic, Clasp::ClaspVmtf, Clasp::ClaspBerkmin, and Clasp::Test::ClauseObserver.

virtual void Clasp::DecisionHeuristic::endInit ( Solver & ) [inline, 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 in Clasp::Restricted, Clasp::ClaspVsids_t< ScoreType >, Clasp::ClaspVsids_t< DomScore >, Clasp::UnitHeuristic, Clasp::ClaspVmtf, and Clasp::ClaspBerkmin.

Definition at line 932 of file solver.h.

virtual void Clasp::DecisionHeuristic::newConstraint	(	const Solver &	,
		const Literal *	,
		LitVec::size_type	,
		ConstraintType
	)		`[inline, 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 in Clasp::Restricted, Clasp::ClaspVsids_t< ScoreType >, Clasp::ClaspVsids_t< DomScore >, Clasp::ClaspVmtf, Clasp::ClaspBerkmin, and Clasp::Test::ClauseObserver.

Definition at line 977 of file solver.h.

DecisionHeuristic& Clasp::DecisionHeuristic::operator= ( const DecisionHeuristic & ) [private]

bool Clasp::DecisionHeuristic::select ( Solver & s ) [inline]

Called whenever the solver must pick a new variable to branch on.

Parameters:

s	The solver that needs a new decision variable.

Returns:

true : if the decision heuristic assumed a literal
false : if no decision could be made because assignment is total or there is a conflict

Postcondition:: If true is returned, the heuristic has asserted a literal.

Definition at line 1008 of file solver.h.

static Literal Clasp::DecisionHeuristic::selectLiteral	(	Solver &	s,
		Var	v,
		int	signScore
	)		`[inline, static]`

Definition at line 1030 of file solver.h.

virtual Literal Clasp::DecisionHeuristic::selectRange	(	Solver &	,
		const Literal *	first,
		const Literal *
	)		`[inline, 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 in Clasp::Restricted, Clasp::ClaspVsids_t< ScoreType >, Clasp::ClaspVsids_t< DomScore >, Clasp::ClaspVmtf, and Clasp::ClaspBerkmin.

Definition at line 1027 of file solver.h.

virtual void Clasp::DecisionHeuristic::simplify	(	const Solver &	,
		LitVec::size_type
	)		`[inline, 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 in Clasp::Restricted, Clasp::ClaspVsids_t< ScoreType >, Clasp::ClaspVsids_t< DomScore >, and Clasp::ClaspVmtf.

Definition at line 957 of file solver.h.

virtual void Clasp::DecisionHeuristic::startInit ( const Solver & ) [inline, 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 in Clasp::Restricted, Clasp::DomainHeuristic, Clasp::ClaspVsids_t< ScoreType >, Clasp::ClaspVsids_t< DomScore >, Clasp::ClaspVmtf, and Clasp::ClaspBerkmin.

Definition at line 924 of file solver.h.

virtual void Clasp::DecisionHeuristic::undoUntil	(	const Solver &	,
		LitVec::size_type
	)		`[inline, 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 in Clasp::Restricted, Clasp::ClaspVsids_t< ScoreType >, Clasp::ClaspVsids_t< DomScore >, Clasp::ClaspVmtf, and Clasp::ClaspBerkmin.

Definition at line 966 of file solver.h.

virtual void Clasp::DecisionHeuristic::updateReason	(	const Solver &	,
		const LitVec &	,
		Literal
	)		`[inline, 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 in Clasp::Restricted, Clasp::ClaspVsids_t< ScoreType >, Clasp::ClaspVsids_t< DomScore >, Clasp::ClaspVmtf, and Clasp::ClaspBerkmin.

Definition at line 989 of file solver.h.

virtual void Clasp::DecisionHeuristic::updateVar	(	const Solver &	,
		Var	,
		uint32
	)		`[pure 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.

Implemented in Clasp::SelectFirst, Clasp::Restricted, Clasp::ClaspVsids_t< ScoreType >, Clasp::ClaspVsids_t< DomScore >, Clasp::UnitHeuristic, Clasp::ClaspVmtf, Clasp::ClaspBerkmin, and Clasp::Test::ClauseObserver.

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

Public Member Functions

Static Public Member Functions

Private Member Functions

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation