org.sat4j.minisat.constraints.cnf
Class BinaryClauses

java.lang.Object
  extended by org.sat4j.minisat.constraints.cnf.BinaryClauses
All Implemented Interfaces:
java.io.Serializable, Constr, Propagatable, IConstr

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

Author:
leberre To change the template for this generated type comment go to Window>Preferences>Java>Code Generation>Code and Comments
See Also:
Serialized Form

Constructor Summary
BinaryClauses(ILits voc, int p)
           
 
Method Summary
 void addBinaryClause(int p)
           
 void assertConstraint(UnitPropagationListener s)
          Method called when the constraint is to be asserted.
 void calcReason(int p, IVecInt outReason)
          Calcule la cause de l'affection d'un litt?
 int get(int i)
          returns the ith literal in the constraint
 double getActivity()
           
 void incActivity(double claInc)
           
 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 the constraint to the solver.
 void remove()
          Enl?
 void rescaleBy(double d)
          Rescale the clause activity by a value.
 void setLearnt()
          Mark a constraint as learnt.
 boolean simplify()
          Simplifie une contrainte, par exemple en enlevant les litt?
 int size()
           
 void undo(int p)
           
 
Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

BinaryClauses

public BinaryClauses(ILits voc,
                     int p)
Method Detail

addBinaryClause

public void addBinaryClause(int p)

remove

public void remove()
Description copied from interface: Constr
Enl?ve une contrainte du prouveur

Specified by:
remove in interface Constr

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.

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.

undo

public void undo(int p)

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.

learnt

public boolean learnt()
Specified by:
learnt in interface IConstr
Returns:
true iff the clause was learnt during the search

incActivity

public void incActivity(double claInc)
Specified by:
incActivity in interface Constr
Parameters:
claInc - the value to increase the activity with

getActivity

public double getActivity()
Specified by:
getActivity in interface Constr
Returns:
the activity of the clause.

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.

setLearnt

public void setLearnt()
Description copied from interface: Constr
Mark a constraint as learnt.

Specified by:
setLearnt in interface Constr

register

public void register()
Description copied from interface: Constr
Register the constraint to the solver.

Specified by:
register in interface Constr

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 - the value to rescale the clause activity with.

size

public int size()
Specified by:
size in interface IConstr
Returns:
the number of literals in the constraint.

get

public int get(int i)
Description copied from interface: IConstr
returns the ith literal in the constraint

Specified by:
get in interface IConstr
Parameters:
i - the index of the literal
Returns:
a literal

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.