Fast SAT Solver: BlindSatSolver Class Reference

BlindSatSolver	(	SatProblem *	problem,
		int	stepWidth
	)

Parameters:

	problem	SatProblem instance containing SAT problem to solve.
	stepWidth	Number of bits explored in one step. This influences the granullarity of notifications and process control. Recomended value for ordinary machines is 16.

Definition at line 68 of file BlindSatSolver.cpp.

References BlindSatSolver::Private::end, SatProblem::getVarsCount(), BlindSatSolver::Private::init(), BlindSatSolver::Private::problem, and BlindSatSolver::Private::stepWidth.

~BlindSatSolver ( ) [virtual]

Definition at line 81 of file BlindSatSolver.cpp.

SatProblem * getProblem ( ) [virtual]

Returns pointer to instance of SatProblem used by solver.

Returns:: Returns pointer to instance of SatProblem used by solver.

Implements AbstractSatSolver.

Definition at line 84 of file BlindSatSolver.cpp.

References BlindSatSolver::Private::problem.

int getSolutionsCount ( ) [virtual]

Returns current count solutions founded by solver.

Returns:: Returns current count solutions founded by solver.

Implements AbstractSatSolver.

Definition at line 87 of file BlindSatSolver.cpp.

References SatItemVector::getLength(), and BlindSatSolver::Private::resultSet.

SatItemVector * getSolutionVector ( ) [virtual]

Returns a set of solutions founded by solver.

Returns:: Returns on heap allocated instance of SatItemVector containing solutions founded by solver.

Implements AbstractSatSolver.

Definition at line 90 of file BlindSatSolver.cpp.

References BlindSatSolver::Private::resultSet.

float minFitness ( ) [virtual]

Returns fitness of the Worst solution managed by solver.

Implements AbstractSatSolver.

Definition at line 93 of file BlindSatSolver.cpp.

References BlindSatSolver::Private::minFitness.

Referenced by BlindSatSolver::doStep().

float avgFitness ( ) [virtual]

Returns average fitness computed by solver.

Implements AbstractSatSolver.

Definition at line 96 of file BlindSatSolver.cpp.

References BlindSatSolver::Private::current, and BlindSatSolver::Private::sumFitness.

float maxFitness ( ) [virtual]

Returns the Best fitness founded by solver.

Note:: This should be always 1.0 if solution was found.

Implements AbstractSatSolver.

Definition at line 99 of file BlindSatSolver.cpp.

References BlindSatSolver::Private::maxFitness.

void initialize ( ) [protected, virtual]

Initialize process.

Note:: Design pattern template method

Implements AbstractProcess.

Definition at line 103 of file BlindSatSolver.cpp.

References SatItemVector::clear(), BlindSatSolver::Private::init(), and BlindSatSolver::Private::resultSet.

void doStep ( ) [protected, virtual]

Do one step of process.

Note:: Design pattern template method

Implements AbstractProcess.

Definition at line 108 of file BlindSatSolver.cpp.

void start ( ) [virtual, inherited]

Start process execution. This method returns control after process ends (or after it is stopped by stop() or reset() method).

Reimplemented from AbstractProcess.

Definition at line 111 of file SatSolver.cpp.

References AbstractProcessWatched::Private::running, AbstractProcess::start(), and AbstractProcessWatched::Private::start.

void stop ( ) [virtual, inherited]

Stop currently executed process as soon as possible.

Reimplemented from AbstractProcess.

Definition at line 117 of file SatSolver.cpp.

References AbstractProcessWatched::Private::currentElapsed(), AbstractProcessWatched::Private::running, AbstractProcess::stop(), and AbstractProcessWatched::Private::total.

Referenced by GaSatSolver::doStep(), BlindSatSolver::doStep(), TimedStop::notify(), and SolutionsCountStop::notify().

void reset ( ) [virtual, inherited]

Reset process to its initial state.

Note:: This implies stop() if process is running.

Reimplemented from AbstractProcess.

Definition at line 125 of file SatSolver.cpp.

References AbstractProcess::reset(), AbstractProcessWatched::Private::running, and AbstractProcessWatched::Private::total.

long getTimeElapsed ( ) [virtual, inherited]

Returns time elapsed by activity.

Returns:: Returns time elapsed by activity.

Implements IStopWatch.

Definition at line 131 of file SatSolver.cpp.

References AbstractProcessWatched::Private::currentElapsed(), AbstractProcessWatched::Private::running, and AbstractProcessWatched::Private::total.

Referenced by ResultsWatch::notify(), FitnessWatch::notify(), and TimedStop::notify().

int getStepsCount ( ) [virtual, inherited]

Returns current step number.

Returns:: Returns current step number.

Definition at line 86 of file SatSolver.cpp.

References AbstractProcess::Private::steps.

Referenced by ProgressWatch::notify().

void addObserver ( IObserver * observer ) [virtual, inherited]

Add observer to list of listeners.

Parameters:

observer

Observer object to add to list of listeners.

Note:: Observers are notified in the same order, as there are added to lsit of listeners.
Design pattern observer

Implements ISubject.

Definition at line 46 of file SatSolver.cpp.

References AbstractSubject::Private::container.

Referenced by main().

void notify ( ) [protected, inherited]

Send notification to all observers (listeners).

Note:: Observers are notified in the same order, as there are added to lsit of listeners.

Definition at line 49 of file SatSolver.cpp.

References AbstractSubject::Private::container, and IObserver::notify().

Referenced by BlindSatSolver::doStep(), GaSatSolver::Private::fitness(), and AbstractProcess::start().


Public Member Functions
	BlindSatSolver (SatProblem *problem, int stepWidth)
virtual	~BlindSatSolver ()
virtual SatProblem *	getProblem ()
	Returns pointer to instance of SatProblem used by solver.
virtual int	getSolutionsCount ()
	Returns current count solutions founded by solver.
virtual SatItemVector *	getSolutionVector ()
	Returns a set of solutions founded by solver.
virtual float	minFitness ()
	Returns fitness of the Worst solution managed by solver.
virtual float	avgFitness ()
	Returns average fitness computed by solver.
virtual float	maxFitness ()
	Returns the Best fitness founded by solver.
virtual void	start ()
	Start process execution. This method returns control after process ends (or after it is stopped by stop() or reset() method).
virtual void	stop ()
	Stop currently executed process as soon as possible.
virtual void	reset ()
	Reset process to its initial state.
virtual long	getTimeElapsed ()
	Returns time elapsed by activity.
virtual int	getStepsCount ()
	Returns current step number.
virtual void	addObserver (IObserver *)
	Add observer to list of listeners.
Protected Member Functions
virtual void	initialize ()
	Initialize process.
virtual void	doStep ()
	Do one step of process.
void	notify ()
	Send notification to all observers (listeners).
Classes
struct	Private

BlindSatSolver Class Reference
[SAT Solver]

Detailed Description

Public Member Functions

Protected Member Functions

Classes

Constructor & Destructor Documentation

Member Function Documentation

BlindSatSolver Class Reference [SAT Solver]

Detailed Description

Public Member Functions

Protected Member Functions

Classes

Constructor & Destructor Documentation

Member Function Documentation

BlindSatSolver Class Reference
[SAT Solver]