org.sat4j.pb.constraints.pb
Class BinaryClausePB

java.lang.Object
  org.sat4j.minisat.constraints.cnf.BinaryClause
      org.sat4j.pb.constraints.pb.BinaryClausePB

All Implemented Interfaces:

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

public class BinaryClausePB
extends BinaryClause
implements PBConstr

See Also:

Serialized Form

Constructor Summary

BinaryClausePB(IVecInt ps, ILits voc)

Method Summary

static BinaryClausePB	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()
boolean	learnt()
void	setLearnt()

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

assertConstraint, calcReason, equals, get, getActivity, getLits, getVocabulary, hashCode, incActivity, 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, getActivity, incActivity, locked, register, remove, rescaleBy, simplify

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

propagate

Methods inherited from interface org.sat4j.specs.IConstr

get, size

Constructor Detail

BinaryClausePB

public BinaryClausePB(IVecInt ps,
                      ILits voc)

Method Detail

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

setLearnt

public void setLearnt()

Specified by:

setLearnt in interface Constr

learnt

public boolean learnt()

Specified by:

learnt in interface IConstr

brandNewClause

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

Creates a brand new clause, presumably from external data. Performs all sanity checks.

Parameters:

s - the object responsible for unit propagation

voc - the vocabulary

literals - the literals to store in the clause (size should be two)

Returns:

the created clause or null if the clause should be ignored (tautology for example)