Base class for (boolean) constraints to be used in a Solver. More...

#include <constraint.h>

Inheritance diagram for Clasp::Constraint:

Collaboration diagram for Clasp::Constraint:

Classes
struct	PropResult
	Type used as return type for Constraint::propagate. More...

Public Member Functions
	Constraint ()

virtual Constraint *	cloneAttach (Solver &other)=0
	Returns a clone of this and adds necessary watches to the given solver. More...

virtual void	destroy (Solver *s=0, bool detach=false)
	Default is to call delete this. More...

virtual ConstraintType	type () const
	Returns the type of this constraint. More...

virtual PropResult	propagate (Solver &s, Literal p, uint32 &data)=0

virtual void	reason (Solver &s, Literal p, LitVec &lits)=0

virtual bool	minimize (Solver &s, Literal p, CCMinRecursive *rec)

virtual void	undoLevel (Solver &s)
	Called when the solver undid a decision level watched by this constraint. More...

virtual bool	simplify (Solver &s, bool reinit=false)

virtual uint32	estimateComplexity (const Solver &s) const
	Returns an estimate of the constraint's complexity relative to a clause (complexity = 1). More...

virtual ClauseHead *	clause ()
	Shall return this if constraint is a clause, otherwise 0. More...

virtual bool	valid (Solver &s)
	Shall return whether the constraint is valid (i.e. not conflicting) w.r.t the current assignment in s. More...

Protected Member Functions
virtual	~Constraint ()

Detailed Description

Base class for (boolean) constraints to be used in a Solver.

Base class for (boolean) constraints like e.g. clauses. Concrete constraint classes define representations for constraints over boolean variables. Each constraint class must define a method for inference (derive information from an assignment), it must be able to detect conflicts (i.e. detect when the current assignment makes the constraint unsatisfiable) and to return a reason for inferred literals as well as conflicts (as a set of literals).

Constructor & Destructor Documentation

Clasp::Constraint::Constraint ( )

Clasp::Constraint::~Constraint ( )

protectedvirtual

Member Function Documentation

ClauseHead * Clasp::Constraint::clause ( )

virtual

Shall return this if constraint is a clause, otherwise 0.

The default implementation returns 0.

Reimplemented in Clasp::ClauseHead.

virtual Constraint* Clasp::Constraint::cloneAttach ( Solver & other )

pure virtual

Returns a clone of this and adds necessary watches to the given solver.

The function shall create and return a copy of this constraint to be used in the given solver. Furthermore, it shall add necessary watches to the given solver.

Note: Return 0 to indicate that cloning is not supported.

Implemented in Clasp::DomainHeuristic::DomMinimize, Clasp::mt::SharedLitsClause, Clasp::LoopFormula, Clasp::PostPropagator, Clasp::DomainHeuristic, Clasp::Clause, Clasp::MinimizeConstraint, Clasp::ModelEnumerator::BacktrackFinder, Clasp::WeightConstraint, Clasp::ModelEnumerator::RecordFinder, and Clasp::CBConsequences::CBFinder.

void Clasp::Constraint::destroy	(	Solver *	s = `0`,
		bool	detach = `false`
	)

virtual

Default is to call delete this.

Reimplemented in Clasp::DomainHeuristic::DomMinimize, Clasp::mt::SharedLitsClause, Clasp::LoopFormula, Clasp::UncoreMinimize, Clasp::Clause, Clasp::DefaultMinimize, Clasp::MinimizeConstraint, Clasp::EnumerationConstraint, Clasp::Lookahead, Clasp::WeightConstraint, Clasp::CBConsequences::CBFinder, and Clasp::ModelEnumerator::ModelFinder.

uint32 Clasp::Constraint::estimateComplexity ( const Solver & s ) const

virtual

Returns an estimate of the constraint's complexity relative to a clause (complexity = 1).

Reimplemented in Clasp::WeightConstraint.

bool Clasp::Constraint::minimize	(	Solver &	s,
		Literal	p,
		CCMinRecursive *	rec
	)

virtual

Called during minimization of learnt clauses.

Precondition: This constraint is the reason for p being true in s.

Returns: true if p can be removed from the current learnt clause, false otherwise.

Note: The default implementation uses the following inefficient algorithm
LitVec temp;

reason(s, p, temp);

for each x in temp

if (!s.ccMinimize(p, rec)) return false;

return true;

Reimplemented in Clasp::mt::SharedLitsClause, Clasp::LoopFormula, Clasp::Clause, Clasp::DefaultMinimize, and Clasp::WeightConstraint.

Here is the call graph for this function:

virtual PropResult Clasp::Constraint::propagate	(	Solver &	s,
		Literal	p,
		uint32 &	data
	)

pure virtual

Propagate is called for each constraint that watches p. It shall enqueue all consequences of p becoming true.

Precondition: p is true in s

Parameters

s	The solver in which p became true.
p	A literal watched by this constraint that recently became true.
data	The data-blob that this constraint passed when the watch for p was registered.

Implemented in Clasp::DomainHeuristic::DomMinimize, Clasp::LoopFormula, Clasp::UncoreMinimize, Clasp::ClauseHead, Clasp::PostPropagator, Clasp::DomainHeuristic, Clasp::DefaultMinimize, Clasp::EnumerationConstraint, Clasp::ModelEnumerator::BacktrackFinder, and Clasp::WeightConstraint.

virtual void Clasp::Constraint::reason	(	Solver &	s,
		Literal	p,
		LitVec &	lits
	)

pure virtual

Precondition: This constraint is the reason for p being true in s.

Postcondition: The literals implying p were added to lits.

Implemented in Clasp::DomainHeuristic::DomMinimize, Clasp::mt::SharedLitsClause, Clasp::LoopFormula, Clasp::UncoreMinimize, Clasp::PostPropagator, Clasp::DomainHeuristic, Clasp::Clause, Clasp::DefaultMinimize, Clasp::EnumerationConstraint, Clasp::ModelEnumerator::BacktrackFinder, and Clasp::WeightConstraint.

bool Clasp::Constraint::simplify	(	Solver &	s,
		bool	reinit = `false`
	)

virtual

Simplify this constraint.

Precondition: s.decisionLevel() == 0 and the current assignment is fully propagated.

Returns: true if this constraint can be ignored (e.g. is satisfied), false otherwise.

Postcondition: If simplify returned true, this constraint has previously removed all its watches from the solver.

Note: The default implementation is a noop and returns false.

Reimplemented in Clasp::DomainHeuristic::DomMinimize, Clasp::mt::SharedLitsClause, Clasp::LoopFormula, Clasp::UncoreMinimize, Clasp::Clause, Clasp::EnumerationConstraint, Clasp::WeightConstraint, and Clasp::ModelEnumerator::ModelFinder.

ConstraintType Clasp::Constraint::type ( ) const

virtual

Returns the type of this constraint.

Note: The default implementation returns Constraint_t::static_constraint.

Reimplemented in Clasp::LoopFormula, Clasp::ClauseHead, and Clasp::LearntConstraint.

void Clasp::Constraint::undoLevel ( Solver & s )

virtual

Called when the solver undid a decision level watched by this constraint.

Parameters

s	the solver in which the decision level is undone.

Reimplemented in Clasp::DomainHeuristic, Clasp::DefaultMinimize, Clasp::Lookahead, and Clasp::WeightConstraint.

bool Clasp::Constraint::valid ( Solver & s )

virtual

Shall return whether the constraint is valid (i.e. not conflicting) w.r.t the current assignment in s.

Precondition: The assignment in s is not conflicting and fully propagated.

Postcondition: A changed assignment if the assignment was not valid.

Note: The default implementation always returns true and assumes that conflicts are detected by Constraint::propagate().

Reimplemented in Clasp::UncoreMinimize, Clasp::EnumerationConstraint, and Clasp::DefaultUnfoundedCheck.

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

/Users/danielbaeck/Dropbox/Uni Klagenfurt/Diplomarbeit/gringo44/libclasp/clasp/constraint.h
/Users/danielbaeck/Dropbox/Uni Klagenfurt/Diplomarbeit/gringo44/libclasp/src/constraint.cpp
/Users/danielbaeck/Dropbox/Uni Klagenfurt/Diplomarbeit/gringo44/libclasp/src/solver.cpp

Classes

Public Member Functions

Protected Member Functions

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation