Logo Search packages:      
Sourcecode: sat4j version File versions

org::sat4j::pb::PseudoOptDecorator Class Reference

Inheritance diagram for org::sat4j::pb::PseudoOptDecorator:

org::sat4j::pb::PBSolverDecorator org::sat4j::specs::IOptimizationProblem org::sat4j::pb::IPBSolver org::sat4j::specs::IProblem org::sat4j::specs::ISolver org::sat4j::specs::IProblem

List of all members.

Detailed Description

A decorator that computes minimal pseudo boolean models.


Definition at line 42 of file PseudoOptDecorator.java.

Public Member Functions

void addAllClauses (IVec< IVecInt > clauses) throws ContradictionException
IConstr addAtLeast (IVecInt literals, int degree) throws ContradictionException
IConstr addAtMost (IVecInt literals, int degree) throws ContradictionException
IConstr addClause (IVecInt literals) throws ContradictionException
IConstr addPseudoBoolean (IVecInt lits, IVec< BigInteger > coeffs, boolean moreThan, BigInteger d) throws ContradictionException
boolean admitABetterSolution () throws TimeoutException
Number calculateObjective ()
void clearLearntClauses ()
void discard () throws ContradictionException
void expireTimeout ()
int[] findModel (IVecInt assumps) throws TimeoutException
int[] findModel () throws TimeoutException
String getExplanation ()
Map< String, Number > getStat ()
int getTimeout ()
boolean hasNoObjectiveFunction ()
boolean isDBSimplificationAllowed ()
boolean isSatisfiable (IVecInt assumps) throws TimeoutException
boolean isSatisfiable (boolean globalTimeout) throws TimeoutException
boolean isSatisfiable (IVecInt assumps, boolean globalTimeout) throws TimeoutException
boolean isSatisfiable () throws TimeoutException
boolean model (int var)
int[] model ()
int nConstraints ()
int newVar (int howmany)
boolean nonOptimalMeansSatisfiable ()
int nVars ()
void printInfos (PrintWriter out, String prefix)
void printStat (PrintWriter out, String prefix)
void printStat (PrintStream out, String prefix)
 PseudoOptDecorator (IPBSolver solver)
boolean removeConstr (IConstr c)
void reset ()
void setDBSimplificationAllowed (boolean status)
void setExpectedNumberOfClauses (int nb)
void setListOfVariablesForExplanation (IVecInt varExplain)
void setObjectiveFunction (ObjectiveFunction objf)
void setTimeout (int t)
void setTimeoutMs (long t)
void setTimeoutOnConflicts (int count)
String toString (String prefix)

Package Functions

int newVar ()

Private Attributes

ObjectiveFunction objfct
boolean[] prevfullmodel
int[] prevmodel

Static Private Attributes

static final long serialVersionUID = 1L

The documentation for this class was generated from the following file:

Generated by  Doxygen 1.6.0   Back to index