A B C D E F G H I J L M N O P R S T U V W X

L

Lanceur - Class in org.sat4j
This class is used to launch the SAT solvers from the command line.
Lanceur() - Constructor for class org.sat4j.Lanceur
 
LanceurPseudo2005 - Class in org.sat4j
Launcher especially dedicated to the pseudo boolean 05 evaluation (@link http://www.cril.univ-artois.fr/PB05/).
LanceurPseudo2005() - Constructor for class org.sat4j.LanceurPseudo2005
 
LanceurPseudo2007 - Class in org.sat4j
 
LanceurPseudo2007() - Constructor for class org.sat4j.LanceurPseudo2007
 
last() - Method in class org.sat4j.core.Vec
return the latest element on the stack.
last() - Method in class org.sat4j.core.VecInt
 
last() - Method in interface org.sat4j.specs.IVec
return the latest element on the stack.
last() - Method in interface org.sat4j.specs.IVecInt
 
Lbool - Enum in org.sat4j.minisat.core
That enumeration defines the possible truth value for a variable: satisfied, falsified or unknown/undefined.
learn(Constr) - Method in class org.sat4j.minisat.core.DotSearchListener
 
learn(Constr) - Method in interface org.sat4j.minisat.core.Learner
 
learn(Constr) - Method in interface org.sat4j.minisat.core.SearchListener
learning a new clause
learn(Constr) - Method in class org.sat4j.minisat.core.Solver
 
learn(Constr) - Method in class org.sat4j.minisat.core.TextOutputListener
 
learnConstraint(Constr) - Method in class org.sat4j.minisat.constraints.AbstractDataStructureFactory
 
learnConstraint(Constr) - Method in class org.sat4j.minisat.constraints.MixedDataStructureWithBinary
 
learnConstraint(Constr) - Method in class org.sat4j.minisat.constraints.MixedDataStructureWithBinaryAndTernary
 
learnConstraint(Constr) - Method in interface org.sat4j.minisat.core.DataStructureFactory
 
learnedbinaryclauses - Variable in class org.sat4j.minisat.core.SolverStats
 
learnedclauses - Variable in class org.sat4j.minisat.core.SolverStats
 
learnedliterals - Variable in class org.sat4j.minisat.core.SolverStats
 
learnedternaryclauses - Variable in class org.sat4j.minisat.core.SolverStats
 
Learner - Interface in org.sat4j.minisat.core
Provide the learning service.
LearningStrategy<L extends ILits> - Interface in org.sat4j.minisat.core
Implementation of the strategy design pattern for allowing various learning schemes.
learns(Constr) - Method in interface org.sat4j.minisat.core.LearningStrategy
 
learns(Constr) - Method in class org.sat4j.minisat.learning.LimitedLearning
 
learns(Constr) - Method in class org.sat4j.minisat.learning.MiniSATLearning
 
learns(Constr) - Method in class org.sat4j.minisat.learning.NoLearningButHeuristics
 
learns(Constr) - Method in class org.sat4j.minisat.learning.NoLearningNoHeuristics
 
learnt() - Method in class org.sat4j.minisat.constraints.card.AtLeast
 
learnt() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
D?
learnt() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
Returns wether the constraint is learnt or not.
learnt() - Method in class org.sat4j.minisat.constraints.cnf.BinaryClauses
 
learnt() - Method in class org.sat4j.minisat.constraints.cnf.CBClause
 
learnt() - Method in class org.sat4j.minisat.constraints.cnf.DefaultWLClause
 
learnt() - Method in class org.sat4j.minisat.constraints.cnf.LearntWLClause
 
learnt() - Method in class org.sat4j.minisat.constraints.cnf.OriginalWLClause
 
learnt() - Method in class org.sat4j.minisat.constraints.cnf.TernaryClauses
 
learnt() - Method in class org.sat4j.minisat.constraints.pb.AtLeastPB
D?
learnt() - Method in class org.sat4j.minisat.constraints.pb.MinWatchCardPB
D?
learnt() - Method in class org.sat4j.minisat.constraints.pb.WatchPb
is the constraint a learnt constrainte ?
learnt() - Method in interface org.sat4j.specs.IConstr
 
LearntWLClause - Class in org.sat4j.minisat.constraints.cnf
 
LearntWLClause(IVecInt, ILits) - Constructor for class org.sat4j.minisat.constraints.cnf.LearntWLClause
 
LecteurDimacs - Class in org.sat4j.reader
Dimacs Reader written by Frederic Laihem.
LecteurDimacs(ISolver) - Constructor for class org.sat4j.reader.LecteurDimacs
 
lightSolver() - Method in class org.sat4j.core.ASolverFactory
To obtain a solver that is suitable for solving many small instances of SAT problems.
lightSolver() - Method in class org.sat4j.minisat.SolverFactory
 
LimitedLearning<L extends ILits> - Class in org.sat4j.minisat.learning
Learn only clauses which size is smaller than a percentage of the number of variables.
LimitedLearning() - Constructor for class org.sat4j.minisat.learning.LimitedLearning
 
LiteralsUtils - Class in org.sat4j.minisat.core
Utility methods to avoid using bit manipulation inside code.
Lits - Class in org.sat4j.minisat.constraints.cnf
 
Lits() - Constructor for class org.sat4j.minisat.constraints.cnf.Lits
 
Lits2 - Class in org.sat4j.minisat.constraints.cnf
 
Lits2() - Constructor for class org.sat4j.minisat.constraints.cnf.Lits2
 
Lits23 - Class in org.sat4j.minisat.constraints.cnf
 
Lits23() - Constructor for class org.sat4j.minisat.constraints.cnf.Lits23
 
locked() - Method in class org.sat4j.minisat.constraints.card.AtLeast
 
locked() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
La contrainte est la cause d'une propagation unitaire
locked() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
Returns if the constraint is the reason for a unit propagation.
locked() - Method in class org.sat4j.minisat.constraints.cnf.BinaryClauses
 
locked() - Method in class org.sat4j.minisat.constraints.cnf.CBClause
 
locked() - Method in class org.sat4j.minisat.constraints.cnf.TernaryClauses
 
locked() - Method in class org.sat4j.minisat.constraints.cnf.WLClause
 
locked() - Method in class org.sat4j.minisat.constraints.pb.WatchPb
The constraint is the reason of a unit propagation.
locked() - Method in interface org.sat4j.minisat.core.Constr
Indicate wether a constraint is responsible from an assignment.
LubyRestarts - Class in org.sat4j.minisat.restarts
Luby series code taken from SATZ_rand 5.0 from Henry Kautz http://www.cs.rochester.edu/u/kautz/satz-rand/satz-rand-v5.0.tgz Luby's series long luby_super(int i) { long power; int k; if (i<=0){ fprintf(stderr, "bad argument super(%d)\n", i); exit(1); } /* let 2ˆk be the least power of 2 >= (i+1) k = 1; power = 2; while (power < (i+1)){ k += 1; power *= 2; } if (power == (i+1)) return (power/2); return (luby_super(i - (power/2) + 1)); }
LubyRestarts() - Constructor for class org.sat4j.minisat.restarts.LubyRestarts
 

A B C D E F G H I J L M N O P R S T U V W X