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

Packages that use Constr
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.core Implementation of the MiniSAT solver skeleton. 
org.sat4j.minisat.learning Various learning strategies. 
 

Uses of Constr in org.sat4j.minisat.constraints
 

Methods in org.sat4j.minisat.constraints that return Constr
 Constr AbstractDataStructureFactory.createCardinalityConstraint(IVecInt literals, int degree)
           
 Constr CardinalityDataStructureYanMin.createCardinalityConstraint(IVecInt literals, int degree)
           
 Constr MixedDataStructureDanielHT.createCardinalityConstraint(IVecInt literals, int degree)
           
 Constr CardinalityDataStructure.createCardinalityConstraint(IVecInt literals, int degree)
           
 Constr MixedDataStructureDanielWL.createCardinalityConstraint(IVecInt literals, int degree)
           
 Constr CardinalityDataStructureYanMax.createCardinalityConstraint(IVecInt literals, int degree)
           
 Constr ClausalDataStructureCB.createClause(IVecInt literals)
           
 Constr CardinalityDataStructureYanMin.createClause(IVecInt literals)
           
 Constr ClausalDataStructureCBWL.createClause(IVecInt literals)
           
 Constr ClausalDataStructureWL.createClause(IVecInt literals)
           
 Constr MixedDataStructureDanielHT.createClause(IVecInt literals)
           
 Constr CardinalityDataStructure.createClause(IVecInt literals)
           
 Constr MixedDataStructureDanielCBWL.createClause(IVecInt literals)
           
 Constr MixedDataStructureDanielWL.createClause(IVecInt literals)
           
 Constr CardinalityDataStructureYanMax.createClause(IVecInt literals)
           
 Constr ClausalDataStructureCB.createUnregisteredClause(IVecInt literals)
           
 Constr CardinalityDataStructureYanMin.createUnregisteredClause(IVecInt literals)
           
 Constr ClausalDataStructureCBWL.createUnregisteredClause(IVecInt literals)
           
 Constr ClausalDataStructureWL.createUnregisteredClause(IVecInt literals)
           
 Constr MixedDataStructureDanielHT.createUnregisteredClause(IVecInt literals)
           
 Constr CardinalityDataStructure.createUnregisteredClause(IVecInt literals)
           
 Constr MixedDataStructureDanielWL.createUnregisteredClause(IVecInt literals)
           
 Constr CardinalityDataStructureYanMax.createUnregisteredClause(IVecInt literals)
           
 

Methods in org.sat4j.minisat.constraints with parameters of type Constr
 void AbstractDataStructureFactory.learnConstraint(Constr constr)
           
 

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

Classes in org.sat4j.minisat.constraints.card that implement Constr
 class AtLeast
           
 class MaxWatchCard
           
 class MinWatchCard
           
 

Methods in org.sat4j.minisat.constraints.card that return Constr
static Constr AtLeast.atLeastNew(UnitPropagationListener s, ILits voc, IVecInt ps, int n)
           
 

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

Classes in org.sat4j.minisat.constraints.cnf that implement Constr
 class BinaryClause
          Data structure for binary clause.
 class CBClause
           
 class HTClause
          Lazy data structure for clause using the Head Tail data structure from SATO, The original scheme is improved by avoiding moving pointers to literals but moving the literals themselves.
 class LearntBinaryClause
           
 class LearntHTClause
           
 class LearntWLClause
           
 class MixableCBClause
          Counter Based clauses that can be mixed with WLCLauses
 class OriginalBinaryClause
           
 class OriginalHTClause
           
 class OriginalWLClause
           
 class UnitClause
           
 class UnitClauses
           
 class WLClause
          Lazy data structure for clause using Watched Literals.
 

Methods in org.sat4j.minisat.constraints.cnf that return Constr
 Constr Lits.getReason(int lit)
           
 

Methods in org.sat4j.minisat.constraints.cnf with parameters of type Constr
 void Lits.setReason(int lit, Constr r)
           
 

Uses of Constr in org.sat4j.minisat.core
 

Fields in org.sat4j.minisat.core declared as Constr
 Constr Pair.reason
           
 

Methods in org.sat4j.minisat.core that return Constr
 Constr DataStructureFactory.createCardinalityConstraint(IVecInt literals, int degree)
           
 Constr DataStructureFactory.createClause(IVecInt literals)
           
 Constr DataStructureFactory.createUnregisteredClause(IVecInt literals)
           
 Constr ILits.getReason(int lit)
           
 Constr Solver.propagate()
           
 

Methods in org.sat4j.minisat.core with parameters of type Constr
protected  IConstr Solver.addConstr(Constr constr)
           
 void Solver.analyze(Constr confl, Pair results)
           
protected  void Solver.analyzeAtRootLevel(Constr conflict)
           
 void Solver.claBumpActivity(Constr confl)
          Propagate activity to a constraint
 boolean UnitPropagationListener.enqueue(int p, Constr from)
          satisfies a literal
 boolean Solver.enqueue(int p, Constr from)
          Put the literal on the queue of assignments to be done.
 void Learner.learn(Constr c)
           
 void Solver.learn(Constr c)
           
 void DataStructureFactory.learnConstraint(Constr constr)
           
 void LearningStrategy.learns(Constr constr)
           
 void ILits.setReason(int lit, Constr r)
           
 

Uses of Constr in org.sat4j.minisat.learning
 

Methods in org.sat4j.minisat.learning with parameters of type Constr
protected abstract  boolean LimitedLearning.learningCondition(Constr constr)
           
protected  boolean ActiveLearning.learningCondition(Constr clause)
           
protected  boolean FixedLengthLearning.learningCondition(Constr constr)
           
protected  boolean ClauseOnlyLearning.learningCondition(Constr constr)
           
protected  boolean PercentLengthLearning.learningCondition(Constr constr)
           
 void LimitedLearning.learns(Constr constr)
           
 void NoLearningButHeuristics.learns(Constr reason)
           
 void MiniSATLearning.learns(Constr constr)
           
 void NoLearningNoHeuristics.learns(Constr reason)
           
 



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