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

#include <constraint.h>

Inheritance diagram for Clasp::Constraint:

Classes
struct	PropResult
	Type used as return type for Constraint::propagate. More...
Public Member Functions
virtual ClauseHead *	clause ()
	Shall return this if constraint is a clause, otherwise 0.
virtual Constraint *	cloneAttach (Solver &other)=0
	Returns a clone of this and adds necessary watches to the given solver.
	Constraint ()
virtual void	destroy (Solver *s=0, bool detach=false)
	Default is to call delete this.
virtual uint32	estimateComplexity (const Solver &s) const
	Returns an estimate of the constraint's complexity relative to a clause (complexity = 1).
virtual bool	minimize (Solver &s, Literal p, CCMinRecursive *rec)
virtual PropResult	propagate (Solver &s, Literal p, uint32 &data)=0
virtual void	reason (Solver &s, Literal p, LitVec &lits)=0
virtual bool	simplify (Solver &s, bool reinit=false)
virtual ConstraintType	type () const
	Returns the type of this constraint.
virtual void	undoLevel (Solver &s)
	Called when the solver undid a decision level watched by this constraint.
virtual bool	valid (Solver &s)
	Shall return whether the constraint is valid (i.e. not conflicting) w.r.t the current assignment in s.
Protected Member Functions
virtual	~Constraint ()
Private Member Functions
	Constraint (const Constraint &)
Constraint &	operator= (const 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).

Definition at line 85 of file constraint.h.

Constructor & Destructor Documentation

Clasp::Constraint::Constraint ( )

Definition at line 27 of file constraint.cpp.

Clasp::Constraint::~Constraint ( ) [protected, virtual]

Definition at line 28 of file constraint.cpp.

Clasp::Constraint::Constraint ( const Constraint & ) [private]

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.

Definition at line 35 of file constraint.cpp.

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, Clasp::CBConsequences::CBFinder, and Clasp::Test::TestingConstraint.

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, Clasp::Test::TestingConstraint, and Clasp::ModelEnumerator::ModelFinder.

Definition at line 29 of file constraint.cpp.

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.

Definition at line 33 of file constraint.cpp.

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.

Definition at line 1318 of file solver.cpp.

Constraint& Clasp::Constraint::operator= ( const Constraint & ) [private]

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::DefaultUnfoundedCheck, Clasp::ModelEnumerator::BacktrackFinder, Clasp::WeightConstraint, and Clasp::Test::TestingConstraint.

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::DefaultUnfoundedCheck, Clasp::ModelEnumerator::BacktrackFinder, Clasp::WeightConstraint, and Clasp::Test::TestingConstraint.

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, Clasp::ModelEnumerator::ModelFinder, and Clasp::Test::TestingConstraint.

Definition at line 31 of file constraint.cpp.

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, Clasp::LearntConstraint, and Clasp::Test::TestingConstraint.

Definition at line 30 of file constraint.cpp.

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::Clause, Clasp::DomainHeuristic, Clasp::DefaultMinimize, Clasp::Lookahead, Clasp::WeightConstraint, and Clasp::Test::TestingConstraint.

Definition at line 32 of file constraint.cpp.

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.

Definition at line 34 of file constraint.cpp.

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

Classes

Public Member Functions

Protected Member Functions

Private Member Functions

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation