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.restarts   
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.
ILits
          That interface manages the solver's internal vocabulary.
ILits2
          Specific vocabulary taking special care of binary clauses.
ILits23
          Specific vocabulary taking special care of binary and ternary clauses.
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.
ILits2
          Specific vocabulary taking special care of binary clauses.
ILits23
          Specific vocabulary taking special care of binary and ternary clauses.
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.
ILits2
          Specific vocabulary taking special care of binary clauses.
ILits23
          Specific vocabulary taking special care of binary and ternary clauses.
IMarkableLits
          Vocabulary in which literals can be marked.
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.pb
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.
Handle
          This class simply holds a reference to a object.
ILits
          That interface manages the solver's internal vocabulary.
IOrder
          Interface for the variable ordering heuristics.
Learner
          Provide the learning service.
LearningStrategy
          Implementation of the strategy design pattern for allowing various learning schemes.
Propagatable
          This interface is to be implemented by the classes wanted to be notified of the falsification of a literal.
RestartStrategy
           
SearchParams
          Some parameters used during the search.
Solver
          The backbone of the library providing the modular implementation of a MiniSAT (Chaff) like solver.
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.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.
Handle
          This class simply holds a reference to a object.
ILits
          That interface manages the solver's internal vocabulary.
ILits2
          Specific vocabulary taking special care of binary clauses.
IOrder
          Interface for the variable ordering heuristics.
Lbool
          That enumeration defines the possible truth value for a variable: satisfied, falsified or unknown/undefined.
Learner
          Provide the learning service.
LearningStrategy
          Implementation of the strategy design pattern for allowing various learning schemes.
Propagatable
          This interface is to be implemented by the classes wanted to be notified of the falsification of a literal.
RestartStrategy
           
SearchListener
          Interface to the solver main steps.
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.
 

Classes in org.sat4j.minisat.core used by org.sat4j.minisat.restarts
RestartStrategy
           
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 © 2007 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.