org.sat4j.pb
Class UserFriendlyPBStringSolver<T>

java.lang.Object
  org.sat4j.tools.AbstractOutputSolver
      org.sat4j.tools.DimacsStringSolver
          org.sat4j.pb.UserFriendlyPBStringSolver<T>

All Implemented Interfaces:

Serializable, IPBSolver, IProblem, ISolver

public class UserFriendlyPBStringSolver<T>
extends DimacsStringSolver
implements IPBSolver

Solver to display SAT instances using domain objects names instead of Dimacs numbers.

Author:

leberre

See Also:

Serialized Form

Field Summary

Fields inherited from class org.sat4j.tools.AbstractOutputSolver

firstConstr, fixedNbClauses, nbclauses, nbvars

Constructor Summary

UserFriendlyPBStringSolver()

UserFriendlyPBStringSolver(int initSize)

Method Summary

IConstr	addAtLeast(IVecInt literals, int degree) Create a cardinality constraint of the type "at least n of those literals must be satisfied"
IConstr	addAtLeast(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree) Create a pseudo-boolean constraint of the type "at least".
IConstr	addAtLeast(IVecInt literals, IVecInt coeffs, int degree) Create a pseudo-boolean constraint of the type "at least".
IConstr	addAtMost(IVecInt literals, int degree) Create a cardinality constraint of the type "at most n of those literals must be satisfied"
IConstr	addAtMost(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree) Create a pseudo boolean constraint of the type "at most".
IConstr	addAtMost(IVecInt literals, IVecInt coeffs, int degree) Create a pseudo boolean constraint of the type "at most".
IConstr	addClause(IVecInt literals) Create a clause from a set of literals The literals are represented by non null integers such that opposite literals a represented by opposite values.
IConstr	addExactly(IVecInt literals, IVec<BigInteger> coeffs, BigInteger weight) Create a pseudo-boolean constraint of the type "subset sum".
IConstr	addExactly(IVecInt literals, IVecInt coeffs, int weight) Create a pseudo-boolean constraint of the type "subset sum".
IConstr	addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs, boolean moreThan, BigInteger d) Create a Pseudo-Boolean constraint of the type "at least n or at most n of those literals must be satisfied"
String	getExplanation()
ObjectiveFunction	getObjectiveFunction() Retrieve the objective function from the solver.
int	newVar(int howmany) Declare howmany variables in the problem (and thus in the vocabulary), that will be represented using the Dimacs format by integers ranging from 1 to howmany.
void	setExpectedNumberOfClauses(int nb) To inform the solver of the expected number of clauses to read.
void	setListOfVariablesForExplanation(IVecInt listOfVariables)
void	setMapping(Map<Integer,T> mapping)
void	setObjectiveFunction(ObjectiveFunction obj) Provide an objective function to the solver.
String	toString()
String	toString(String prefix) Display a textual representation of the solver configuration.

Methods inherited from class org.sat4j.tools.DimacsStringSolver

addExactly, getOut, modelWithInternalVariables, nConstraints, newVar, nextFreeVarId, nVars, realNumberOfVariables, registerLiteral, reset, setNbVars

Methods inherited from class org.sat4j.tools.AbstractOutputSolver

addAllClauses, addBlockingClause, clearLearntClauses, expireTimeout, findModel, findModel, getLogPrefix, getSearchListener, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, isVerbose, model, model, primeImplicant, printInfos, printStat, printStat, removeConstr, removeSubsumedConstr, setDBSimplificationAllowed, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, unsatExplanation

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, addExactly, clearLearntClauses, expireTimeout, getLogPrefix, getSearchListener, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isVerbose, modelWithInternalVariables, newVar, nextFreeVarId, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, unsatExplanation

Methods inherited from interface org.sat4j.specs.IProblem

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

Constructor Detail

UserFriendlyPBStringSolver

public UserFriendlyPBStringSolver()

UserFriendlyPBStringSolver

public UserFriendlyPBStringSolver(int initSize)

Parameters:

initSize -

Method Detail

setMapping

public void setMapping(Map<Integer,T> mapping)

addPseudoBoolean

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

Description copied from interface: IPBSolver

Create a Pseudo-Boolean constraint of the type "at least n or at most 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, false 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)

Description copied from interface: IPBSolver

Provide an objective function to the solver.

Specified by:

setObjectiveFunction in interface IPBSolver

Parameters:

obj - the objective function

addAtLeast

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

Description copied from interface: ISolver

Create a cardinality constraint of the type "at least n of those literals must be satisfied"

Specified by:

addAtLeast in interface ISolver

Overrides:

addAtLeast in class DimacsStringSolver

Parameters:

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

degree - the degree (n) 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 degree literals are not remaining unfalsified after unit propagation

See Also:

ISolver.removeConstr(IConstr)

addAtMost

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

Description copied from interface: ISolver

Create a cardinality constraint of the type "at most n of those literals must be satisfied"

Specified by:

addAtMost in interface ISolver

Overrides:

addAtMost in class DimacsStringSolver

Parameters:

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

degree - the degree (n) 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 it contains more than degree satisfied literals after unit propagation

See Also:

ISolver.removeConstr(IConstr)

addClause

public IConstr addClause(IVecInt literals)
                  throws ContradictionException

Description copied from interface: ISolver

Create a clause from a set of literals The literals are represented by non null integers such that opposite literals a represented by opposite values. (classical Dimacs way of representing literals).

Specified by:

addClause in interface ISolver

Overrides:

addClause in class DimacsStringSolver

Parameters:

literals - a set of literals

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 it contains only falsified literals after unit propagation

See Also:

ISolver.removeConstr(IConstr)

getExplanation

public String getExplanation()

setListOfVariablesForExplanation

public void setListOfVariablesForExplanation(IVecInt listOfVariables)

toString

public String toString()

Overrides:

toString in class DimacsStringSolver

toString

public String toString(String prefix)

Description copied from interface: ISolver

Display a textual representation of the solver configuration.

Specified by:

toString in interface ISolver

Overrides:

toString in class DimacsStringSolver

Parameters:

prefix - the prefix to use on each line.

Returns:

a textual description of the solver internals.

newVar

public int newVar(int howmany)

Description copied from interface: IProblem

Declare howmany variables in the problem (and thus in the vocabulary), that will be represented using the Dimacs format by integers ranging from 1 to howmany. That feature allows encodings to create additional variables with identifier starting at howmany+1.

Specified by:

newVar in interface IProblem

Overrides:

newVar in class DimacsStringSolver

Parameters:

howmany - number of variables to create

Returns:

the total number of variables available in the solver (the highest variable number)

See Also:

IProblem.nVars()

setExpectedNumberOfClauses

public void setExpectedNumberOfClauses(int nb)

Description copied from interface: ISolver

To inform the solver of the expected number of clauses to read. This is an optional method, that is called when the p cnf line is read in dimacs formatted input file. Note that this method is supposed to be called AFTER a call to newVar(int)

Specified by:

setExpectedNumberOfClauses in interface ISolver

Overrides:

setExpectedNumberOfClauses in class DimacsStringSolver

Parameters:

nb - the expected number of clauses.

See Also:

IProblem.newVar(int)

getObjectiveFunction

public ObjectiveFunction getObjectiveFunction()

Description copied from interface: IPBSolver

Retrieve the objective function from the solver.

Specified by:

getObjectiveFunction in interface IPBSolver

Returns:

the objective function

addAtMost

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

Description copied from interface: IPBSolver

Create a pseudo boolean constraint of the type "at most".

Specified by:

addAtMost in interface IPBSolver

Parameters:

literals - 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.

degree - the degree of the pseudo-boolean constraint

Returns:

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

Throws:

ContradictionException - iff the constraint is found trivially unsat.

See Also:

ISolver.removeConstr(IConstr)

addAtMost

public IConstr addAtMost(IVecInt literals,
                         IVec<BigInteger> coeffs,
                         BigInteger degree)
                  throws ContradictionException

Description copied from interface: IPBSolver

Create a pseudo boolean constraint of the type "at most".

Specified by:

addAtMost in interface IPBSolver

Parameters:

literals - 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.

degree - the degree of the pseudo-boolean constraint

Returns:

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

Throws:

ContradictionException - iff the constraint is found trivially unsat.

See Also:

ISolver.removeConstr(IConstr)

addAtLeast

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

Description copied from interface: IPBSolver

Create a pseudo-boolean constraint of the type "at least".

Specified by:

addAtLeast in interface IPBSolver

Parameters:

literals - 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.

degree - the degree of the pseudo-boolean constraint

Returns:

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

Throws:

ContradictionException - iff the constraint is found trivially unsat.

See Also:

ISolver.removeConstr(IConstr)

addAtLeast

public IConstr addAtLeast(IVecInt literals,
                          IVec<BigInteger> coeffs,
                          BigInteger degree)
                   throws ContradictionException

Description copied from interface: IPBSolver

Create a pseudo-boolean constraint of the type "at least".

Specified by:

addAtLeast in interface IPBSolver

Parameters:

literals - 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.

degree - the degree of the pseudo-boolean constraint

Returns:

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

Throws:

ContradictionException - iff the constraint is found trivially unsat.

See Also:

ISolver.removeConstr(IConstr)

addExactly

public IConstr addExactly(IVecInt literals,
                          IVecInt coeffs,
                          int weight)
                   throws ContradictionException

Description copied from interface: IPBSolver

Create a pseudo-boolean constraint of the type "subset sum".

Specified by:

addExactly in interface IPBSolver

Parameters:

literals - 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.

weight - the number of literals that must be satisfied

Returns:

a reference to the constraint added to the solver. It might return an object representing a group of constraints.

Throws:

ContradictionException - iff the constraint is trivially unsatisfiable.

addExactly

public IConstr addExactly(IVecInt literals,
                          IVec<BigInteger> coeffs,
                          BigInteger weight)
                   throws ContradictionException

Description copied from interface: IPBSolver

Create a pseudo-boolean constraint of the type "subset sum".

Specified by:

addExactly in interface IPBSolver

Parameters:

literals - 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.

weight - the number of literals that must be satisfied

Returns:

a reference to the constraint added to the solver. It might return an object representing a group of constraints.

Throws:

ContradictionException - iff the constraint is trivially unsatisfiable.