|
||||||||||
| PREV NEXT | FRAMES NO FRAMES | |||||||||
| 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. |
|
|
||||||||||
| PREV NEXT | FRAMES NO FRAMES | |||||||||