org.sat4j.pb.constraints.pb
Class AtLeastPB

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

public final class AtLeastPB
extends AtLeast
implements PBConstr

See Also:
Serialized Form

Field Summary
 
Fields inherited from class org.sat4j.minisat.constraints.card.AtLeast
lits, maxUnsatisfied, voc
 
Method Summary
 void assertConstraint(UnitPropagationListener s)
          Method called when the constraint is to be asserted.
static AtLeastPB atLeastNew(ILits voc, IVecInt ps, int n)
           
static PBConstr atLeastNew(UnitPropagationListener s, ILits voc, IVecInt ps, int n)
           
 IVecInt computeAnImpliedClause()
           
 BigInteger getCoef(int literal)
           
 BigInteger[] getCoefs()
           
 BigInteger getDegree()
           
 int[] getLits()
           
 ILits getVocabulary()
           
 boolean learnt()
          D?
 void register()
          Register the constraint to the solver.
 void setLearnt()
          Mark a constraint as learnt.
 
Methods inherited from class org.sat4j.minisat.constraints.card.AtLeast
calcReason, canBePropagatedMultipleTimes, forwardActivity, get, getActivity, incActivity, locked, niceParameters, propagate, remove, rescaleBy, simplify, size, toString, undo
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 
Methods inherited from interface org.sat4j.minisat.core.Constr
calcReason, forwardActivity, incActivity, locked, remove, rescaleBy, simplify
 
Methods inherited from interface org.sat4j.minisat.core.Propagatable
propagate
 
Methods inherited from interface org.sat4j.specs.IConstr
canBePropagatedMultipleTimes, get, getActivity, size
 

Method Detail

atLeastNew

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

atLeastNew

public static AtLeastPB atLeastNew(ILits voc,
                                   IVecInt ps,
                                   int n)

getCoef

public BigInteger getCoef(int literal)
Specified by:
getCoef in interface PBConstr

getDegree

public BigInteger getDegree()
Specified by:
getDegree in interface PBConstr

getVocabulary

public ILits getVocabulary()
Specified by:
getVocabulary in interface PBConstr

getLits

public int[] getLits()
Specified by:
getLits in interface PBConstr

getCoefs

public BigInteger[] getCoefs()
Specified by:
getCoefs in interface PBConstr

learnt

public boolean learnt()
D?termine si la contrainte est apprise

Specified by:
learnt in interface IConstr
Overrides:
learnt in class AtLeast
Returns:
true si la contrainte est apprise, false sinon
See Also:
IConstr.learnt()

setLearnt

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

Specified by:
setLearnt in interface Constr
Overrides:
setLearnt in class AtLeast

register

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

Specified by:
register in interface Constr
Overrides:
register in class AtLeast

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
Overrides:
assertConstraint in class AtLeast
Parameters:
s - a UnitPropagationListener to use for unit propagation.

computeAnImpliedClause

public IVecInt computeAnImpliedClause()
Specified by:
computeAnImpliedClause in interface PBConstr


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