Minimization via unsat cores. More...

#include <minimize_constraint.h>

Inheritance diagram for Clasp::UncoreMinimize:

Classes
struct	Core
struct	LitData
struct	LitPair
struct	WCTemp
Public Member Functions
bool	attach (Solver &s)
	Attaches this object to the given solver.
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.
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	simplify (Solver &s, bool reinit=false)
bool	valid (Solver &s)
	Shall return whether the constraint is valid (i.e. not conflicting) w.r.t the current assignment in s.
Private Types
typedef PodVector< Constraint * > ::type	ConTable
typedef PodVector< Core >::type	CoreTable
typedef DefaultMinimize *	EnumPtr
typedef PodVector< LitPair >::type	LitSet
typedef PodVector< LitData >::type	LitTable
Private Member Functions
bool	addCore (Solver &s, const LitPair *lits, uint32 size, weight_t weight)
bool	addCore (Solver &s, const WCTemp &wc, weight_t w)
LitData &	addLit (Literal p, weight_t w)
uint32	allocCore (WeightConstraint *con, weight_t bound, weight_t weight, bool open)
uint32	analyze (Solver &s, LitVec &cfl, weight_t &minW, LitVec &poppedOther)
bool	closeCore (Solver &s, LitData &x, bool sat)
wsum_t *	computeSum (Solver &s) const
void	detach (Solver *s, bool b)
bool	fixLevel (Solver &s)
bool	fixLit (Solver &s, Literal p)
Core &	getCore (const LitData &x)
LitData &	getData (uint32 id)
bool	hasCore (const LitData &x) const
void	init ()
bool	initLevel (Solver &s)
uint32	initRoot (Solver &s)
void	integrateOpt (Solver &s)
bool	popPath (Solver &s, uint32 dl, LitVec &out)
bool	pushPath (Solver &s)
void	releaseLits ()
void	setLower (wsum_t x)
	UncoreMinimize (SharedData *d, bool preprocess)
bool	validLowerBound () const
Private Attributes
LitSet	assume_
uint32	aTop_
uint32	auxAdd_
uint32	auxInit_
ConTable	closed_
LitVec	conflict_
EnumPtr	enum_
uint32	eRoot_
LitVec	fix_
uint32	freeOpen_
uint32	gen_
uint32	hasPre_: 1
uint32	init_: 1
uint32	level_: 25
LitTable	litData_
wsum_t	lower_
uint32	next_: 1
CoreTable	open_
uint32	path_: 1
uint32	pre_: 1
uint32	sat_: 1
wsum_t *	sum_
WCTemp	temp_
LitSet	todo_
wsum_t	upper_
uint32	valid_: 1
Friends
class	SharedMinimizeData

Detailed Description

Minimization via unsat cores.

Definition at line 423 of file minimize_constraint.h.

Member Typedef Documentation

typedef PodVector<Constraint*>::type Clasp::UncoreMinimize::ConTable [private]

Definition at line 471 of file minimize_constraint.h.

typedef PodVector<Core>::type Clasp::UncoreMinimize::CoreTable [private]

Definition at line 470 of file minimize_constraint.h.

typedef DefaultMinimize* Clasp::UncoreMinimize::EnumPtr [private]

Definition at line 440 of file minimize_constraint.h.

typedef PodVector<LitPair>::type Clasp::UncoreMinimize::LitSet [private]

Definition at line 472 of file minimize_constraint.h.

typedef PodVector<LitData>::type Clasp::UncoreMinimize::LitTable [private]

Definition at line 469 of file minimize_constraint.h.

Constructor & Destructor Documentation

Clasp::UncoreMinimize::UncoreMinimize	(	SharedData *	d,
		bool	preprocess
	)		`[explicit, private]`

Definition at line 805 of file minimize_constraint.cpp.

Member Function Documentation

bool Clasp::UncoreMinimize::addCore	(	Solver &	s,
		const LitPair *	lits,
		uint32	size,
		weight_t	weight
	)		`[private]`

Definition at line 1213 of file minimize_constraint.cpp.

bool Clasp::UncoreMinimize::addCore	(	Solver &	s,
		const WCTemp &	wc,
		weight_t	w
	)		`[private]`

Definition at line 1256 of file minimize_constraint.cpp.

UncoreMinimize::LitData & Clasp::UncoreMinimize::addLit	(	Literal	p,
		weight_t	w
	)		`[private]`

Definition at line 958 of file minimize_constraint.cpp.

uint32 Clasp::UncoreMinimize::allocCore	(	WeightConstraint *	con,
		weight_t	bound,
		weight_t	weight,
		bool	open
	)		`[private]`

Definition at line 1326 of file minimize_constraint.cpp.

uint32 Clasp::UncoreMinimize::analyze	(	Solver &	s,
		LitVec &	cfl,
		weight_t &	minW,
		LitVec &	poppedOther
	)		`[private]`

Definition at line 1154 of file minimize_constraint.cpp.

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

Attaches this object to the given solver.

Implements Clasp::MinimizeConstraint.

Definition at line 830 of file minimize_constraint.cpp.

bool Clasp::UncoreMinimize::closeCore	(	Solver &	s,
		LitData &	x,
		bool	sat
	)		`[private]`

Definition at line 1341 of file minimize_constraint.cpp.

wsum_t * Clasp::UncoreMinimize::computeSum ( Solver & s ) const [private]

Definition at line 1045 of file minimize_constraint.cpp.

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

Default is to call delete this.

Reimplemented from Clasp::MinimizeConstraint.

Definition at line 857 of file minimize_constraint.cpp.

void Clasp::UncoreMinimize::detach	(	Solver *	s,
		bool	b
	)		`[private]`

Definition at line 844 of file minimize_constraint.cpp.

bool Clasp::UncoreMinimize::fixLevel ( Solver & s ) [private]

Definition at line 1307 of file minimize_constraint.cpp.

bool Clasp::UncoreMinimize::fixLit	(	Solver &	s,
		Literal	p
	)		`[private]`

Definition at line 1294 of file minimize_constraint.cpp.

Core& Clasp::UncoreMinimize::getCore ( const LitData & x ) [inline, private]

Definition at line 476 of file minimize_constraint.h.

LitData& Clasp::UncoreMinimize::getData ( uint32 id ) [inline, private]

Definition at line 475 of file minimize_constraint.h.

bool Clasp::UncoreMinimize::handleModel ( Solver & s ) [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 1081 of file minimize_constraint.cpp.

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

Shall handle the unsatisfiable path in s.

Implements Clasp::MinimizeConstraint.

Definition at line 1094 of file minimize_constraint.cpp.

bool Clasp::UncoreMinimize::hasCore ( const LitData & x ) const [inline, private]

Definition at line 474 of file minimize_constraint.h.

void Clasp::UncoreMinimize::init ( ) [private]

Definition at line 814 of file minimize_constraint.cpp.

bool Clasp::UncoreMinimize::initLevel ( Solver & s ) [private]

Definition at line 897 of file minimize_constraint.cpp.

uint32 Clasp::UncoreMinimize::initRoot ( Solver & s ) [private]

Definition at line 1285 of file minimize_constraint.cpp.

bool Clasp::UncoreMinimize::integrate ( Solver & s ) [virtual]

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

Implements Clasp::MinimizeConstraint.

Definition at line 878 of file minimize_constraint.cpp.

void Clasp::UncoreMinimize::integrateOpt ( Solver & s ) [private]

bool Clasp::UncoreMinimize::popPath	(	Solver &	s,
		uint32	dl,
		LitVec &	out
	)		`[private]`

Definition at line 1007 of file minimize_constraint.cpp.

Constraint::PropResult Clasp::UncoreMinimize::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 863 of file minimize_constraint.cpp.

bool Clasp::UncoreMinimize::pushPath ( Solver & s ) [private]

Definition at line 967 of file minimize_constraint.cpp.