org.sat4j.pb.constraints.pb
Class OriginalBinaryClausePB

java.lang.Object
  extended by org.sat4j.minisat.constraints.cnf.BinaryClause
      extended by org.sat4j.minisat.constraints.cnf.OriginalBinaryClause
          extended by org.sat4j.pb.constraints.pb.OriginalBinaryClausePB
All Implemented Interfaces:
Serializable, Constr, Propagatable, PBConstr, IConstr

public final class OriginalBinaryClausePB
extends OriginalBinaryClause
implements PBConstr

See Also:
Serialized Form

Field Summary
 
Fields inherited from class org.sat4j.minisat.constraints.cnf.BinaryClause
activity, head, tail
 
Constructor Summary
OriginalBinaryClausePB(IVecInt ps, ILits voc)
           
 
Method Summary
static OriginalBinaryClausePB brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals)
          Creates a brand new clause, presumably from external data.
 IVecInt computeAnImpliedClause()
           
 BigInteger getCoef(int literal)
           
 BigInteger[] getCoefs()
           
 BigInteger getDegree()
           
 
Methods inherited from class org.sat4j.minisat.constraints.cnf.OriginalBinaryClause
forwardActivity, incActivity, learnt, setLearnt
 
Methods inherited from class org.sat4j.minisat.constraints.cnf.BinaryClause
assertConstraint, calcReason, canBePropagatedMultipleTimes, equals, get, getActivity, getLits, getVocabulary, hashCode, locked, propagate, register, remove, rescaleBy, simplify, size, 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
assertConstraint, calcReason, forwardActivity, 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
canBePropagatedMultipleTimes, get, getActivity, learnt, size
 

Constructor Detail

OriginalBinaryClausePB

public OriginalBinaryClausePB(IVecInt ps,
                              ILits voc)
Method Detail

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

brandNewClause

public static OriginalBinaryClausePB brandNewClause(UnitPropagationListener s,
                                                    ILits voc,
                                                    IVecInt literals)
Creates a brand new clause, presumably from external data.

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


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