A variant of the BerkMin decision heuristic from the BerkMin Sat-Solver. More...

#include <heuristics.h>

Inheritance diagram for Clasp::ClaspBerkmin:

Classes
struct	HScore
struct	Order
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.
	ClaspBerkmin (uint32 maxBerk=0, const HeuParams &params=HeuParams(), bool berkHuang=false)
void	endInit (Solver &s)
void	newConstraint (const Solver &s, const Literal *first, LitVec::size_type size, ConstraintType t)
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 VarVec::iterator	Pos
typedef PodVector< HScore >::type	Scores
Private Member Functions
Var	getMostActiveFreeVar (const Solver &s)
Var	getTopMoms (const Solver &s)
bool	hasActivities () const
void	hasActivities (bool b)
bool	hasTopUnsat (Solver &s)
bool	initHuang () const
void	initHuang (bool b)
Literal	selectLiteral (Solver &s, Var v, bool vsids) const
Literal	selectRange (Solver &s, const Literal first, const Literal last)
Private Attributes
VarVec	cache_
Pos	cacheFront_
uint32	cacheSize_
LitVec	freeLits_
LitVec	freeOtherLits_
Var	front_
uint32	maxBerkmin_
uint32	numVsids_
struct Clasp::ClaspBerkmin::Order	order_
RNG	rng_
uint32	topConflict_
uint32	topOther_
TypeSet	types_

Detailed Description

A variant of the BerkMin decision heuristic from the BerkMin Sat-Solver.

See also:: E. Goldberg, Y. Navikov: "BerkMin: a Fast and Robust Sat-Solver"

Note:

This version of the BerkMin heuristic varies mostly in the following points from the original BerkMin:

it considers loop-nogoods if requested (this is the default)
it uses a MOMS-like heuristic as long as there are no conflicts (and therefore no activities)
it uses a MOMS-like score to break ties whenever multiple variables from an unsatisfied learnt constraint have equal activities
it uses a lazy decaying scheme that only touches active variables

Definition at line 66 of file heuristics.h.

Member Typedef Documentation

typedef VarVec::iterator Clasp::ClaspBerkmin::Pos [private]

Definition at line 118 of file heuristics.h.

typedef PodVector<HScore>::type Clasp::ClaspBerkmin::Scores [private]

Definition at line 117 of file heuristics.h.

Constructor & Destructor Documentation

Clasp::ClaspBerkmin::ClaspBerkmin	(	uint32	maxBerk = `0`,
		const HeuParams &	params = `HeuParams()`,
		bool	berkHuang = `false`
	)		`[explicit]`

Parameters:

maxBerk Check at most maxBerk candidates when searching for not yet satisfied learnt constraints.

Note:: maxBerk = 0 means check *all* candidates.

Definition at line 58 of file heuristics.cpp.

Member Function Documentation

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

Literal Clasp::ClaspBerkmin::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 256 of file heuristics.cpp.

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

Var Clasp::ClaspBerkmin::getMostActiveFreeVar ( const Solver & s ) [private]

Definition at line 71 of file heuristics.cpp.

Var Clasp::ClaspBerkmin::getTopMoms ( const Solver & s ) [private]

Definition at line 107 of file heuristics.cpp.

bool Clasp::ClaspBerkmin::hasActivities ( ) const [inline, private]

Definition at line 87 of file heuristics.h.

void Clasp::ClaspBerkmin::hasActivities ( bool b ) [inline, private]

Definition at line 88 of file heuristics.h.

bool Clasp::ClaspBerkmin::hasTopUnsat ( Solver & s ) [private]

Definition at line 219 of file heuristics.cpp.

bool Clasp::ClaspBerkmin::initHuang ( ) const [inline, private]

Definition at line 85 of file heuristics.h.

void Clasp::ClaspBerkmin::initHuang ( bool b ) [inline, private]

Definition at line 86 of file heuristics.h.

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

Literal Clasp::ClaspBerkmin::selectLiteral	(	Solver &	s,
		Var	v,
		bool	vsids
	)		const `[private]`

Definition at line 306 of file heuristics.cpp.

Literal Clasp::ClaspBerkmin::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 276 of file heuristics.cpp.

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

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

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