|
|||||||||
| PREV NEXT | FRAMES NO FRAMES | ||||||||
AbstractSATDecoder can be used for the construction of custom SAT
Decoders.AbstractSATDecoder with the given
SATManager.
Literal with the coefficient 1.
Literal with specified coefficient.
Constraint to the Solver.
Constraint as used in an Integer Linear
Program (ILP).Constraint with >=1.
Constraint.
Constraint.
Constraint.Operators correspond to the Boolean operators <=,=,>=.true if the Constraint contains the
Literal.
ContradictionException.
ContradictionException with a message.
ContradictionException.
ContradictionException.
Model into a phenotype.
Constraint.
Constraints.
Genotype from the variables, priorities, and
phases.
Genotype to a phenotype by using a SAT/PB solver.
Genotype into a Model.
SAT4JSolver with timeout 3600
seconds, fixed length learning with learning size 10, and MiniSAT restarts.Object with this for equality.
Term equals another Term if they have equal
Literals and coefficients.
Literals.
Constraint.Operator.
String to an operator.
Solver.
SAT4JSolver.
Constraint is satisfied for a given
Model.
Literal.
Constraints and variables.
true if lhs Constraint.Operator rhs is
true.
Literal is a data structure that represents a variable and its
phase.Literal with a variable and their phase.
MixedSATManager encodes the decision strategy into two vectors:
One binary vector for the phase and one double vector for the priority.MixedSATManager.
Model is a data structure that represents a solution of the given
problem, i.e., all Literals are set such that all Constraints
specified by the AbstractSATDecoder are feasible.Model.
Literal.
Order is the base class for a decision strategy.Order.
Decoder.Literal.
PooledSolver is a decorator that enables pooling of
Solver instances and, therefore, a parallel execution of the
Solvers.PooledSolver.
SAT4JModule enables and configures the SAT4JSolver.SAT4JSolver implements a Solver.SAT4JSolver with a timeout and the number of
kept learning clauses.
Genotype for the AbstractSATDecoder.SATGenotype with empty vectors.
SATGenotype with the given vectors.
Genotypes and the
decoding to a Model.Solver.Constraint.Operator.
SAT4JSolver.
var to the specified
value.
varInc to increase the activity of the variables.
phase of a variable var.
Solver is an interface for SAT/PB solvers.Term is an element of the linear Constraint.Term.
TimeoutException.
String representation of this Constraint.Operator.
String representation of this Literal.
var by the specified
value.
Literal.
VariableOrder implementation for the SAT4J interface.VariableOrder.
VarOrder implements an Order like it is used in MiniSAT.VarOrder.
|
|||||||||
| PREV NEXT | FRAMES NO FRAMES | ||||||||