Class WLClausePB

  extended by org.sat4j.minisat.constraints.cnf.WLClause
      extended by org.sat4j.minisat.constraints.pb.WLClausePB
All Implemented Interfaces:, PBConstr, Constr, Propagatable, IConstr

public class WLClausePB
extends WLClause
implements PBConstr

See Also:
Serialized Form

Constructor Summary
WLClausePB(IVecInt ps, ILits voc)
Method Summary
 void assertConstraint(UnitPropagationListener s)
          Method called when the constraint is to be asserted.
static WLClausePB brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals)
          Creates a brand new clause, presumably from external data.
 IVecInt computeAnImpliedClause()
 java.math.BigInteger getCoef(int literal)
 java.math.BigInteger[] getCoefs()
 java.math.BigInteger getDegree()
Methods inherited from class org.sat4j.minisat.constraints.cnf.WLClause
calcReason, get, getActivity, getLits, getVocabulary, incActivity, learnt, locked, propagate, register, remove, rescaleBy, sanityCheck, setLearnt, simplify, size, toString
Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, wait, wait, wait
Methods inherited from interface org.sat4j.minisat.constraints.pb.PBConstr
getLits, getVocabulary
Methods inherited from interface org.sat4j.minisat.core.Constr
calcReason, getActivity, incActivity, locked, register, remove, rescaleBy, setLearnt, simplify
Methods inherited from interface org.sat4j.minisat.core.Propagatable
Methods inherited from interface org.sat4j.specs.IConstr
get, learnt, size

Constructor Detail


public WLClausePB(IVecInt ps,
                  ILits voc)
Method Detail


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


public java.math.BigInteger getDegree()
Specified by:
getDegree in interface PBConstr


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


public static WLClausePB brandNewClause(UnitPropagationListener s,
                                        ILits voc,
                                        IVecInt literals)
Creates a brand new clause, presumably from external data. Performs all sanity checks.

s - the object responsible for unit propagation
voc - the vocabulary
literals - the literals to store in the clause
the created clause or null if the clause should be ignored (tautology for example)


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


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