Minimization via branch and bound. More...

#include <minimize_constraint.h>

Inheritance diagram for Clasp::DefaultMinimize:

Classes
struct	Step
union	UndoInfo
Public Member Functions
bool	active () const
bool	attach (Solver &s)
	Attaches the constraint to the given solver.
bool	commitLowerBound (const Solver &s, bool upShared)
	Sets the current local upper bound as the lower bound of this constraint.
void	commitUpperBound (const Solver &s)
	Sets the current local sum as the global optimum (upper bound).
	DefaultMinimize (SharedData *d, uint32 strat)
void	destroy (Solver *, bool)
	Default is to call delete this.
bool	handleModel (Solver &s)
	Shall commit the model in s to the shared data object.
bool	handleUnsat (Solver &s, bool up, LitVec &out)
	Shall handle the unsatisfiable path in s.
bool	integrate (Solver &s)
	Shall activate the minimize constraint by integrating bounds stored in the shared data object.
bool	integrateBound (Solver &s)
	Tries to integrate the next tentative bound into this constraint.
bool	minimize (Solver &s, Literal p, CCMinRecursive *r)
bool	more () const
uint32	numRules () const
	Number of minimize statements contained in this constraint.
PropResult	propagate (Solver &s, Literal p, uint32 &data)
void	reason (Solver &s, Literal p, LitVec &lits)
bool	relax (Solver &, bool reset)
	Shall relax this constraint (i.e. remove any bounds).
bool	relaxBound (bool full=false)
	Removes the local upper bound of this constraint and therefore disables it.
wsum_t	sum (uint32 i, bool adjust) const
void	undoLevel (Solver &s)
	Called when the solver undid a decision level watched by this constraint.
Private Types
typedef const WeightLiteral *	Iter
enum	PropMode { propagate_new_sum, propagate_new_opt }
Private Member Functions
void	assign (wsum_t lhs, wsum_t rhs) const
uint32	computeImplicationSet (const Solver &s, const WeightLiteral &it, uint32 &undoPos)
wsum_t *	end () const
bool	greater (wsum_t lhs, wsum_t rhs, uint32 len, uint32 &aLev) const
uint32	lastUndoLevel (const Solver &s) const
bool	litSeen (uint32 i) const
wsum_t *	opt () const
bool	propagateImpl (Solver &s, PropMode m)
void	pushUndo (Solver &s, uint32 litIdx)
void	stepInit (uint32 n)
wsum_t &	stepLow () const
wsum_t *	sum () const
wsum_t *	temp () const
bool	updateBounds (bool applyStep)
	~DefaultMinimize ()
Private Attributes
uint32	actLev_
wsum_t *	bounds_
Iter	pos_
uint32	posTop_
const uint32	size_
struct Clasp::DefaultMinimize::Step	step_
UndoInfo *	undo_
uint32	undoTop_

Detailed Description

Minimization via branch and bound.

The class supports both basic branch and bound as well as hierarchical branch and bound (with or without varying step sizes).

Definition at line 311 of file minimize_constraint.h.

Member Typedef Documentation

typedef const WeightLiteral* Clasp::DefaultMinimize::Iter [private]

Definition at line 388 of file minimize_constraint.h.

Member Enumeration Documentation

enum Clasp::DefaultMinimize::PropMode [private]

Enumerator:

propagate_new_sum
propagate_new_opt

Definition at line 387 of file minimize_constraint.h.

Constructor & Destructor Documentation

Clasp::DefaultMinimize::DefaultMinimize	(	SharedData *	d,
		uint32	strat
	)		`[explicit]`

Definition at line 183 of file minimize_constraint.cpp.

Clasp::DefaultMinimize::~DefaultMinimize ( ) [private]

Definition at line 196 of file minimize_constraint.cpp.

Member Function Documentation

bool Clasp::DefaultMinimize::active ( ) const [inline]

Definition at line 333 of file minimize_constraint.h.

void Clasp::DefaultMinimize::assign	(	wsum_t *	lhs,
		wsum_t *	rhs
	)		const `[private]`

Definition at line 275 of file minimize_constraint.cpp.

bool Clasp::DefaultMinimize::attach ( Solver & s ) [virtual]

Attaches the constraint to the given solver.

Precondition:: s.decisionLevel() == 0

Note:: If either MinimizeMode_t::enumOpt or hierarchical optimization is active, s.sharedContext()->tagLiteral() shall be an unassigned literal.

Implements Clasp::MinimizeConstraint.

Definition at line 214 of file minimize_constraint.cpp.

bool Clasp::DefaultMinimize::commitLowerBound	(	const Solver &	s,
		bool	upShared
	)

Sets the current local upper bound as the lower bound of this constraint.

commitLowerBound() shall be called on unsat. The function stores the local upper bound as new lower bound in this constraint. If upShared is true, the lower bound is also copied to the shared data object.

Once the local bound is committed, the function integrateBound() has to be called in order to continue optimization.

Returns:: false if search-space is exceeded w.r.t this constraint.

Definition at line 412 of file minimize_constraint.cpp.

void Clasp::DefaultMinimize::commitUpperBound ( const Solver & s )

Sets the current local sum as the global optimum (upper bound).

commitUpperBound() shall be called whenever the solver finds a model. The current local sum is recorded as new optimum in the shared data object. Once the local bound is committed, the function integrateBound() has to be called in order to continue optimization.

Definition at line 408 of file minimize_constraint.cpp.

uint32 Clasp::DefaultMinimize::computeImplicationSet	(	const Solver &	s,
		const WeightLiteral &	it,
		uint32 &	undoPos
	)		`[private]`

Definition at line 293 of file minimize_constraint.cpp.

void Clasp::DefaultMinimize::destroy	(	Solver *	s,
		bool	detach
	)		`[virtual]`

Default is to call delete this.

Reimplemented from Clasp::MinimizeConstraint.

Definition at line 201 of file minimize_constraint.cpp.

wsum_t* Clasp::DefaultMinimize::end ( ) const [inline, private]

Definition at line 395 of file minimize_constraint.h.

bool Clasp::DefaultMinimize::greater	(	wsum_t *	lhs,
		wsum_t *	rhs,
		uint32	len,
		uint32 &	aLev
	)		const `[private]`

Definition at line 279 of file minimize_constraint.cpp.

bool Clasp::DefaultMinimize::handleModel ( Solver & s ) [inline, virtual]

Shall commit the model in s to the shared data object.

The return value indicates whether the model is valid w.r.t the costs stored in the shared data object.

Implements Clasp::MinimizeConstraint.

Definition at line 324 of file minimize_constraint.h.

bool Clasp::DefaultMinimize::handleUnsat	(	Solver &	s,
		bool	upShared,
		LitVec &	restore
	)		`[virtual]`

Shall handle the unsatisfiable path in s.

Implements Clasp::MinimizeConstraint.

Definition at line 424 of file minimize_constraint.cpp.

bool Clasp::DefaultMinimize::integrate ( Solver & s ) [inline, virtual]

Shall activate the minimize constraint by integrating bounds stored in the shared data object.

Implements Clasp::MinimizeConstraint.

Definition at line 322 of file minimize_constraint.h.

bool Clasp::DefaultMinimize::integrateBound ( Solver & s )

Tries to integrate the next tentative bound into this constraint.

Starting from the current optimum stored in the shared data object, the function tries to integrate the next candidate bound into this constraint.

Returns:: The function returns true if integration succeeded. Otherwise false is returned and s.hasConflict() is true.

Note:: If integrateBound() failed, the bound of this constraint is relaxed. The caller has to resolve the conflict first and then integrateBound() shall be called again.; The caller has to call s.propagate() to propagate any new information from the new bound.; If the tag literal (if any) is not true, the minimize constraint first assumes it.

Definition at line 451 of file minimize_constraint.cpp.

uint32 Clasp::DefaultMinimize::lastUndoLevel ( const Solver & s ) const [private]

Definition at line 243 of file minimize_constraint.cpp.

bool Clasp::DefaultMinimize::litSeen ( uint32 i ) const [private]

Definition at line 248 of file minimize_constraint.cpp.

bool Clasp::DefaultMinimize::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 from Clasp::Constraint.

Definition at line 389 of file minimize_constraint.cpp.

bool Clasp::DefaultMinimize::more ( ) const [inline]

Definition at line 382 of file minimize_constraint.h.

uint32 Clasp::DefaultMinimize::numRules ( ) const [inline]

Number of minimize statements contained in this constraint.

Definition at line 335 of file minimize_constraint.h.

wsum_t* Clasp::DefaultMinimize::opt ( ) const [inline, private]

Definition at line 392 of file minimize_constraint.h.

Constraint::PropResult Clasp::DefaultMinimize::propagate	(	Solver &	s,
		Literal	p,
		uint32 &	data
	)		`[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.

Implements Clasp::Constraint.

Definition at line 284 of file minimize_constraint.cpp.