|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object org.sat4j.tools.SolverDecorator org.sat4j.opt.WeightedMaxSatDecorator
public class WeightedMaxSatDecorator
Constructor Summary | |
---|---|
WeightedMaxSatDecorator(ISolver solver)
|
Method Summary | |
---|---|
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. |
boolean |
admitABetterSolution()
|
java.lang.Number |
calculateObjective()
|
void |
discard()
|
boolean |
hasNoObjectiveFunction()
|
int[] |
model()
Provide a model (if any) for a satisfiable formula. |
int |
newVar(int howmany)
Create howmany variables in the solver (and thus in the
vocabulary). |
boolean |
nonOptimalMeansSatisfiable()
|
void |
reset()
Clean up the internal state of the solver. |
void |
setExpectedNumberOfClauses(int nb)
To inform the solver of the expected number of clauses to read. |
Methods inherited from class org.sat4j.tools.SolverDecorator |
---|
addAllClauses, addAtLeast, addAtMost, addPseudoBoolean, decorated, getStat, getTimeout, isSatisfiable, isSatisfiable, model, nConstraints, newVar, nVars, printStat, printStat, removeConstr, setTimeout, toString |
Methods inherited from class java.lang.Object |
---|
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Methods inherited from interface org.sat4j.specs.IProblem |
---|
isSatisfiable, isSatisfiable, model, nConstraints, nVars |
Constructor Detail |
---|
public WeightedMaxSatDecorator(ISolver solver)
Method Detail |
---|
public int[] model()
IProblem
model
in interface IProblem
model
in class SolverDecorator
public int newVar(int howmany)
ISolver
howmany
variables in the solver (and thus in the
vocabulary).
newVar
in interface ISolver
newVar
in class SolverDecorator
howmany
- number of variables to create
public void setExpectedNumberOfClauses(int nb)
ISolver
p cnf
line is read in dimacs formatted input file.
setExpectedNumberOfClauses
in interface ISolver
setExpectedNumberOfClauses
in class SolverDecorator
nb
- the expected number of clauses.public IConstr addClause(IVecInt literals) throws ContradictionException
ISolver
addClause
in interface ISolver
addClause
in class SolverDecorator
literals
- a set of literals
ContradictionException
- iff the vector of literals is empty or if it contains
only falsified literals after unit propagationISolver.removeConstr(IConstr)
public void reset()
ISolver
reset
in interface ISolver
reset
in class SolverDecorator
public boolean admitABetterSolution() throws TimeoutException
admitABetterSolution
in interface IOptimizationProblem
TimeoutException
public boolean hasNoObjectiveFunction()
hasNoObjectiveFunction
in interface IOptimizationProblem
public boolean nonOptimalMeansSatisfiable()
nonOptimalMeansSatisfiable
in interface IOptimizationProblem
public java.lang.Number calculateObjective()
calculateObjective
in interface IOptimizationProblem
public void discard() throws ContradictionException
discard
in interface IOptimizationProblem
ContradictionException
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |