Class implementing smodels-like cardinality- and weight constraints. More...

#include <weight_constraint.h>

Inheritance diagram for Clasp::WeightConstraint:

Collaboration diagram for Clasp::WeightConstraint:

Classes
class	CPair

Public Types
enum	CreationFlags { create_explicit = 1u, create_no_add = 3u, create_sat = 4u, create_no_freeze = 8u, create_no_share =16u, create_eq_bound =32u, create_only_btb =64u, create_only_bfb =128u }

enum	ActiveConstraint { FFB_BTB = 0, FTB_BFB = 1 }

Public Member Functions
Constraint *	cloneAttach (Solver &)
	Returns a clone of this and adds necessary watches to the given solver. More...

bool	simplify (Solver &s, bool=false)

void	destroy (Solver *, bool)
	Default is to call delete this. More...

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

void	reason (Solver &, Literal p, LitVec &lits)

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

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

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

Literal	lit (uint32 i, ActiveConstraint c) const

weight_t	weight (uint32 i) const
	Returns the weight of the i'th literal or 1 if constraint is a cardinality constraint. More...

uint32	size () const
	Returns the number of literals in this constraint (including W). More...

bool	isWeight () const
	Returns false if constraint is a cardinality constraint. More...

uint32	getBpIndex () const

Public Member Functions inherited from Clasp::Constraint
	Constraint ()

virtual ConstraintType	type () const
	Returns the type of this constraint. 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...

Static Public Member Functions
static CPair	create (Solver &s, Literal W, WeightLitVec &lits, weight_t bound, uint32 creationFlags=0)
	Creates a new weight constraint from the given weight literals. More...

static CPair	create (Solver &s, Literal W, WeightLitsRep rep, uint32 creationFlags)

Additional Inherited Members
Protected Member Functions inherited from Clasp::Constraint
virtual	~Constraint ()

Detailed Description

Class implementing smodels-like cardinality- and weight constraints.

This class represents a constraint of type W == w1*x1 ... wn*xn >= B, where W and each xi are literals and B and each wi are strictly positive integers. The class is used to represent smodels-like weight constraint, i.e. the body of a basic weight rule. In this case W is the literal associated with the body. A cardinality constraint is handled like a weight constraint where all weights are equal to 1.

The class implements the following four inference rules: Let L be the set of literals of the constraint, let sumTrue be the sum of the weights of all literals l in L that are currently true, let sumReach be the sum of the weights of all literals l in L that are currently not false, let U = {l in L | value(l.var()) == value_free}

FTB: If sumTrue >= bound: set W to true.
BFB: If W is false: set false all literals l in U for which sumTrue + weight(l) >= bound.
FFB: If sumReach < bound: set W to false.
BTB: If W is true: set true all literals l in U for which sumReach - weight(l) < bound.

Member Enumeration Documentation

enum Clasp::WeightConstraint::ActiveConstraint

Logically, we distinguish two constraints: FFB_BTB for handling forward false body and backward true body and FTB_BFB for handling forward true body and backward false body. Physically, we store the literals in one array: ~W=1, l0=w0,...,ln-1=wn-1.

Enumerator
FFB_BTB	(SumW-bound)+1 [~W=1, l0=w0,..., ln-1=wn-1];
FTB_BFB	bound [ W=1,~l0=w0,...,~ln-1=wn-1]

enum Clasp::WeightConstraint::CreationFlags

Enumerator
create_explicit	Force creation of explicit constraint even if size/bound is small.
create_no_add	Do not add constraint to solver db.
create_sat	Force creation even if constraint is always satisfied.
create_no_freeze	Do not freeze variables in constraint.
create_no_share	Do not allow sharing of literals.
create_eq_bound	Create equality instead of less-than constraint.
create_only_btb	Only create FFB_BTB constraint.
create_only_bfb	Only create FTB_BFB constraint.

Member Function Documentation

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

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.

Implements Clasp::Constraint.

Here is the call graph for this function:

WeightConstraint::CPair Clasp::WeightConstraint::create	(	Solver &	s,
		Literal	W,
		WeightLitVec &	lits,
		weight_t	bound,
		uint32	creationFlags = `0`
	)

static

Creates a new weight constraint from the given weight literals.

If the right hand side of the weight constraint is initially true/false (FTB/FFB), W is assigned appropriately but no constraint is created. Otherwise, the new weight constraint is added to s unless creationFlags contains create_no_add.

Parameters

s	Solver in which the new constraint is to be used.
W	The literal that is associated with the constraint.
lits	The literals of the weight constraint.
bound	The lower bound of the weight constraint.

Note: Cardinality constraint are represented as weight constraints with all weights equal to 1.; If creationFlags contains create_eq_bound, a constraint W == (lits == bound) is created that is represented by up to two weight constraints.

Here is the call graph for this function:

WeightConstraint::CPair Clasp::WeightConstraint::create	(	Solver &	s,
		Literal	W,
		WeightLitsRep	rep,
		uint32	creationFlags
	)

static

Here is the call graph for this function:

void Clasp::WeightConstraint::destroy	(	Solver *	s,
		bool	detach
	)

virtual

Default is to call delete this.

Reimplemented from Clasp::Constraint.

Here is the call graph for this function:

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

virtual

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

Reimplemented from Clasp::Constraint.

Here is the call graph for this function:

uint32 Clasp::WeightConstraint::getBpIndex ( ) const

inline

Here is the call graph for this function:

bool Clasp::WeightConstraint::isWeight ( ) const

inline

Returns false if constraint is a cardinality constraint.

Literal Clasp::WeightConstraint::lit	(	uint32	i,
		ActiveConstraint	c
	)		const

inline

Returns the i'th literal of constraint c, i.e. li, iff c == FFB_BTB ~li, iff c == FTB_BFB.

Here is the call graph for this function:

bool Clasp::WeightConstraint::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.

Here is the call graph for this function:

Constraint::PropResult Clasp::WeightConstraint::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.

Here is the call graph for this function:

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

virtual

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

Postcondition: The literals implying p were added to lits.

Implements Clasp::Constraint.

Here is the call graph for this function:

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

Here is the call graph for this function:

uint32 Clasp::WeightConstraint::size ( ) const

inline

Returns the number of literals in this constraint (including W).

void Clasp::WeightConstraint::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 from Clasp::Constraint.

Here is the call graph for this function:

weight_t Clasp::WeightConstraint::weight ( uint32 i ) const

inline

Returns the weight of the i'th literal or 1 if constraint is a cardinality constraint.

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

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

Classes

Public Types

Public Member Functions

Static Public Member Functions

Additional Inherited Members

Detailed Description

Member Enumeration Documentation

Member Function Documentation