Package | Description |
---|---|
org.sat4j.csp |
Classes needed for CSP to SAT translation.
|
org.sat4j.maxsat |
MAXSAT and Weighted Max SAT framework.
|
org.sat4j.minisat |
Implementation of the MiniSAT specification in Java.
|
org.sat4j.minisat.constraints |
Implementations of various constraints for MiniSAT.
|
org.sat4j.minisat.core |
Implementation of the MiniSAT solver skeleton.
|
org.sat4j.minisat.learning |
Various learning strategies.
|
org.sat4j.pb.constraints |
Implementation of data structures for pseudo boolean constraints.
|
org.sat4j.pb.core |
Implementations of pseudo boolean solvers
|
Modifier and Type | Method and Description |
---|---|
static <L extends ILits> |
SolverFactory.newMiniSAT(DataStructureFactory dsf) |
Modifier and Type | Method and Description |
---|---|
static <L extends ILits> |
SolverFactory.newMiniSAT(DataStructureFactory dsf) |
Modifier and Type | Method and Description |
---|---|
static Solver<DataStructureFactory> |
SolverFactory.newMiniMaxSAT()
Builds a SAT solver for the MAX sat evaluation.
|
Modifier and Type | Method and Description |
---|---|
static Solver<DataStructureFactory> |
SolverFactory.newMiniLearning(DataStructureFactory dsf,
IOrder order) |
static Solver<DataStructureFactory> |
SolverFactory.newMiniLearningHeap(DataStructureFactory dsf) |
static Solver<DataStructureFactory> |
SolverFactory.newMiniSATHeap(DataStructureFactory dsf) |
Modifier and Type | Class and Description |
---|---|
class |
AbstractCardinalityDataStructure |
class |
AbstractDataStructureFactory |
class |
CardinalityDataStructure |
class |
CardinalityDataStructureYanMax |
class |
CardinalityDataStructureYanMin |
class |
ClausalDataStructureWL |
class |
MixedDataStructureDanielHT
Uses specific data structure for cardinality constraints.
|
class |
MixedDataStructureDanielWL |
class |
MixedDataStructureSingleWL |
Modifier and Type | Interface and Description |
---|---|
interface |
ICDCL<D extends DataStructureFactory>
Abstraction for Conflict Driven Clause Learning Solver.
|
interface |
LearningStrategy<D extends DataStructureFactory>
Implementation of the strategy design pattern for allowing various learning
schemes.
|
class |
Solver<D extends DataStructureFactory>
The backbone of the library providing the modular implementation of a MiniSAT
(Chaff) like solver.
|
Modifier and Type | Field and Description |
---|---|
protected D |
Solver.dsfactory |
Modifier and Type | Method and Description |
---|---|
DataStructureFactory |
Solver.getDSFactory() |
Modifier and Type | Class and Description |
---|---|
class |
ActiveLearning<D extends DataStructureFactory>
Learn clauses with a great number of active variables.
|
class |
ClauseOnlyLearning<D extends DataStructureFactory>
The solver only records among all the constraints only the clauses.
|
class |
FixedLengthLearning<D extends DataStructureFactory>
A learning scheme for learning constraints of size smaller than a given
constant.
|
class |
LimitedLearning<D extends DataStructureFactory>
Learn only clauses which size is smaller than a percentage of the number of
variables.
|
class |
MiniSATLearning<D extends DataStructureFactory>
MiniSAT learning scheme.
|
class |
NoLearningButHeuristics<D extends DataStructureFactory>
Allows MiniSAT to do backjumping without learning.
|
class |
NoLearningNoHeuristics<D extends DataStructureFactory>
Allows MiniSAT to do backjumping without learning.
|
class |
PercentLengthLearning<D extends DataStructureFactory>
Selects the constraints to learn according to its length as a percentage of
the total number of variables in the solver universe.
|
Modifier and Type | Method and Description |
---|---|
void |
MiniSATLearning.setDataStructureFactory(DataStructureFactory dsf) |
Modifier and Type | Interface and Description |
---|---|
interface |
PBDataStructureFactory |
Copyright © 2013 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.