Base class for satisfiability solvers. More...

#include <include/dlvhex2/SATSolver.h>

Inheritance diagram for SATSolver:

Collaboration diagram for SATSolver:

Public Types
typedef boost::shared_ptr < SATSolver >	Ptr
typedef boost::shared_ptr < const SATSolver >	ConstPtr
Public Member Functions
virtual void	restartWithAssumptions (const std::vector< ID > &assumptions)=0
	Resets the search and assumes truth values for selected atoms.
virtual void	addPropagator (PropagatorCallback *pb)=0
	Adds a propagator callback which is to be called by the SAT solver whenever it cannot propagate by other means or when a model is complete but before getNextModel returns it.
virtual void	removePropagator (PropagatorCallback *pb)=0
	Removes a propagator callback.
virtual InterpretationPtr	getNextModel ()=0
	Returns the next model.
virtual Nogood	getInconsistencyCause (InterpretationConstPtr explanationAtoms)=0
	Returns an explanation for an inconsistency in terms of litervals over the atoms given in `explanationAtoms`.
virtual void	addNogoodSet (const NogoodSet &ns, InterpretationConstPtr frozen=InterpretationConstPtr())=0
	Adds a set of additional nogoods to the solver instance.
Static Public Member Functions
static Ptr	getInstance (ProgramCtx &ctx, NogoodSet &ns, InterpretationConstPtr frozen=InterpretationConstPtr())
	Interprets the settings in `ctx` and creates an instance of a concrete subclass of this class, which implements a specific reasoner.

Detailed Description

Base class for satisfiability solvers.

Definition at line 50 of file SATSolver.h.

Member Typedef Documentation

typedef boost::shared_ptr<const SATSolver> SATSolver::ConstPtr

Reimplemented from NogoodContainer.

Reimplemented in CDNLSolver, InternalGroundASPSolver, and InternalGroundDASPSolver.

Definition at line 54 of file SATSolver.h.

typedef boost::shared_ptr<SATSolver> SATSolver::Ptr

Reimplemented from NogoodContainer.

Reimplemented in CDNLSolver, InternalGroundASPSolver, and InternalGroundDASPSolver.

Definition at line 53 of file SATSolver.h.

Member Function Documentation

virtual void SATSolver::addNogoodSet	(	const NogoodSet &	ns,
		InterpretationConstPtr	frozen = `InterpretationConstPtr()`
	)		`[pure virtual]`

Adds a set of additional nogoods to the solver instance.

Parameters:

ns	The set of nogoods to add.
frozen	A set of atoms which occur in `ns` and are saved from being optimized away (e.g. because their truth values are relevant).

Implemented in CDNLSolver, and InternalGroundASPSolver.

virtual void SATSolver::addPropagator ( PropagatorCallback * pb ) [pure virtual]

Adds a propagator callback which is to be called by the SAT solver whenever it cannot propagate by other means or when a model is complete but before getNextModel returns it.

The propagator can add additional nogoods by calling NogoodContainer::addNogood inherited from the base class.

Parameters:

pb	The callback to be added.

Implemented in CDNLSolver, and InternalGroundASPSolver.

virtual Nogood SATSolver::getInconsistencyCause ( InterpretationConstPtr explanationAtoms ) [pure virtual]

Returns an explanation for an inconsistency in terms of litervals over the atoms given in explanationAtoms.

Details (definition of explanations) are specified in subclasses.

The method may only be called after getNextModel() has returned a NULL-pointer after first call.

Parameters:

explanationAtoms The atoms which serve as explanation.

Returns:: An explanation for the inconsistency depending on the atoms in explanationAtoms.

Implemented in CDNLSolver, and InternalGroundASPSolver.

DLVHEX_NAMESPACE_BEGIN SATSolverPtr SATSolver::getInstance	(	ProgramCtx &	ctx,
		NogoodSet &	ns,
		InterpretationConstPtr	frozen = `InterpretationConstPtr()`
	)		`[static]`

Interprets the settings in ctx and creates an instance of a concrete subclass of this class, which implements a specific reasoner.

Parameters:

ctx	ProgramCtx.
ns	Encoding of the SAT instance as a set of nogoods.
frozen	A set of atoms which occur in `ns` and are saved from being optimized away (e.g. because their truth values are relevant). if NULL, then all variables are frozen.

Returns:: Pointer to the new solver instance.

Definition at line 45 of file SATSolver.cpp.

References ProgramCtx::config, DBGLOG, and Configuration::getOption().

Referenced by AssumptionBasedUnfoundedSetChecker::constructUFSDetectionProblemAndInstantiateSolver(), and EncodingBasedUnfoundedSetChecker::getUnfoundedSet().

virtual InterpretationPtr SATSolver::getNextModel ( ) [pure virtual]

Returns the next model.

This will also trigger callbacks to the propagators, see addPropagator.

Returns:: The next model or a NULL-pointer of no more models exist.

Implemented in CDNLSolver, InternalGroundASPSolver, and InternalGroundDASPSolver.

virtual void SATSolver::removePropagator ( PropagatorCallback * pb ) [pure virtual]

Removes a propagator callback.

Parameters:

pb	The callback to be removed.

Implemented in CDNLSolver, and InternalGroundASPSolver.

virtual void SATSolver::restartWithAssumptions ( const std::vector< ID > & assumptions ) [pure virtual]

Resets the search and assumes truth values for selected atoms.

Parameters:

assumptions Vector of positive or negated (using ID::NAF_MASK) atoms which are temporarily assumed to hold (until the next reset); ID::NAF_MASK is used to represent that the according atom is assumed to be false.

Implemented in CDNLSolver, and InternalGroundASPSolver.

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

include/dlvhex2/SATSolver.h
src/SATSolver.cpp

Public Types

Public Member Functions

Static Public Member Functions

Detailed Description

Member Typedef Documentation

Member Function Documentation