org.opt4j.satdecoding.sat4j
Class SAT4JSolver

java.lang.Object
  org.opt4j.satdecoding.sat4j.SAT4JSolver

All Implemented Interfaces:

Solver

Direct Known Subclasses:

DefaultSolver

public class SAT4JSolver
extends java.lang.Object
implements Solver

The SAT4JSolver implements a Solver. It is based on the Java SAT/PB-Solver from Sat4J.org.

Nested Class Summary

static class	SAT4JSolver.Learning
static class	SAT4JSolver.Restarts

Field Summary

protected java.util.Queue<Constraint>	constraints
protected int	nextVariable
protected org.sat4j.pb.core.PBSolverResolution	solver
protected java.util.Map<java.lang.Object,java.lang.Integer>	variables

Constructor Summary

SAT4JSolver(int timeout, int clauseLearningLength, SAT4JSolver.Learning learning, SAT4JSolver.Restarts restarts)
Constructs a new SAT4JSolver with a timeout and the number of kept learning clauses.

Method Summary

void	addConstraint(Constraint constraint) Adds a Constraint to the Solver.
protected void	addConstraintToSolver(Constraint constraint)
protected void	setNVars(int n) Sets the instance to n vars.
Model	solve(Order order) Solve the problem defined by the constraints with a given order (branching strategy).
protected org.sat4j.core.VecInt	toVecInt(java.lang.Iterable<Literal> list)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

constraints

protected final java.util.Queue<Constraint> constraints

solver

protected final org.sat4j.pb.core.PBSolverResolution solver

variables

protected final java.util.Map<java.lang.Object,java.lang.Integer> variables

nextVariable

protected int nextVariable

Constructor Detail

SAT4JSolver

@Inject
public SAT4JSolver(int timeout,
                          int clauseLearningLength,
                          SAT4JSolver.Learning learning,
                          SAT4JSolver.Restarts restarts)

Constructs a new SAT4JSolver with a timeout and the number of kept learning clauses. Additionally, this constructor allows the specification of the learning and restart strategy.

Parameters:

timeout - timeout in seconds

clauseLearningLength - clauses are learned if they have a smaller or equal number of literals per clause

learning - the learning strategy

restarts - the restart strategy

Method Detail

addConstraint

public void addConstraint(Constraint constraint)

Description copied from interface: Solver

Adds a Constraint to the Solver.

Specified by:

addConstraint in interface Solver

Parameters:

constraint - the added constraint

solve

public Model solve(Order order)
            throws TimeoutException,
                   ContradictionException

Description copied from interface: Solver

Solve the problem defined by the constraints with a given order (branching strategy).

Specified by:

solve in interface Solver

Parameters:

order - the branching strategy

Returns:

a model that represents a feasible solution

Throws:

TimeoutException - if a feasible solution cannot be found within a given amount of time

ContradictionException - if no feasible solution exists

addConstraintToSolver

protected void addConstraintToSolver(Constraint constraint)

toVecInt

protected org.sat4j.core.VecInt toVecInt(java.lang.Iterable<Literal> list)

setNVars

protected void setNVars(int n)

Sets the instance to n vars.

Parameters:

n - the number of vars.