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.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.restarts Various restart strategies. 
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
          The aim of the factory is to provide a concrete implementation of clauses, cardinality constraints and pseudo boolean consraints.
IOrder
          Interface for the variable ordering heuristics.
Solver
          The backbone of the library providing the modular implementation of a MiniSAT (Chaff) like solver.
 

Classes in org.sat4j.minisat.core used by org.sat4j.minisat.constraints
Constr
          Basic constraint abstraction used in Solver.
DataStructureFactory
          The aim of the factory is to provide a concrete implementation of clauses, cardinality constraints and pseudo boolean consraints.
ILits
          That interface manages the solver's internal vocabulary.
Learner
          Provide the learning service.
Propagatable
          This interface is to be implemented by the classes wanted to be notified of the falsification of a literal.
UnitPropagationListener
          Interface providing the unit propagation capability.
 

Classes in org.sat4j.minisat.core used by org.sat4j.minisat.constraints.card
Constr
          Basic constraint abstraction used in Solver.
ILits
          That interface manages the solver's internal vocabulary.
Propagatable
          This interface is to be implemented by the classes wanted to be notified of the falsification of a literal.
Undoable
          Interface providing the undoable service.
UnitPropagationListener
          Interface providing the unit propagation capability.
 

Classes in org.sat4j.minisat.core used by org.sat4j.minisat.constraints.cnf
Constr
          Basic constraint abstraction used in Solver.
ILits
          That interface manages the solver's internal vocabulary.
Propagatable
          This interface is to be implemented by the classes wanted to be notified of the falsification of a literal.
Undoable
          Interface providing the undoable service.
UnitPropagationListener
          Interface providing the unit propagation capability.
 

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
          Basic constraint abstraction used in Solver.
DataStructureFactory
          The aim of the factory is to provide a concrete implementation of clauses, cardinality constraints and pseudo boolean consraints.
ILits
          That interface manages the solver's internal vocabulary.
IOrder
          Interface for the variable ordering heuristics.
IPhaseSelectionStrategy
          The responsibility of that class is to choose the phase (positive or negative) of the variable that was selected by the IOrder.
Learner
          Provide the learning service.
LearningStrategy
          Implementation of the strategy design pattern for allowing various learning schemes.
Pair
          Utility class to be used to return the two results of a conflict analysis.
Propagatable
          This interface is to be implemented by the classes wanted to be notified of the falsification of a literal.
RestartStrategy
          Abstraction allowing to choose various restarts strategies.
SearchParams
          Some parameters used during the search.
Solver
          The backbone of the library providing the modular implementation of a MiniSAT (Chaff) like solver.
SolverStats
          Contains some statistics regarding the search.
Undoable
          Interface providing the undoable service.
UnitPropagationListener
          Interface providing the unit propagation capability.
VarActivityListener
          Interface providing the capability to increase the activity of a given variable.
 

Classes in org.sat4j.minisat.core used by org.sat4j.minisat.learning
Constr
          Basic constraint abstraction used in Solver.
DataStructureFactory
          The aim of the factory is to provide a concrete implementation of clauses, cardinality constraints and pseudo boolean consraints.
ILits
          That interface manages the solver's internal vocabulary.
IOrder
          Interface for the variable ordering heuristics.
LearningStrategy
          Implementation of the strategy design pattern for allowing various learning schemes.
Solver
          The backbone of the library providing the modular implementation of a MiniSAT (Chaff) like solver.
VarActivityListener
          Interface providing the capability to increase the activity of a given variable.
 

Classes in org.sat4j.minisat.core used by org.sat4j.minisat.orders
Heap
          Heap implementation used to maintain the variables order in some heuristics.
ILits
          That interface manages the solver's internal vocabulary.
IOrder
          Interface for the variable ordering heuristics.
IPhaseSelectionStrategy
          The responsibility of that class is to choose the phase (positive or negative) of the variable that was selected by the IOrder.
 

Classes in org.sat4j.minisat.core used by org.sat4j.minisat.restarts
RestartStrategy
          Abstraction allowing to choose various restarts strategies.
SearchParams
          Some parameters used during the search.
 

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.
 



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