org.sat4j.pb.constraints.pb
Class LearntHTClausePB
java.lang.Object
org.sat4j.minisat.constraints.cnf.HTClause
org.sat4j.minisat.constraints.cnf.LearntHTClause
org.sat4j.pb.constraints.pb.LearntHTClausePB
- All Implemented Interfaces:
- Serializable, Constr, Propagatable, PBConstr, IConstr
public final class LearntHTClausePB
- extends LearntHTClause
- implements PBConstr
- See Also:
- Serialized Form
Methods inherited from class org.sat4j.minisat.constraints.cnf.HTClause |
calcReason, canBePropagatedMultipleTimes, equals, get, getActivity, getLits, getVocabulary, hashCode, locked, propagate, remove, rescaleBy, simplify, size, toString |
LearntHTClausePB
public LearntHTClausePB(IVecInt ps,
ILits voc)
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 HTClause
- Parameters:
s
- a UnitPropagationListener to use for unit propagation.
computeAnImpliedClause
public IVecInt computeAnImpliedClause()
- Specified by:
computeAnImpliedClause
in interface PBConstr
getCoef
public BigInteger getCoef(int literal)
- Specified by:
getCoef
in interface PBConstr
getCoefs
public BigInteger[] getCoefs()
- Specified by:
getCoefs
in interface PBConstr
getDegree
public BigInteger getDegree()
- Specified by:
getDegree
in interface PBConstr
Copyright © 2011 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.