Uses of Package
org.sat4j.minisat.core

Packages that use org.sat4j.minisat.core
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. 
org.sat4j.minisat.uip Various ways to compute an asserting clause (containing one Unique Implication Point). 
 

Classes in org.sat4j.minisat.core used by org.sat4j.minisat
DataStructureFactory
           
IOrder
           
 

Classes in org.sat4j.minisat.core used by org.sat4j.minisat.constraints
Constr
           
DataStructureFactory
           
ILits
           
Learner
           
Propagatable
          This interface is to be implemented by the classes wanted to be notified of the falsification of a literal.
UnitPropagationListener
           
 

Classes in org.sat4j.minisat.core used by org.sat4j.minisat.constraints.card
Constr
           
ILits
           
Propagatable
          This interface is to be implemented by the classes wanted to be notified of the falsification of a literal.
Undoable
           
UnitPropagationListener
           
 

Classes in org.sat4j.minisat.core used by org.sat4j.minisat.constraints.cnf
Constr
           
ILits
           
ILits2
           
ILits23
           
IMarkableLits
           
Lbool
           
Propagatable
          This interface is to be implemented by the classes wanted to be notified of the falsification of a literal.
Undoable
           
UnitPropagationListener
           
 

Classes in org.sat4j.minisat.core used by org.sat4j.minisat.constraints.pb
AssertingClauseGenerator
          An assertingClauseGenerator is responsible for the creation of an asserting clause during conflict analysis.
Constr
           
DataStructureFactory
           
Handle
          This class simply holds a reference to a object.
ILits
           
IOrder
           
Learner
           
LearningStrategy
           
Propagatable
          This interface is to be implemented by the classes wanted to be notified of the falsification of a literal.
Solver
           
Undoable
           
UnitPropagationListener
           
 

Classes in org.sat4j.minisat.core used by org.sat4j.minisat.core
AssertingClauseGenerator
          An assertingClauseGenerator is responsible for the creation of an asserting clause during conflict analysis.
Constr
           
DataStructureFactory
           
Handle
          This class simply holds a reference to a object.
ILits
           
ILits2
           
IOrder
           
Lbool
           
Learner
           
LearningStrategy
           
Propagatable
          This interface is to be implemented by the classes wanted to be notified of the falsification of a literal.
SearchListener
           
SearchParams
           
SolverStats
           
Undoable
           
UnitPropagationListener
           
VarActivityListener
           
 

Classes in org.sat4j.minisat.core used by org.sat4j.minisat.learning
Constr
           
DataStructureFactory
           
IOrder
           
LearningStrategy
           
Solver
           
VarActivityListener
           
 

Classes in org.sat4j.minisat.core used by org.sat4j.minisat.orders
ILits
           
IOrder
           
 

Classes in org.sat4j.minisat.core used by org.sat4j.minisat.uip
AssertingClauseGenerator
          An assertingClauseGenerator is responsible for the creation of an asserting clause during conflict analysis.