org.sat4j.minisat.constraints.pb
Class MixableCBClausePB

java.lang.Object
  extended by org.sat4j.minisat.constraints.cnf.CBClause
      extended by org.sat4j.minisat.constraints.cnf.MixableCBClause
          extended by org.sat4j.minisat.constraints.pb.MixableCBClausePB
All Implemented Interfaces:
java.io.Serializable, PBConstr, Constr, Propagatable, Undoable, IConstr

public class MixableCBClausePB
extends MixableCBClause
implements PBConstr

See Also:
Serialized Form

Field Summary
 
Fields inherited from class org.sat4j.minisat.constraints.cnf.CBClause
falsified, lits, voc
 
Constructor Summary
MixableCBClausePB(IVecInt ps, ILits voc)
           
MixableCBClausePB(IVecInt ps, ILits voc, boolean learnt)
           
 
Method Summary
 void assertConstraint(UnitPropagationListener s)
          Method called when the constraint is to be asserted.
static MixableCBClausePB brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals)
           
 IVecInt computeAnImpliedClause()
           
 java.math.BigInteger getCoef(int literal)
           
 java.math.BigInteger[] getCoefs()
           
 java.math.BigInteger getDegree()
           
 int[] getLits()
           
 ILits getVocabulary()
           
 
Methods inherited from class org.sat4j.minisat.constraints.cnf.MixableCBClause
propagate
 
Methods inherited from class org.sat4j.minisat.constraints.cnf.CBClause
calcReason, get, getActivity, incActivity, learnt, locked, register, remove, rescaleBy, setLearnt, 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, getActivity, incActivity, locked, register, remove, rescaleBy, setLearnt, simplify
 
Methods inherited from interface org.sat4j.minisat.core.Propagatable
propagate
 
Methods inherited from interface org.sat4j.specs.IConstr
get, learnt, size
 

Constructor Detail

MixableCBClausePB

public MixableCBClausePB(IVecInt ps,
                         ILits voc,
                         boolean learnt)

MixableCBClausePB

public MixableCBClausePB(IVecInt ps,
                         ILits voc)
Method Detail

brandNewClause

public static MixableCBClausePB brandNewClause(UnitPropagationListener s,
                                               ILits voc,
                                               IVecInt literals)

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

getLits

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

getVocabulary

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

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 CBClause
Parameters:
s - a UnitPropagationListener to use for unit propagation.


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