org.sat4j.pb
Class OPBStringSolver

java.lang.Object
  org.sat4j.tools.DimacsStringSolver
      org.sat4j.pb.OPBStringSolver

All Implemented Interfaces:

java.io.Serializable, IPBSolver, IProblem, ISolver

public class OPBStringSolver
extends DimacsStringSolver
implements IPBSolver

Solver used to display in a string the pb-instance in OPB format. That solver is useful to produce OPB files to be used by third party solvers.

Author:

parrain

See Also:

Serialized Form

Constructor Summary

OPBStringSolver()

OPBStringSolver(int initSize)

Method Summary

IConstr	addAtLeast(IVecInt literals, int degree)
IConstr	addAtMost(IVecInt literals, int degree)
IConstr	addClause(IVecInt literals)
IConstr	addPseudoBoolean(IVecInt lits, IVec<java.math.BigInteger> coeffs, boolean moreThan, java.math.BigInteger d) Create a Pseudo-Boolean constraint of the type "at least n of those literals must be satisfied"
java.lang.String	getExplanation()
ObjectiveFunction	getObjectiveFunction()
int	newVar(int howmany)
void	setExpectedNumberOfClauses(int nb)
void	setListOfVariablesForExplanation(IVecInt listOfVariables)
void	setObjectiveFunction(ObjectiveFunction obj)
java.lang.String	toString()
java.lang.String	toString(java.lang.String prefix)

Methods inherited from class org.sat4j.tools.DimacsStringSolver

addAllClauses, addBlockingClause, clearLearntClauses, expireTimeout, findModel, findModel, getOut, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, model, nConstraints, newVar, nextFreeVarId, nVars, printInfos, printStat, printStat, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setNbVars, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts

Methods inherited from class java.lang.Object

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

Methods inherited from interface org.sat4j.specs.ISolver

addAllClauses, addBlockingClause, clearLearntClauses, expireTimeout, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, newVar, nextFreeVarId, printStat, printStat, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts

Methods inherited from interface org.sat4j.specs.IProblem

findModel, findModel, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, model, nConstraints, nVars, printInfos

Constructor Detail

OPBStringSolver

public OPBStringSolver()

OPBStringSolver

public OPBStringSolver(int initSize)

Parameters:

initSize -

Method Detail

addPseudoBoolean

public IConstr addPseudoBoolean(IVecInt lits,
                                IVec<java.math.BigInteger> coeffs,
                                boolean moreThan,
                                java.math.BigInteger d)
                         throws ContradictionException

Description copied from interface: IPBSolver

Create a Pseudo-Boolean constraint of the type "at least n of those literals must be satisfied"

Specified by:

addPseudoBoolean in interface IPBSolver

Parameters:

lits - a set of literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

coeffs - the coefficients of the literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.

moreThan - true if it is a constraint >= degree

d - the degree of the cardinality constraint

Returns:

a reference to the constraint added in the solver, to use in removeConstr().

Throws:

ContradictionException - iff the vector of literals is empty or if the constraint is falsified after unit propagation

See Also:

ISolver.removeConstr(IConstr)

setObjectiveFunction

public void setObjectiveFunction(ObjectiveFunction obj)

Specified by:

setObjectiveFunction in interface IPBSolver

addAtLeast

public IConstr addAtLeast(IVecInt literals,
                          int degree)
                   throws ContradictionException

Specified by:

addAtLeast in interface ISolver

Overrides:

addAtLeast in class DimacsStringSolver

Throws:

ContradictionException

addAtMost

public IConstr addAtMost(IVecInt literals,
                         int degree)
                  throws ContradictionException

Specified by:

addAtMost in interface ISolver

Overrides:

addAtMost in class DimacsStringSolver

Throws:

ContradictionException

addClause

public IConstr addClause(IVecInt literals)
                  throws ContradictionException

Specified by:

addClause in interface ISolver

Overrides:

addClause in class DimacsStringSolver

Throws:

ContradictionException

getExplanation

public java.lang.String getExplanation()

setListOfVariablesForExplanation

public void setListOfVariablesForExplanation(IVecInt listOfVariables)

toString

public java.lang.String toString()

Overrides:

toString in class DimacsStringSolver

toString

public java.lang.String toString(java.lang.String prefix)

Specified by:

toString in interface ISolver

Overrides:

toString in class DimacsStringSolver

newVar

public int newVar(int howmany)

Specified by:

newVar in interface ISolver

Overrides:

newVar in class DimacsStringSolver

setExpectedNumberOfClauses

public void setExpectedNumberOfClauses(int nb)

Specified by:

setExpectedNumberOfClauses in interface ISolver

Overrides:

setExpectedNumberOfClauses in class DimacsStringSolver

getObjectiveFunction

public ObjectiveFunction getObjectiveFunction()

Specified by:

getObjectiveFunction in interface IPBSolver