org.sat4j.minisat.constraints.card
Class AtLeast

java.lang.Object
  extended by org.sat4j.minisat.constraints.card.AtLeast
All Implemented Interfaces:
Serializable, Constr, Propagatable, Undoable, IConstr

public class AtLeast
extends Object
implements Constr, Undoable, Serializable

Author:
leberre Contrainte de cardinalit?
See Also:
Serialized Form

Field Summary
protected  int[] lits
          constraint literals
protected  int maxUnsatisfied
          number of allowed falsified literal
protected  ILits voc
           
 
Constructor Summary
protected AtLeast(ILits voc, IVecInt ps, int degree)
           
 
Method Summary
 void assertConstraint(UnitPropagationListener s)
          Method called when the constraint is to be asserted.
static Constr atLeastNew(UnitPropagationListener s, ILits voc, IVecInt ps, int n)
           
 void calcReason(int p, IVecInt outReason)
          Compute the reason for a given assignment.
 boolean canBePropagatedMultipleTimes()
          Partition constraints into the ones that can only be found once on the trail (e.g. clauses) and the ones that can be found several times (e.g.
 void forwardActivity(double claInc)
           
 int get(int i)
          returns the ith literal in the constraint
 double getActivity()
          To obtain the activity of the constraint.
 void incActivity(double claInc)
          Increase the constraint activity.
 boolean learnt()
           
 boolean locked()
          Indicate wether a constraint is responsible from an assignment.
protected static int niceParameters(UnitPropagationListener s, ILits voc, IVecInt ps, int deg)
           
 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(UnitPropagationListener upl)
          Remove a constraint from the solver.
 void rescaleBy(double d)
          Rescale the clause activity by a value.
 void setLearnt()
          Mark a constraint as learnt.
 boolean simplify()
          Simplifies a constraint, by removing top level falsified literals for instance.
 int size()
           
 String toString()
          Cha?
 void undo(int p)
          Method called when backtracking
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Field Detail

maxUnsatisfied

protected int maxUnsatisfied
number of allowed falsified literal


lits

protected final int[] lits
constraint literals


voc

protected final ILits voc
Constructor Detail

AtLeast

protected AtLeast(ILits voc,
                  IVecInt ps,
                  int degree)
Parameters:
ps - a vector of literals
degree - the minimal number of satisfied literals
Method Detail

niceParameters

protected static int niceParameters(UnitPropagationListener s,
                                    ILits voc,
                                    IVecInt ps,
                                    int deg)
                             throws ContradictionException
Throws:
ContradictionException

atLeastNew

public static Constr atLeastNew(UnitPropagationListener s,
                                ILits voc,
                                IVecInt ps,
                                int n)
                         throws ContradictionException
Throws:
ContradictionException
Since:
2.1

remove

public void remove(UnitPropagationListener upl)
Description copied from interface: Constr
Remove a constraint from the solver.

Specified by:
remove in interface Constr
Since:
2.1

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
Simplifies a constraint, by removing top level falsified literals for instance.

Specified by:
simplify in interface Constr
Returns:
true iff the constraint is satisfied and can be removed from the database.

undo

public void undo(int p)
Description copied from interface: Undoable
Method called when backtracking

Specified by:
undo in interface Undoable
Parameters:
p - a literal to be unassigned.

calcReason

public void calcReason(int p,
                       IVecInt outReason)
Description copied from interface: Constr
Compute the reason for a given assignment. If the constraint is a clause, it is supposed to be either a unit clause or a falsified one.

Specified by:
calcReason in interface Constr
Parameters:
p - a satisfied literal (or Lit.UNDEFINED)
outReason - the list of falsified literals whose negation is the reason of the assignment of p to true.

learnt

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

getActivity

public double getActivity()
Description copied from interface: IConstr
To obtain the activity of the constraint.

Specified by:
getActivity in interface IConstr
Returns:
the activity of the clause.

incActivity

public void incActivity(double claInc)
Description copied from interface: Constr
Increase the constraint activity.

Specified by:
incActivity in interface Constr
Parameters:
claInc - the value to increase the activity with

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

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

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.

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.

toString

public String toString()
Cha?ne repr?sentant la contrainte

Overrides:
toString in class Object
Returns:
Cha?ne repr?sentant la contrainte

forwardActivity

public void forwardActivity(double claInc)
Specified by:
forwardActivity in interface Constr
Since:
2.1

canBePropagatedMultipleTimes

public boolean canBePropagatedMultipleTimes()
Description copied from interface: IConstr
Partition constraints into the ones that can only be found once on the trail (e.g. clauses) and the ones that can be found several times (e.g. cardinality constraints and pseudo-boolean constraints).

Specified by:
canBePropagatedMultipleTimes in interface IConstr
Returns:
true if the constraint can be used several times as a reason to propagate a literal.


Copyright © 2011 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.