Uses of Interface org.sat4j.minisat.core.ILits (sat4j 1.7 API)

Overview

Package

Class

Use

Tree

Deprecated

Index

Help

PREV NEXT

FRAMES NO FRAMES

Uses of Interface
org.sat4j.minisat.core.ILits

Packages that use ILits
org.sat4j.minisat	Implementation of the MiniSAT specification in Java.
org.sat4j.minisat.constraints	Implementations of various constraints for MiniSAT.
org.sat4j.minisat.constraints.card	Implementations of cardinality contraints.
org.sat4j.minisat.constraints.cnf	Implementations of clausal contraints.
org.sat4j.minisat.constraints.pb	Implementations of pseudo boolean contraints.
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.

Uses of ILits in org.sat4j.minisat

Methods in org.sat4j.minisat with type parameters of type ILits

static



<L extends ILits> 


Solver<L>

SolverFactory.newMiniLearning(DataStructureFactory<L> dsf)

static



<L extends ILits> 


Solver<L>

SolverFactory.newMiniLearning(DataStructureFactory<L> dsf,
                int n)

static



<L extends ILits> 


Solver<L>

SolverFactory.newMiniLearning(DataStructureFactory<L> dsf,
                IOrder<L> order)

static



<L extends ILits> 


Solver<L>

SolverFactory.newMiniLearningEZSimp(DataStructureFactory<L> dsf)

static



<L extends ILits> 


Solver<L>

SolverFactory.newMiniLearningHeap(DataStructureFactory<L> dsf)

static



<L extends ILits> 


Solver<L>

SolverFactory.newMiniSAT(DataStructureFactory<L> dsf)

static



<L extends ILits> 


Solver<L>

SolverFactory.newMiniSATHeap(DataStructureFactory<L> dsf)

Methods in org.sat4j.minisat that return types with arguments of type ILits
`static Solver<ILits>`	`SolverFactory.newActiveLearning()`
`static Solver<ILits>`	`SolverFactory.newBackjumping()`
`static Solver<ILits>`	`SolverFactory.newMiniCard()`
`static Solver<ILits>`	`SolverFactory.newMiniLearning()`
`static Solver<ILits>`	`SolverFactory.newMiniLearning(int n)`
`static Solver<ILits>`	`SolverFactory.newMiniLearningCB()`
`static Solver<ILits>`	`SolverFactory.newMiniLearningCBWL()`
`static Solver<ILits>`	`SolverFactory.newMiniLearningCBWLPure()`
`static Solver<ILits>`	`SolverFactory.newMiniLearningEZSimp()`
`static Solver<ILits>`	`SolverFactory.newMiniLearningHeap()`
`static Solver<ILits>`	`SolverFactory.newMiniLearningHeapExpSimp()`
`static Solver<ILits>`	`SolverFactory.newMiniLearningHeapEZSimp()`
`static Solver<ILits>`	`SolverFactory.newMiniLearningHeapEZSimpLongRestarts()`
`static Solver<ILits>`	`SolverFactory.newMiniLearningHeapEZSimpNoRestarts()`
`static Solver<ILits>`	`SolverFactory.newMiniLearningHeapRsatExpSimp()`
`static Solver<ILits>`	`SolverFactory.newMiniLearningHeapRsatExpSimpBiere()`
`static Solver<ILits>`	`SolverFactory.newMiniLearningHeapRsatExpSimpLuby()`
`static Solver<ILits>`	`SolverFactory.newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncremental()`
`static Solver<ILits>`	`SolverFactory.newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalLearnJustClauses()`
`static Solver<ILits>`	`SolverFactory.newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalMerging()`
`static Solver<ILits>`	`SolverFactory.newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalNoLearning()`
`static Solver<ILits>`	`SolverFactory.newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalReductionToClause()`
`static Solver<ILits>`	`SolverFactory.newMiniLearningPure()`
`static Solver<ILits>`	`SolverFactory.newMinimalOPBClauseCardConstrMaxSpecificOrder()`
`static Solver<ILits>`	`SolverFactory.newMinimalOPBMax()`
`static Solver<ILits>`	`SolverFactory.newMinimalOPBMin()`
`static Solver<ILits>`	`SolverFactory.newMinimalOPBMinPueblo()`
`static Solver<ILits>`	`SolverFactory.newMiniMaxSAT()` Builds a SAT solver for the MAX sat evaluation.
`static Solver<ILits>`	`SolverFactory.newMiniOPBClauseAtLeastConstrMax()`
`static Solver<ILits>`	`SolverFactory.newMiniOPBClauseAtLeastMinPueblo()`
`static Solver<ILits>`	`SolverFactory.newMiniOPBClauseCardConstrMax()`
`static Solver<ILits>`	`SolverFactory.newMiniOPBClauseCardConstrMaxImplied()`
`static Solver<ILits>`	`SolverFactory.newMiniOPBClauseCardConstrMaxReduceToClause()`
`static Solver<ILits>`	`SolverFactory.newMiniOPBClauseCardConstrMaxSpecificOrder()`
`static Solver<ILits>`	`SolverFactory.newMiniOPBClauseCardMin()`
`static Solver<ILits>`	`SolverFactory.newMiniOPBClauseCardMinPueblo()`
`static Solver<ILits>`	`SolverFactory.newMiniOPBCounterBasedClauseCardConstrMax()`
`static Solver<ILits>`	`SolverFactory.newMiniOPBMax()`
`static Solver<ILits>`	`SolverFactory.newMiniOPBMin()`
`static Solver<ILits>`	`SolverFactory.newMiniOPBMinPueblo()`
`static Solver<ILits>`	`SolverFactory.newMiniSAT()`
`static Solver<ILits>`	`SolverFactory.newMiniSATHeap()`
`static Solver<ILits>`	`SolverFactory.newMiniSATHeapExpSimp()`
`static Solver<ILits>`	`SolverFactory.newMiniSATHeapEZSimp()`
`static Solver<ILits>`	`SolverFactory.newMiniSATNoRestarts()`
`static Solver<ILits>`	`SolverFactory.newRelsat()`

Uses of ILits in org.sat4j.minisat.constraints

Classes in org.sat4j.minisat.constraints with type parameters of type ILits
`class`	`AbstractDataStructureFactory<L extends ILits>`

Fields in org.sat4j.minisat.constraints declared as ILits
`protected L`	`AbstractDataStructureFactory.lits`

Methods in org.sat4j.minisat.constraints that return ILits
`protected ILits`	`AbstractPBDataStructureFactory.createLits()`
`protected ILits`	`ClausalDataStructureWL.createLits()`
`protected ILits`	`ClausalDataStructureCBWL.createLits()`
`protected ILits`	`ClausalDataStructureCB.createLits()`
`protected ILits`	`AbstractCardinalityDataStructure.createLits()`
`protected ILits`	`MixedDataStructureDaniel.createLits()`

Uses of ILits in org.sat4j.minisat.constraints.card

Fields in org.sat4j.minisat.constraints.card declared as ILits
`protected ILits`	`AtLeast.voc`

Methods in org.sat4j.minisat.constraints.card that return ILits
`ILits`	`MaxWatchCard.getVocabulary()`
`ILits`	`MinWatchCard.getVocabulary()`

Methods in org.sat4j.minisat.constraints.card with parameters of type ILits
`static AtLeast`	`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 MaxWatchCard`	`MaxWatchCard.maxWatchCardNew(UnitPropagationListener s, ILits voc, IVecInt ps, boolean moreThan, int degree)` Permet la cr?
`static MinWatchCard`	`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)`

Constructors in org.sat4j.minisat.constraints.card with parameters of type ILits
`AtLeast(ILits voc, IVecInt ps, int degree)`
`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.

Uses of ILits in org.sat4j.minisat.constraints.cnf

Classes in org.sat4j.minisat.constraints.cnf that implement ILits
`class`	`Lits`
`class`	`Lits2`
`class`	`Lits23`
`class`	`MarkableLits`

Fields in org.sat4j.minisat.constraints.cnf declared as ILits
`protected ILits`	`WLClause.voc`
`protected ILits`	`CBClause.voc`

Methods in org.sat4j.minisat.constraints.cnf that return ILits
`ILits`	`WLClause.getVocabulary()`

Methods in org.sat4j.minisat.constraints.cnf with parameters of type ILits
`static CBClause`	`MixableCBClause.brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals)`
`static OriginalWLClause`	`OriginalWLClause.brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals)` Creates a brand new clause, presumably from external data.
`static WLClause`	`WLClause.brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals)` Creates a brand new clause, presumably from external data.
`static CBClause`	`CBClause.brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals)`
`static IVecInt`	`WLClause.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

Constructors in org.sat4j.minisat.constraints.cnf with parameters of type ILits
`BinaryClauses(ILits voc, int p)`
`CBClause(IVecInt ps, ILits voc)`
`CBClause(IVecInt ps, ILits voc, boolean learnt)`
`DefaultWLClause(IVecInt ps, ILits voc)`
`LearntWLClause(IVecInt ps, ILits voc)`
`MixableCBClause(IVecInt ps, ILits voc)`
`MixableCBClause(IVecInt ps, ILits voc, boolean learnt)`
`OriginalWLClause(IVecInt ps, ILits voc)`
`TernaryClauses(ILits voc, int p)`
`WLClause(IVecInt ps, ILits voc)` Creates a new basic clause

Uses of ILits in org.sat4j.minisat.constraints.pb

Classes in org.sat4j.minisat.constraints.pb with type parameters of type ILits
`class`	`PBSolver<L extends ILits>`

Fields in org.sat4j.minisat.constraints.pb declared as ILits
`protected ILits`	`WatchPb.voc` constraint's vocabulary

Methods in org.sat4j.minisat.constraints.pb that return ILits
`ILits`	`MixableCBClausePB.getVocabulary()`
`ILits`	`AtLeastPB.getVocabulary()`
`ILits`	`WatchPb.getVocabulary()`
`ILits`	`PBConstr.getVocabulary()`

Methods in org.sat4j.minisat.constraints.pb with parameters of type ILits
`static AtLeastPB`	`AtLeastPB.atLeastNew(ILits voc, IVecInt ps, int n)`
`static AtLeastPB`	`AtLeastPB.atLeastNew(UnitPropagationListener s, ILits voc, IVecInt ps, int n)`
`static MixableCBClausePB`	`MixableCBClausePB.brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals)`
`static WLClausePB`	`WLClausePB.brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals)` Creates a brand new clause, presumably from external data.
`static MaxWatchPb`	`MaxWatchPb.maxWatchPbNew(UnitPropagationListener s, ILits voc, IVecInt ps, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)`
`static MaxWatchPb`	`MaxWatchPb.maxWatchPbNew(UnitPropagationListener s, ILits voc, IVecInt ps, IVecInt coefs, boolean moreThan, int degree)`
`static MinWatchCardPB`	`MinWatchCardPB.minWatchCardPBNew(UnitPropagationListener s, ILits voc, IVecInt ps, boolean moreThan, int degree)` Permet la cr?
`static PuebloMinWatchPb`	`PuebloMinWatchPb.minWatchPbNew(UnitPropagationListener s, ILits voc, IDataStructurePB mpb)`
`static PuebloMinWatchPb`	`PuebloMinWatchPb.minWatchPbNew(UnitPropagationListener s, ILits voc, IVecInt ps, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)`
`static MinWatchPb`	`MinWatchPb.minWatchPbNew(UnitPropagationListener s, ILits voc, IVecInt ps, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)`
`static PuebloMinWatchPb`	`PuebloMinWatchPb.minWatchPbNew(UnitPropagationListener s, ILits voc, IVecInt ps, IVecInt coefs, boolean moreThan, int degree)`
`static MinWatchPb`	`MinWatchPb.minWatchPbNew(UnitPropagationListener s, ILits voc, IVecInt ps, IVecInt coefs, boolean moreThan, int degree)`
`static IDataStructurePB`	`WatchPb.niceCheckedParameters(IVecInt ps, IVec<java.math.BigInteger> bigCoefs, boolean moreThan, java.math.BigInteger bigDeg, ILits voc)`
`static IDataStructurePB`	`WatchPb.niceParameters(IVecInt ps, IVec<java.math.BigInteger> bigCoefs, boolean moreThan, java.math.BigInteger bigDeg, ILits voc)`
`static MaxWatchPb`	`MaxWatchPb.normalizedMaxWatchPbNew(UnitPropagationListener s, ILits voc, IDataStructurePB mpb)`
`static MaxWatchPb`	`MaxWatchPb.normalizedMaxWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, java.math.BigInteger[] coefs, java.math.BigInteger degree)`
`static MinWatchCardPB`	`MinWatchCardPB.normalizedMinWatchCardPBNew(UnitPropagationListener s, ILits voc, IVecInt ps, int degree)` Permet la cr?
`static MinWatchPb`	`MinWatchPb.normalizedMinWatchPbNew(UnitPropagationListener s, ILits voc, IDataStructurePB mpb)`
`static MinWatchPb`	`MinWatchPb.normalizedMinWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, java.math.BigInteger[] coefs, java.math.BigInteger degree)`
`static WatchPb`	`PuebloMinWatchPb.normalizedWatchPbNew(ILits voc, IDataStructurePB mpb)`
`static WatchPb`	`MinWatchPb.normalizedWatchPbNew(ILits voc, IDataStructurePB mpb)`
`static WatchPb`	`MaxWatchPb.watchPbNew(ILits voc, IVecInt lits, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)`
`static WatchPb`	`PuebloMinWatchPb.watchPbNew(ILits voc, IVecInt lits, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)`
`static WatchPb`	`MinWatchPb.watchPbNew(ILits voc, IVecInt lits, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)`
`static WatchPb`	`MaxWatchPb.watchPbNew(ILits voc, IVecInt lits, IVecInt coefs, boolean moreThan, int degree)`
`static WatchPb`	`PuebloMinWatchPb.watchPbNew(ILits voc, IVecInt lits, IVecInt coefs, boolean moreThan, int degree)`
`static WatchPb`	`MinWatchPb.watchPbNew(ILits voc, IVecInt lits, IVecInt coefs, boolean moreThan, int degree)`

Constructors in org.sat4j.minisat.constraints.pb with parameters of type ILits
`ConflictMapCardinality(java.util.Map<java.lang.Integer,java.math.BigInteger> m, java.math.BigInteger d, ILits voc, int level)`
`ConflictMapClause(java.util.Map<java.lang.Integer,java.math.BigInteger> m, java.math.BigInteger d, ILits voc, int level)`
`ConflictMapMerging(java.util.Map<java.lang.Integer,java.math.BigInteger> m, java.math.BigInteger d, ILits voc, int level)`
`MinWatchCardPB(ILits voc, IVecInt ps, boolean moreThan, int degree)`
`MinWatchCardPB(ILits voc, IVecInt ps, int degree)`
`MinWatchPb(ILits voc, IDataStructurePB mpb)` Constructeur de base des contraintes
`MinWatchPb(ILits voc, int[] lits, java.math.BigInteger[] coefs, java.math.BigInteger degree)`
`MixableCBClausePB(IVecInt ps, ILits voc)`
`MixableCBClausePB(IVecInt ps, ILits voc, boolean learnt)`
`WLClausePB(IVecInt ps, ILits voc)`

Constructor parameters in org.sat4j.minisat.constraints.pb with type arguments of type ILits
`PBSolverClause(AssertingClauseGenerator acg, LearningStrategy<ILits> learner, DataStructureFactory<ILits> dsf, IOrder<ILits> order)`
`PBSolverClause(AssertingClauseGenerator acg, LearningStrategy<ILits> learner, DataStructureFactory<ILits> dsf, IOrder<ILits> order)`
`PBSolverClause(AssertingClauseGenerator acg, LearningStrategy<ILits> learner, DataStructureFactory<ILits> dsf, IOrder<ILits> order)`
`PBSolverMerging(AssertingClauseGenerator acg, LearningStrategy<ILits> learner, DataStructureFactory<ILits> dsf, IOrder<ILits> order)`
`PBSolverMerging(AssertingClauseGenerator acg, LearningStrategy<ILits> learner, DataStructureFactory<ILits> dsf, IOrder<ILits> order)`
`PBSolverMerging(AssertingClauseGenerator acg, LearningStrategy<ILits> learner, DataStructureFactory<ILits> dsf, IOrder<ILits> order)`
`PBSolverWithImpliedClause(AssertingClauseGenerator acg, LearningStrategy<ILits> learner, DataStructureFactory<ILits> dsf, IOrder<ILits> order)`
`PBSolverWithImpliedClause(AssertingClauseGenerator acg, LearningStrategy<ILits> learner, DataStructureFactory<ILits> dsf, IOrder<ILits> order)`
`PBSolverWithImpliedClause(AssertingClauseGenerator acg, LearningStrategy<ILits> learner, DataStructureFactory<ILits> dsf, IOrder<ILits> order)`

Uses of ILits in org.sat4j.minisat.core

Classes in org.sat4j.minisat.core with type parameters of type ILits
`interface`	`DataStructureFactory<L extends ILits>` The aim of the factory is to provide a concrete implementation of clauses, cardinality constraints and pseudo boolean consraints.
`interface`	`IOrder<L extends ILits>` Interface for the variable ordering heuristics.
`interface`	`LearningStrategy<L extends ILits>` Implementation of the strategy design pattern for allowing various learning schemes.
`class`	`Solver<L extends ILits>` The backbone of the library providing the modular implementation of a MiniSAT (Chaff) like solver.

Subinterfaces of ILits in org.sat4j.minisat.core
`interface`	`ILits2` Specific vocabulary taking special care of binary clauses.
`interface`	`ILits23` Specific vocabulary taking special care of binary and ternary clauses.
`interface`	`IMarkableLits` Vocabulary in which literals can be marked.

Fields in org.sat4j.minisat.core declared as ILits
`protected L`	`Solver.voc`

Uses of ILits in org.sat4j.minisat.learning

Classes in org.sat4j.minisat.learning with type parameters of type ILits
`class`	`ActiveLearning<L extends ILits>` Learn clauses with a great number of active variables.
`class`	`ClauseOnlyLearning<L extends ILits>`
`class`	`FixedLengthLearning<L extends ILits>` A learning scheme for learning constraints of size smaller than a given constant.
`class`	`LimitedLearning<L extends ILits>` Learn only clauses which size is smaller than a percentage of the number of variables.
`class`	`MiniSATLearning<L extends ILits>` MiniSAT learning scheme.
`class`	`NoLearningButHeuristics<L extends ILits>` Allows MiniSAT to do backjumping without learning.
`class`	`NoLearningNoHeuristics<L extends ILits>` Allows MiniSAT to do backjumping without learning.
`class`	`PercentLengthLearning<L extends ILits>`

Fields in org.sat4j.minisat.learning declared as ILits
`protected L`	`LimitedLearning.lits`

Uses of ILits in org.sat4j.minisat.orders

Classes in org.sat4j.minisat.orders with type parameters of type ILits
`class`	`VarOrder<L extends ILits>`
`class`	`VarOrderHeap<L extends ILits>`

Fields in org.sat4j.minisat.orders declared as ILits
`protected L`	`VarOrder.lits`
`protected L`	`VarOrderHeap.lits`

Methods in org.sat4j.minisat.orders that return ILits
`ILits`	`VarOrder.getVocabulary()`
`ILits`	`VarOrderHeap.getVocabulary()`