org.sat4j.pb
Class UserFriendlyPBStringSolver<T>

java.lang.Object
  extended by org.sat4j.tools.DimacsStringSolver
      extended by org.sat4j.pb.UserFriendlyPBStringSolver<T>
All Implemented Interfaces:
java.io.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

Constructor Summary
UserFriendlyPBStringSolver()
           
UserFriendlyPBStringSolver(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 setMapping(java.util.Map<java.lang.Integer,T> mapping)
           
 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

UserFriendlyPBStringSolver

public UserFriendlyPBStringSolver()

UserFriendlyPBStringSolver

public UserFriendlyPBStringSolver(int initSize)
Parameters:
initSize -
Method Detail

setMapping

public void setMapping(java.util.Map<java.lang.Integer,T> mapping)

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


Copyright © 2009 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.