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:

java.io.Serializable, Constr, Propagatable, PBConstr, IConstr

public final class LearntHTClausePB
extends LearntHTClause
implements PBConstr

See Also:

Serialized Form

Field Summary

Fields inherited from class org.sat4j.minisat.constraints.cnf.HTClause

activity, head, middleLits, tail, voc

Constructor Summary

Constructors

Constructor and Description
LearntHTClausePB(IVecInt ps, ILits voc)

Method Summary

Modifier and Type	Method and Description
void	assertConstraint(UnitPropagationListener s) Method called when the constraint is to be asserted.
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.LearntHTClause

forwardActivity, incActivity, learnt, register, setActivity, setLearnt

Methods inherited from class org.sat4j.minisat.constraints.cnf.HTClause

assertConstraintIfNeeded, calcReason, calcReasonOnTheFly, canBePropagatedMultipleTimes, equals, get, getActivity, getLits, getVocabulary, hashCode, locked, propagate, remove, rescaleBy, simplify, size, toConstraint, toString

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Methods inherited from interface org.sat4j.pb.constraints.pb.PBConstr

getLits, getVocabulary

Methods inherited from interface org.sat4j.minisat.core.Constr

assertConstraintIfNeeded, calcReason, calcReasonOnTheFly, forwardActivity, incActivity, locked, register, remove, rescaleBy, setActivity, setLearnt, simplify

Methods inherited from interface org.sat4j.specs.IConstr

canBePropagatedMultipleTimes, get, getActivity, learnt, size

Constructor Detail

LearntHTClausePB

public LearntHTClausePB(IVecInt ps,
                        ILits voc)

Method Detail

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 learned 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 java.math.BigInteger getCoef(int literal)

Specified by:

getCoef in interface PBConstr

getCoefs

public java.math.BigInteger[] getCoefs()

Specified by:

getCoefs in interface PBConstr

getDegree

public java.math.BigInteger getDegree()

Specified by:

getDegree in interface PBConstr