#include <clause.h>

Inheritance diagram for Clasp::LoopFormula:

Public Member Functions
Activity	activity () const
	Returns the loop-formula's activity.
void	addAtom (Literal atom, Solver &s)
	Adds an atom to the loop-formula.
Constraint *	cloneAttach (Solver &)
	Returns a clone of this and adds necessary watches to the given solver.
void	decreaseActivity ()
	Halves the loop-formula's activity.
void	destroy (Solver *=0, bool=false)
	Default is to call delete this.
uint32	isOpen (const Solver &s, const TypeSet &t, LitVec &freeLits)
	Shall return 0 if either !t.inSet(type()) or this constraint is satisfied w.r.t the current assignment.
bool	locked (const Solver &s) const
bool	minimize (Solver &s, Literal p, CCMinRecursive *ccMin)
PropResult	propagate (Solver &s, Literal p, uint32 &data)
void	reason (Solver &, Literal p, LitVec &lits)
void	resetActivity (Activity hint)
	Asks the constraint to reset its activity.
bool	simplify (Solver &s, bool=false)
uint32	size () const
	Returns the size of the loop-formula.
ConstraintType	type () const
	Returns Constraint_t::learnt_loop.
void	updateHeuristic (Solver &s)
	Notifies the installed heuristic about the new constraint.
Static Public Member Functions
static LoopFormula *	newLoopFormula (Solver &s, Literal *bodyLits, uint32 numBodies, uint32 bodyToWatch, uint32 numAtoms, const Activity &act)
Private Member Functions
bool	isTrue (const Solver &s, uint32 idx)
	LoopFormula (Solver &s, uint32 size, Literal *bodyLits, uint32 numBodies, uint32 bodyToWatch, const Activity &a)
bool	watchable (const Solver &s, uint32 idx)
Private Attributes
Activity	act_
uint32	end_
Literal	lits_ [0]
uint32	other_
uint32	size_

Detailed Description

Constraint for Loop-Formulas.

Special purpose constraint for loop formulas of the form: R -> ~a1, ~a2, ..., ~an where R is a conjunction (B1,...,Bm) of bodies that are false and a1...an are the atoms of an unfounded set. I.e. such a loop formula is equivalent to the following n clauses: ~a1 v B1 v ... v Bm ... ~an v B1 v ... v Bm Representing loop formulas as n clauses is wasteful because each clause contains the same set of bodies.

The idea behind LoopFormula is to treat the conjunction of atoms as a special "macro-literal" L with the following properties:

isTrue(L), iff for all ai isTrue(~ai)
isFalse(L), iff for some ai isFalse(~ai)
L is watchable, iff not isFalse(L)
Watching L means watching all ai.
setting L to true means setting all ai to false. Using this convention the TWL-algo can be implemented as in a clause.

Implementation:

The literal-array is divided into two parts, an "active clause" part and an atom part
The "active clause" contains one atom and all bodies: [B1 ... Bj ~ai]
The atom part contains all atoms: [~a1 ... ~an]
Two of the literals of the "active clause" are watched (again: watching an atom means watching all atoms)
If a watched atom becomes true, it is copied into the "active clause" and the TWL-algo starts.

Definition at line 423 of file clause.h.

Constructor & Destructor Documentation

Clasp::LoopFormula::LoopFormula	(	Solver &	s,
		uint32	size,
		Literal *	bodyLits,
		uint32	numBodies,
		uint32	bodyToWatch,
		const Activity &	a
	)		`[private]`

Definition at line 871 of file clause.cpp.

Member Function Documentation

Activity Clasp::LoopFormula::activity ( ) const [inline, virtual]

Returns the loop-formula's activity.

The activity of a loop-formula is increased, whenever reason() is called.

Reimplemented from Clasp::LearntConstraint.

Definition at line 466 of file clause.h.

void Clasp::LoopFormula::addAtom	(	Literal	atom,
		Solver &	s
	)

Adds an atom to the loop-formula.

Precondition:: the loop-formula currently contains fewer than numAtoms atoms

Definition at line 916 of file clause.cpp.

Constraint* Clasp::LoopFormula::cloneAttach ( Solver & other ) [inline, 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.

Definition at line 450 of file clause.h.

void Clasp::LoopFormula::decreaseActivity ( ) [inline, virtual]

Halves the loop-formula's activity.

Reimplemented from Clasp::LearntConstraint.

Definition at line 469 of file clause.h.

void Clasp::LoopFormula::destroy	(	Solver *	s = `0`,
		bool	detach = `false`
	)		`[virtual]`

Default is to call delete this.

Reimplemented from Clasp::Constraint.

Definition at line 888 of file clause.cpp.

uint32 Clasp::LoopFormula::isOpen	(	const Solver &	s,
		const TypeSet &	t,
		LitVec &	freeLits
	)		`[virtual]`

Shall return 0 if either !t.inSet(type()) or this constraint is satisfied w.r.t the current assignment.

If this constraint is currently not satisfied and t.inSet(type()), shall return type() and freeLits shall contain all currently unassigned literals of this constraint.

Implements Clasp::LearntConstraint.

Definition at line 1065 of file clause.cpp.

bool Clasp::LoopFormula::isTrue	(	const Solver &	s,
		uint32	idx
	)		`[private]`

Definition at line 950 of file clause.cpp.

bool Clasp::LoopFormula::locked ( const Solver & s ) const [virtual]

Shall return true if this constraint can't be deleted because it currently implies one ore more literals and false otherwise.

Implements Clasp::LearntConstraint.

Definition at line 1053 of file clause.cpp.

bool Clasp::LoopFormula::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 1038 of file clause.cpp.

LoopFormula * Clasp::LoopFormula::newLoopFormula	(	Solver &	s,
		Literal *	bodyLits,
		uint32	numBodies,
		uint32	bodyToWatch,
		uint32	numAtoms,
		const Activity &	act
	)		`[static]`

Creates a new loop-formula for numAtoms atoms sharing the literals contained in bodyLits.

Parameters:

s	Solver in which the new loop-formula is to be used.
bodyLits	Pointer to an array of numBodies body-literals.
numBodies	Number of body-literals in bodyLits.
numAtoms	Number of atoms in the loop-formula.

Precondition:: all body-literals are currently false.

Definition at line 865 of file clause.cpp.

Constraint::PropResult Clasp::LoopFormula::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 961 of file clause.cpp.