Package org.opt4j.satdecoding

Provides classes for using a PB solver as Decoder.

See:
Description

Interface Summary

SATManager	Classes with this interface manage the creation of Genotypes and the decoding to a Model.
Solver	The Solver is an interface for SAT/PB solvers.

Class Summary

AbstractSATDecoder<G extends Genotype,P>	The AbstractSATDecoder can be used for the construction of custom SAT Decoders.
Constraint	A linear pseudo-Boolean Constraint as used in an Integer Linear Program (ILP).
DefaultSolver	The default SAT/PB solver is the SAT4JSolver with timeout 3600 seconds, fixed length learning with learning size 10, and MiniSAT restarts.
Literal	A Literal is a data structure that represents a variable and its phase.
MixedSATManager	The MixedSATManager encodes the decision strategy into two vectors: One binary vector for the phase and one double vector for the priority.
Model	The 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.
Order	The abstract Order is the base class for a decision strategy.
PooledSolver	The PooledSolver is a decorator that enables pooling of Solver instances and, therefore, a parallel execution of the Solvers.
SATGenotype	Specialized Genotype for the AbstractSATDecoder.
SATModule	Module class for a SAT-Solver.
Term	The Term is an element of the linear Constraint.
VarOrder	The VarOrder implements an Order like it is used in MiniSAT.

Enum Summary

Constraint.Operator

The Constraint.Operators correspond to the Boolean operators <=,=,>=.

Exception Summary

ContradictionException	Thrown if a contradiction is recognized.
TimeoutException	Thrown if the solver can not solve the problem within a given time bound.

Package org.opt4j.satdecoding Description

Provides classes for using a PB solver as Decoder.

Many optimization problems with a discrete search space consist of binary variables. However, in some cases not all representations of these variables are feasible . Common approaches deteriorate the objectives if the solution is not feasible. As a matter of fact, in case that the number of feasible solutions is much lower than the number of infeasible solutions, the optimization process is more focused on the search of feasible solutions than optimizing the objectives.

This package includes a specialized Decoder that gives the user the opportunity to define constraints that have to be fulfilled to obtain a feasible solution.

As an example for the SAT Decoding we will use the following example: Given is a vector with a fixed number of binary (0/1) variables. The objective is to minimize the number of 1s of this vector. The solution of this problem is quite simple: Set all variables to 0. However, in order to make this problem more difficult, we introduce the following condition: A solution is only considered feasible if the variables satisfy a set of constraints . The following example is used to illustrate this problem:

 minimize w + x + y + z
 subject to:
     w + x + y > 0    (constraint 1)
     y + z > 0        (constraint 2)
     w + z > 0        (constraint 3)
     x + y + z > 0    (constraint 4)
 

Solution (w=1,x=1,y=0,z=1) is feasible which fulfills all constraints and the objective is 3. On the other hand, for (w=0,x=0,y=0,z=0), the objective is 0 but this solution is not feasible and therefore invalid. A good solution that fulfills all constraints would be (w=0,x=1,y=0,z=1) with the objective value 2.

Example

In the following, an example that minimizes the ones of a random is outlined. First, the phenotype and Evaluator are defined.

 public class MinOnesResult extends ArrayList<Boolean> {
 }
 

 public class MinOnesEvaluator implements Evaluator<MinOnesResult> {
 
        public Objectives evaluate(MinOnesResult minOnesResult) {
 
                int value = 0;
                for (Boolean v : minOnesResult) {
                        if (v != null && v) {
                                value++;
                        }
                }
 
                Objectives objectives = new Objectives();
                objectives.add("ones", Sign.MIN, value);
                return objectives;
        }
 }
 

The Decoder is defined as follows:

 public class MinOnesDecoder extends AbstractSATDecoder<Genotype, MinOnesResult> {
 
        @Inject
        public MinOnesDecoder(SATManager satManager, Rand random) {
                super(satManager, random);
        }
 
        // Here you can set the constraints of your problem. In our case, we will
        // randomly generate a problem as a 3SAT problem (3 literals per clause)
        // with 1000 variables and 1000 clauses. This problem is known to be
        // NP-complete. However, we hope that there exists at least one feasible
        // solution (and with the seed 0 of random it does).
        public Set<Constraint> createConstraints() {
                Set<Constraint> constraints = new HashSet<Constraint>();
                Random random = new Random(0);
 
                for (int i = 0; i < 1000; i++) {
                        Constraint clause = new Constraint(">=", 1);
                        HashSet<Integer> vars = new HashSet<Integer>();
                        do {
                                vars.add(random.nextInt(1000));
                        } while (vars.size() < 3);
 
                        for (int n : vars) {
                                clause.add(new Literal(n, random.nextBoolean()));
                        }
 
                        constraints.add(clause);
                }
 
                return constraints;
        }
 
        public MinOnesResult convertModel(Model model) {
                MinOnesResult minOnesResult = new MinOnesResult();
 
                for (int i = 0; i < 1000; i++) {
                        minOnesResult.add(model.get(i));
                }
 
                return minOnesResult;
        }
 }
 

Finally, the problem specific module is defined as follows:

 public class MinOnesModule extends ProblemModule {
        public void config() {
                bindProblem(MinOnesDecoder.class, MinOnesDecoder.class, MinOnesEvaluator.class);
        }
 }