org.sat4j.minisat.constraints.cnf
Class WLClause

java.lang.Object
  org.sat4j.minisat.constraints.cnf.WLClause

All Implemented Interfaces:

java.io.Serializable, Constr, Propagatable, IConstr

public final class WLClause
extends java.lang.Object
implements Constr, java.io.Serializable

Lazy data structure for clause using Watched Literals.

Author:

leberre

See Also:

Serialized Form

Constructor Summary

WLClause(IVecInt ps, ILits voc)
Creates a new basic clause

Method Summary

void	assertConstraint(UnitPropagationListener s) Method called when the constraint is to be asserted.
static WLClause	brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals) Creates a brand new clause, presumably from external data.
void	calcReason(int p, IVecInt outReason) Calcule la cause de l'affection d'un litt?
int	get(int i) Retourne le ieme literal de la clause.
double	getActivity()
int	getId()
void	incActivity(double claInc)
static int	lastid()
boolean	learnt()
boolean	locked() Indicate wether a constraint is responsible from an assignment.
boolean	propagate(UnitPropagationListener s, int p) Propagate the truth value of a literal in constraints in which that literal is falsified.
void	register() Register this clause which means watching the necessary literals If the clause is learnt, setLearnt() must be called before a call to register()
void	remove() Enl?
void	rescaleBy(double d) Rescale the clause activity by a value.
static void	resetIds()
static IVecInt	sanityCheck(IVecInt ps, ILits voc, UnitPropagationListener s) Perform some sanity check before constructing a clause a) if a literal is assigned true, return null (the clause is satisfied) b) if a literal is assigned false, remove it c) if a clause contains a literal and its opposite (tautology) return null d) remove duplicate literals e) if the clause is empty, return null f) if the clause if unit, transmit it to the object responsible for unit propagation
void	setLearnt() declares this clause as learnt
boolean	simplify() Simplifie une contrainte, par exemple en enlevant les litt?
int	size()
java.lang.String	toString()

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

Constructor Detail

WLClause

public WLClause(IVecInt ps,
                ILits voc)

Creates a new basic clause

Parameters:

voc - the vocabulary of the formula

ps - A VecInt that WILL BE EMPTY after calling that method.

Method Detail

getId

public int getId()

resetIds

public static void resetIds()

sanityCheck

public static IVecInt sanityCheck(IVecInt ps,
                                  ILits voc,
                                  UnitPropagationListener s)
                           throws ContradictionException

Perform some sanity check before constructing a clause a) if a literal is assigned true, return null (the clause is satisfied) b) if a literal is assigned false, remove it c) if a clause contains a literal and its opposite (tautology) return null d) remove duplicate literals e) if the clause is empty, return null f) if the clause if unit, transmit it to the object responsible for unit propagation

Parameters:

ps - the list of literals

voc - the vocabulary used

s - the object responsible for unit propagation

Returns:

null if the clause should be ignored, the (possibly modified) list of literals otherwise

Throws:

ContradictionException - if discovered by unit propagation

setLearnt

public void setLearnt()

declares this clause as learnt

Specified by:

setLearnt in interface Constr

register

public void register()

Register this clause which means watching the necessary literals If the clause is learnt, setLearnt() must be called before a call to register()

Specified by:

register in interface Constr

See Also:

setLearnt()

brandNewClause

public static WLClause brandNewClause(UnitPropagationListener s,
                                      ILits voc,
                                      IVecInt literals)

Creates a brand new clause, presumably from external data. Performs all sanity checks.

Parameters:

s - the object responsible for unit propagation

voc - the vocabulary

literals - the literals to store in the clause

Returns:

the created clause or null if the clause should be ignored (tautology for example)

calcReason

public void calcReason(int p,
                       IVecInt outReason)

Description copied from interface: Constr

Calcule la cause de l'affection d'un litt?ral

Specified by:

calcReason in interface Constr

Parameters:

p - un litt?ral falsifi? (ou Lit.UNDEFINED)

outReason - la liste des litt?raux falsifi?s dont la n?gation correspond ? la raison de l'affectation.

remove

public void remove()

Description copied from interface: Constr

Enl?ve une contrainte du prouveur

Specified by:

remove in interface Constr

simplify

public boolean simplify()

Description copied from interface: Constr

Simplifie une contrainte, par exemple en enlevant les litt?raux falsifi?s.

Specified by:

simplify in interface Constr

Returns:

true ssi la contrainte est satisfaite.

propagate

public boolean propagate(UnitPropagationListener s,
                         int p)

Description copied from interface: Propagatable

Propagate the truth value of a literal in constraints in which that literal is falsified.

Specified by:

propagate in interface Propagatable

Parameters:

s - something able to perform unit propagation

p - the literal being propagated. Its negation must appear in the constraint.

Returns:

false iff an inconsistency (a contradiction) is detected.

locked

public boolean locked()

Description copied from interface: Constr

Indicate wether a constraint is responsible from an assignment.

Specified by:

locked in interface Constr

Returns:

true if a constraint is a "reason" for an assignment.

getActivity

public double getActivity()

Specified by:

getActivity in interface Constr

Returns:

the activity of the clause

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

get

public int get(int i)

Retourne le ieme literal de la clause. Attention, cet ordre change durant la recherche.

Specified by:

get in interface IConstr

Parameters:

i - the index of the literal

Returns:

the literal

incActivity

public void incActivity(double claInc)

Specified by:

incActivity in interface Constr

Parameters:

claInc -

rescaleBy

public void rescaleBy(double d)

Description copied from interface: Constr

Rescale the clause activity by a value.

Specified by:

rescaleBy in interface Constr

Parameters:

d -

learnt

public boolean learnt()

Specified by:

learnt in interface IConstr

Returns:

true iff the clause was learnt during the search

size

public int size()

Specified by:

size in interface IConstr

Returns:

the number of literals in the constraint.

lastid

public static int lastid()

Returns:

the id the the last created clause.

assertConstraint

public void assertConstraint(UnitPropagationListener s)

Description copied from interface: Constr

Method called when the constraint is to be asserted. It means that the constraint was learnt during the search and it should now propagate some truth values. In the clausal case, only one literal should be propagated. In other cases, it might be different.

Specified by:

assertConstraint in interface Constr

Parameters:

s - a UnitPropagationListener to use for unit propagation.