Package | Description |
---|---|
org.sat4j.csp |
Classes needed for CSP to SAT translation.
|
org.sat4j.minisat.constraints |
Implementations of various constraints for MiniSAT.
|
org.sat4j.minisat.constraints.card |
Implementations of cardinality constraints.
|
org.sat4j.minisat.constraints.cnf |
Implementations of clausal constraints.
|
org.sat4j.minisat.core |
Implementation of the MiniSAT solver skeleton.
|
org.sat4j.minisat.learning |
Various learning strategies.
|
org.sat4j.minisat.orders |
Various heuristics to select the next variable to branch on.
|
org.sat4j.pb.constraints |
Implementation of data structures for pseudo boolean constraints.
|
org.sat4j.pb.constraints.pb |
Implementations of pseudo boolean constraints.
|
Modifier and Type | Method and Description |
---|---|
static <L extends ILits> |
SolverFactory.newMiniSAT(DataStructureFactory dsf) |
Modifier and Type | Field and Description |
---|---|
protected ILits |
AbstractDataStructureFactory.lits |
Modifier and Type | Method and Description |
---|---|
protected ILits |
ClausalDataStructureWL.createLits() |
protected abstract ILits |
AbstractDataStructureFactory.createLits() |
protected ILits |
MixedDataStructureSingleWL.createLits() |
protected ILits |
AbstractCardinalityDataStructure.createLits() |
protected ILits |
MixedDataStructureDanielHT.createLits() |
protected ILits |
MixedDataStructureDanielWL.createLits() |
ILits |
AbstractDataStructureFactory.getVocabulary() |
Modifier and Type | Field and Description |
---|---|
protected ILits |
AtLeast.voc |
Modifier and Type | Method and Description |
---|---|
ILits |
MaxWatchCard.getVocabulary() |
ILits |
MinWatchCard.getVocabulary() |
Modifier and Type | Method and Description |
---|---|
static Constr |
AtLeast.atLeastNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
int n) |
protected static int |
MinWatchCard.linearisation(ILits voc,
IVecInt ps)
Simplifies the constraint w.r.t. the assignments of the literals
|
static Constr |
MaxWatchCard.maxWatchCardNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
boolean moreThan,
int degree)
Permet la cr?
|
static Constr |
MinWatchCard.minWatchCardNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
boolean moreThan,
int degree)
Constructs a cardinality constraint with a minimal set of watched
literals Permet la cr?
|
protected static int |
AtLeast.niceParameters(UnitPropagationListener s,
ILits voc,
IVecInt ps,
int deg) |
Constructor and Description |
---|
AtLeast(ILits voc,
IVecInt ps,
int degree) |
MaxWatchCard(ILits voc,
IVecInt ps,
boolean moreThan,
int degree)
Constructeur de base cr?
|
MinWatchCard(ILits voc,
IVecInt ps,
boolean moreThan,
int degree)
Constructs and normalizes a cardinality constraint. used by
minWatchCardNew in the non-normalized case.
|
MinWatchCard(ILits voc,
IVecInt ps,
int degree)
Constructs and normalizes a cardinality constraint. used by
MinWatchCardPB.normalizedMinWatchCardNew() in the normalized case.
|
Modifier and Type | Class and Description |
---|---|
class |
Lits |
Modifier and Type | Field and Description |
---|---|
protected ILits |
HTClause.voc |
protected ILits |
WLClause.voc |
Modifier and Type | Method and Description |
---|---|
ILits |
HTClause.getVocabulary() |
ILits |
WLClause.getVocabulary() |
ILits |
BinaryClause.getVocabulary() |
Modifier and Type | Method and Description |
---|---|
static OriginalWLClause |
OriginalWLClause.brandNewClause(UnitPropagationListener s,
ILits voc,
IVecInt literals)
Creates a brand new clause, presumably from external data.
|
static OriginalHTClause |
OriginalHTClause.brandNewClause(UnitPropagationListener s,
ILits voc,
IVecInt literals)
Creates a brand new clause, presumably from external data.
|
static OriginalBinaryClause |
OriginalBinaryClause.brandNewClause(UnitPropagationListener s,
ILits voc,
IVecInt literals)
Creates a brand new clause, presumably from external data.
|
static IVecInt |
Clauses.sanityCheck(IVecInt ps,
ILits voc,
UnitPropagationListener s)
Perform some sanity check before constructing a clause a) if a literal is
assigned true, return null (the clause is satisfied) b) if a literal is
assigned false, remove it c) if a clause contains a literal and its
opposite (tautology) return null d) remove duplicate literals e) if the
clause is empty, return null f) if the clause if unit, transmit it to the
object responsible for unit propagation
|
Constructor and Description |
---|
BinaryClause(IVecInt ps,
ILits voc)
Creates a new basic clause
|
HTClause(IVecInt ps,
ILits voc)
Creates a new basic clause
|
LearntBinaryClause(IVecInt ps,
ILits voc) |
LearntHTClause(IVecInt ps,
ILits voc) |
LearntWLClause(IVecInt ps,
ILits voc) |
OriginalBinaryClause(IVecInt ps,
ILits voc) |
OriginalHTClause(IVecInt ps,
ILits voc) |
OriginalWLClause(IVecInt ps,
ILits voc) |
WLClause(IVecInt ps,
ILits voc)
Creates a new basic clause
|
Modifier and Type | Field and Description |
---|---|
protected ILits |
Solver.voc |
Modifier and Type | Method and Description |
---|---|
ILits |
Solver.getVocabulary() |
ILits |
DataStructureFactory.getVocabulary() |
Modifier and Type | Method and Description |
---|---|
void |
IOrder.setLits(ILits lits)
Method used to provide an easy access the the solver vocabulary.
|
Modifier and Type | Field and Description |
---|---|
protected ILits |
LimitedLearning.lits |
Modifier and Type | Field and Description |
---|---|
protected ILits |
VarOrderHeap.lits |
Modifier and Type | Method and Description |
---|---|
ILits |
VarOrderHeap.getVocabulary() |
Modifier and Type | Method and Description |
---|---|
void |
VarOrderHeap.setLits(ILits lits) |
void |
RandomWalkDecorator.setLits(ILits lits) |
void |
TabuListDecorator.setLits(ILits lits) |
Modifier and Type | Method and Description |
---|---|
protected ILits |
AbstractPBDataStructureFactory.createLits() |
Modifier and Type | Method and Description |
---|---|
Constr |
MinCardConstructor.constructCard(UnitPropagationListener solver,
ILits voc,
IVecInt theLits,
int degree) |
Constr |
ICardConstructor.constructCard(UnitPropagationListener solver,
ILits voc,
IVecInt theLits,
int degree) |
Constr |
AtLeastCardPBConstructor.constructCard(UnitPropagationListener solver,
ILits voc,
IVecInt theLits,
int degree) |
Constr |
MinCardPBConstructor.constructCard(UnitPropagationListener solver,
ILits voc,
IVecInt theLits,
int degree) |
Constr |
AtLeastCardConstructor.constructCard(UnitPropagationListener solver,
ILits voc,
IVecInt theLits,
int degree) |
Constr |
UnitBinaryHTClauseConstructor.constructClause(UnitPropagationListener solver,
ILits voc,
IVecInt v) |
Constr |
UnitBinaryWLClauseConstructor.constructClause(UnitPropagationListener solver,
ILits voc,
IVecInt v) |
Constr |
UnitBinaryHTClausePBConstructor.constructClause(UnitPropagationListener solver,
ILits voc,
IVecInt v) |
Constr |
IClauseConstructor.constructClause(UnitPropagationListener solver,
ILits voc,
IVecInt v) |
Constr |
MinCardConstructor.constructLearntCard(ILits voc,
IDataStructurePB dspb) |
Constr |
ICardConstructor.constructLearntCard(ILits voc,
IDataStructurePB dspb) |
Constr |
AtLeastCardPBConstructor.constructLearntCard(ILits voc,
IDataStructurePB dspb) |
Constr |
MinCardPBConstructor.constructLearntCard(ILits voc,
IDataStructurePB dspb) |
Constr |
AtLeastCardConstructor.constructLearntCard(ILits voc,
IDataStructurePB dspb) |
Constr |
UnitBinaryHTClauseConstructor.constructLearntClause(ILits voc,
IVecInt literals) |
Constr |
UnitBinaryWLClauseConstructor.constructLearntClause(ILits voc,
IVecInt literals) |
Constr |
UnitBinaryHTClausePBConstructor.constructLearntClause(ILits voc,
IVecInt literals) |
Constr |
IClauseConstructor.constructLearntClause(ILits voc,
IVecInt literals) |
Constr |
MinLongWatchPBConstructor.constructLearntPB(ILits voc,
IDataStructurePB dspb) |
Constr |
MaxLongWatchPBConstructor.constructLearntPB(ILits voc,
IDataStructurePB dspb) |
Constr |
MinWatchPBConstructor.constructLearntPB(ILits voc,
IDataStructurePB dspb) |
Constr |
MaxWatchPBConstructor.constructLearntPB(ILits voc,
IDataStructurePB dspb) |
Constr |
MinLongWatchPBCPConstructor.constructLearntPB(ILits voc,
IDataStructurePB dspb) |
Constr |
MaxLongWatchPBCPConstructor.constructLearntPB(ILits voc,
IDataStructurePB dspb) |
Constr |
IPBConstructor.constructLearntPB(ILits voc,
IDataStructurePB dspb) |
Constr |
PuebloMinWatchPBConstructor.constructLearntPB(ILits voc,
IDataStructurePB dspb) |
Constr |
MinLongWatchPBConstructor.constructPB(UnitPropagationListener solver,
ILits voc,
int[] theLits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs) |
Constr |
MaxLongWatchPBConstructor.constructPB(UnitPropagationListener solver,
ILits voc,
int[] theLits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs) |
Constr |
MinWatchPBConstructor.constructPB(UnitPropagationListener solver,
ILits voc,
int[] theLits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs) |
Constr |
MaxWatchPBConstructor.constructPB(UnitPropagationListener solver,
ILits voc,
int[] theLits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs) |
Constr |
MinLongWatchPBCPConstructor.constructPB(UnitPropagationListener solver,
ILits voc,
int[] theLits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs) |
Constr |
MaxLongWatchPBCPConstructor.constructPB(UnitPropagationListener solver,
ILits voc,
int[] theLits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs) |
Constr |
IPBConstructor.constructPB(UnitPropagationListener solver,
ILits voc,
int[] theLits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs) |
Constr |
PuebloMinWatchPBConstructor.constructPB(UnitPropagationListener solver,
ILits voc,
int[] theLits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs) |
Modifier and Type | Field and Description |
---|---|
protected ILits |
WatchPbLongCP.voc
constraint's vocabulary
|
protected ILits |
WatchPb.voc
constraint's vocabulary
|
protected ILits |
WatchPbLong.voc
constraint's vocabulary
|
Modifier and Type | Method and Description |
---|---|
ILits |
WatchPbLongCP.getVocabulary() |
ILits |
AtLeastPB.getVocabulary() |
ILits |
WatchPb.getVocabulary() |
ILits |
PBConstr.getVocabulary() |
ILits |
UnitClausesPB.getVocabulary() |
ILits |
WatchPbLong.getVocabulary() |
ILits |
UnitClausePB.getVocabulary() |
Modifier and Type | Method and Description |
---|---|
static AtLeastPB |
AtLeastPB.atLeastNew(ILits voc,
IVecInt ps,
int n) |
static PBConstr |
AtLeastPB.atLeastNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
int n) |
static OriginalBinaryClausePB |
OriginalBinaryClausePB.brandNewClause(UnitPropagationListener s,
ILits voc,
IVecInt literals)
Creates a brand new clause, presumably from external data.
|
static OriginalHTClausePB |
OriginalHTClausePB.brandNewClause(UnitPropagationListener s,
ILits voc,
IVecInt literals)
Creates a brand new clause, presumably from external data.
|
static PBConstr |
MinWatchCardPB.minWatchCardPBNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
boolean moreThan,
int degree)
Permet la cr?
|
static IDataStructurePB |
Pseudos.niceCheckedParameters(IVecInt ps,
IVec<BigInteger> bigCoefs,
boolean moreThan,
BigInteger bigDeg,
ILits voc) |
static IDataStructurePB |
Pseudos.niceParameters(IVecInt ps,
IVec<BigInteger> bigCoefs,
boolean moreThan,
BigInteger bigDeg,
ILits voc) |
static MaxWatchPb |
MaxWatchPb.normalizedMaxWatchPbNew(UnitPropagationListener s,
ILits voc,
int[] lits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs)
build a pseudo boolean constraint.
|
static MaxWatchPbLongCP |
MaxWatchPbLongCP.normalizedMaxWatchPbNew(UnitPropagationListener s,
ILits voc,
int[] lits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs)
build a pseudo boolean constraint.
|
static MaxWatchPbLong |
MaxWatchPbLong.normalizedMaxWatchPbNew(UnitPropagationListener s,
ILits voc,
int[] lits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs)
build a pseudo boolean constraint.
|
static PBConstr |
MinWatchCardPB.normalizedMinWatchCardPBNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
int degree)
Permet la cr?
|
static PuebloMinWatchPb |
PuebloMinWatchPb.normalizedMinWatchPbNew(UnitPropagationListener s,
ILits voc,
int[] lits,
BigInteger[] coefs,
BigInteger degree) |
static MinWatchPbLong |
MinWatchPbLong.normalizedMinWatchPbNew(UnitPropagationListener s,
ILits voc,
int[] lits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs)
build a pseudo boolean constraint.
|
static MinWatchPb |
MinWatchPb.normalizedMinWatchPbNew(UnitPropagationListener s,
ILits voc,
int[] lits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs)
build a pseudo boolean constraint.
|
static MinWatchPbLongCP |
MinWatchPbLongCP.normalizedMinWatchPbNew(UnitPropagationListener s,
ILits voc,
int[] lits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs)
build a pseudo boolean constraint.
|
static WatchPb |
MaxWatchPb.normalizedWatchPbNew(ILits voc,
IDataStructurePB mpb)
build a pseudo boolean constraint from a specific data structure.
|
static WatchPbLong |
MinWatchPbLong.normalizedWatchPbNew(ILits voc,
IDataStructurePB mpb)
build a pseudo boolean constraint from a specific data structure.
|
static WatchPbLongCP |
MaxWatchPbLongCP.normalizedWatchPbNew(ILits voc,
IDataStructurePB mpb)
build a pseudo boolean constraint from a specific data structure.
|
static WatchPb |
MinWatchPb.normalizedWatchPbNew(ILits voc,
IDataStructurePB mpb)
build a pseudo boolean constraint from a specific data structure.
|
static WatchPbLongCP |
MinWatchPbLongCP.normalizedWatchPbNew(ILits voc,
IDataStructurePB mpb)
build a pseudo boolean constraint from a specific data structure.
|
static WatchPb |
PuebloMinWatchPb.normalizedWatchPbNew(ILits voc,
IDataStructurePB mpb) |
static WatchPbLong |
MaxWatchPbLong.normalizedWatchPbNew(ILits voc,
IDataStructurePB mpb)
build a pseudo boolean constraint from a specific data structure.
|
Constructor and Description |
---|
LearntBinaryClausePB(IVecInt ps,
ILits voc) |
LearntHTClausePB(IVecInt ps,
ILits voc) |
MinWatchCardPB(ILits voc,
IVecInt ps,
boolean moreThan,
int degree) |
MinWatchCardPB(ILits voc,
IVecInt ps,
int degree) |
MinWatchPb(ILits voc,
IDataStructurePB mpb)
Basic constructor for pb constraint a0.x0 + a1.x1 + ... + an.xn >= k
This constructor is called for learnt pseudo boolean constraints.
|
MinWatchPb(ILits voc,
int[] lits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs)
Basic constructor for PB constraint a0.x0 + a1.x1 + ... + an.xn >= k
|
MinWatchPbLong(ILits voc,
IDataStructurePB mpb)
Basic constructor for pb constraint a0.x0 + a1.x1 + ... + an.xn >= k
This constructor is called for learnt pseudo boolean constraints.
|
MinWatchPbLong(ILits voc,
int[] lits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs)
Basic constructor for PB constraint a0.x0 + a1.x1 + ... + an.xn >= k
|
MinWatchPbLongCP(ILits voc,
IDataStructurePB mpb)
Basic constructor for pb constraint a0.x0 + a1.x1 + ... + an.xn >= k
This constructor is called for learnt pseudo boolean constraints.
|
MinWatchPbLongCP(ILits voc,
int[] lits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs)
Basic constructor for PB constraint a0.x0 + a1.x1 + ... + an.xn >= k
|
OriginalBinaryClausePB(IVecInt ps,
ILits voc) |
OriginalHTClausePB(IVecInt ps,
ILits voc) |
UnitClausePB(int value,
ILits voc) |
Copyright © 2013 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.