Class for model enumeration with minimization and projection. More...

#include <model_enumerators.h>

Inheritance diagram for Clasp::ModelEnumerator:

Classes
class	BacktrackFinder
class	ModelFinder
class	RecordFinder
class	SolutionQueue
Public Types
enum	ProjectOptions { project_enable_simple = 1, project_use_heuristic = 2, project_save_progress = 4, project_enable_full = 6 }
	Projective solution enumeration and options. More...
enum	Strategy { strategy_auto = 0, strategy_backtrack = 1, strategy_record = 2 }
	Enumeration algorithms. More...
Public Member Functions
	ModelEnumerator (Strategy st=strategy_auto)
bool	projectionEnabled () const
void	setStrategy (Strategy st=strategy_auto, uint32 projection=0)
	Configure strategy.
Strategy	strategy () const
	~ModelEnumerator ()
Protected Member Functions
ConPtr	doInit (SharedContext &ctx, MinimizeConstraint *m, int numModels)
	Shall prepare the enumerator and freeze any enumeration-related variable.
bool	supportsParallel () const
	Returns whether or not this enumerator supports parallel search.
bool	supportsRestarts () const
	Returns whether or not this enumerator supports full restarts once a model was found.
Private Types
enum	{ detect_strategy_flag = 4u, trivial_flag = 8u, strategy_opts_mask = 15u }
typedef SolutionQueue *	QPtr
Private Member Functions
void	addProjectVar (SharedContext &ctx, Var v, bool mark)
bool	detectStrategy () const
void	initProjection (SharedContext &ctx)
uint32	numProjectionVars () const
uint32	projectOpts () const
Var	projectVar (uint32 i) const
bool	trivial () const
Private Attributes
uint32	options_
VarVec *	project_
QPtr	queue_

Detailed Description

Class for model enumeration with minimization and projection.

This class implements algorithms for enumerating models with or without optimization and/or projection. It supports two different algorithms (strategies), first, enumeration via restricted backjumping, and second, enumeration via recording of solution nogoods.

The first strategy, strategy_backtrack, maintains a special backtracking level to suppress certain backjumps that could otherwise "re-open" search spaces already visited. If projection is not active, no extra nogoods are created. Otherwise, the number of additional solution nogoods is linear in the number of projection atoms.

The second strategy, strategy_record, enumerates models by recording nogoods for found solutions. In general, this strategy is exponential in space (bounded by the number of solutions). On the other hand, if optimization is active, additional nogoods are not needed because the optimization constraint already serves as solution nogood.

There is also a third strategy, strategy_auto, provided for convenience. This strategy automatically selects between strategy_backtrack and strategy_record based on the problem at hand. It uses strategy_record, if one of the following holds:

optimization is active, or
only one model is requested, or
both parallel search as well as projection are active

In all other cases, strategy_auto selects strategy_backtrack.

Definition at line 59 of file model_enumerators.h.

Member Typedef Documentation

typedef SolutionQueue* Clasp::ModelEnumerator::QPtr [private]

Definition at line 97 of file model_enumerators.h.

Member Enumeration Documentation

anonymous enum [private]

Enumerator:

detect_strategy_flag
trivial_flag
strategy_opts_mask

Definition at line 93 of file model_enumerators.h.

enum Clasp::ModelEnumerator::ProjectOptions

Projective solution enumeration and options.

Enumerator:

project_enable_simple	Enable projective solution enumeration.
project_use_heuristic	Use heuristic when selecting a literal from a projection nogood.
project_save_progress	Enable progress saving after the first solution was found.
project_enable_full	Enable projective solution enumeration with heuristic and progress saving.

Definition at line 68 of file model_enumerators.h.

enum Clasp::ModelEnumerator::Strategy

Enumeration algorithms.

Enumerator:

strategy_auto	Use strategy best suited to problem.
strategy_backtrack	Use backtrack-based enumeration.
strategy_record	Use nogood-based enumeration.

Definition at line 62 of file model_enumerators.h.

Constructor & Destructor Documentation

Clasp::ModelEnumerator::ModelEnumerator ( Strategy st = strategy_auto ) [explicit]

Parameters:

p	The printer to use for outputting results.

Definition at line 230 of file model_enumerators.cpp.

Clasp::ModelEnumerator::~ModelEnumerator ( )

Definition at line 247 of file model_enumerators.cpp.

Member Function Documentation

void Clasp::ModelEnumerator::addProjectVar	(	SharedContext &	ctx,
		Var	v,
		bool	mark
	)		`[private]`

Definition at line 324 of file model_enumerators.cpp.

bool Clasp::ModelEnumerator::detectStrategy ( ) const [inline, private]

Definition at line 104 of file model_enumerators.h.

EnumerationConstraint * Clasp::ModelEnumerator::doInit	(	SharedContext &	ctx,
		MinimizeConstraint *	m,
		int	numModels
	)		`[protected, virtual]`

Shall prepare the enumerator and freeze any enumeration-related variable.

Returns:: A prototypical enumeration constraint to be used in the master solver.

Implements Clasp::Enumerator.

Definition at line 265 of file model_enumerators.cpp.

void Clasp::ModelEnumerator::initProjection ( SharedContext & ctx ) [private]

Definition at line 298 of file model_enumerators.cpp.

uint32 Clasp::ModelEnumerator::numProjectionVars ( ) const [inline, private]

Definition at line 101 of file model_enumerators.h.

bool Clasp::ModelEnumerator::projectionEnabled ( ) const [inline]

Definition at line 86 of file model_enumerators.h.

uint32 Clasp::ModelEnumerator::projectOpts ( ) const [inline, private]

Definition at line 103 of file model_enumerators.h.

Var Clasp::ModelEnumerator::projectVar ( uint32 i ) const [inline, private]

Definition at line 102 of file model_enumerators.h.

void Clasp::ModelEnumerator::setStrategy	(	Strategy	st = `strategy_auto`,
		uint32	projection = `0`
	)

Configure strategy.

st Enumeration algorithm to use. projection The set of ProjectOptions to be applied or 0 to disable projective enumeration.

Definition at line 252 of file model_enumerators.cpp.

Strategy Clasp::ModelEnumerator::strategy ( ) const [inline]

Definition at line 87 of file model_enumerators.h.

bool Clasp::ModelEnumerator::supportsParallel ( ) const [inline, protected, virtual]

Returns whether or not this enumerator supports parallel search.

Reimplemented from Clasp::Enumerator.

Definition at line 90 of file model_enumerators.h.

bool Clasp::ModelEnumerator::supportsRestarts ( ) const [inline, protected, virtual]

Returns whether or not this enumerator supports full restarts once a model was found.

Reimplemented from Clasp::Enumerator.

Definition at line 89 of file model_enumerators.h.

bool Clasp::ModelEnumerator::trivial ( ) const [inline, private]

Definition at line 105 of file model_enumerators.h.

Member Data Documentation

uint32 Clasp::ModelEnumerator::options_ [private]

Definition at line 108 of file model_enumerators.h.

VarVec* Clasp::ModelEnumerator::project_ [private]

Definition at line 107 of file model_enumerators.h.

QPtr Clasp::ModelEnumerator::queue_ [private]

Definition at line 106 of file model_enumerators.h.

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

Classes

Public Types

Public Member Functions

Protected Member Functions

Private Types

Private Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

Member Enumeration Documentation

Constructor & Destructor Documentation

Member Function Documentation

Member Data Documentation