org.sat4j.maxsat
Class WeightedMaxSatDecorator

java.lang.Object
  org.sat4j.tools.SolverDecorator<IPBSolver>
      org.sat4j.pb.PBSolverDecorator
          org.sat4j.maxsat.WeightedMaxSatDecorator

All Implemented Interfaces:

Serializable, IPBSolver, IOptimizationProblem, IProblem, ISolver

public class WeightedMaxSatDecorator
extends PBSolverDecorator
implements IOptimizationProblem

A decorator for solving weighted MAX SAT problems. The first value of the list of literals in the addClause() method contains the weight of the clause.

Author:

daniel

See Also:

Serialized Form

Field Summary

protected int	nbnewvar
protected int	nborigvars
protected boolean[]	prevboolmodel
protected int[]	prevfullmodel
protected int[]	prevmodel
static BigInteger	SAT4J_MAX_BIG_INTEGER
protected BigInteger	top

Constructor Summary

WeightedMaxSatDecorator(IPBSolver solver)

Method Summary

IConstr	addClause(IVecInt literals) Add a set of literals to the solver.
IConstr	addHardClause(IVecInt literals) Add a hard clause in the solver, i.e. a clause that must be satisfied.
void	addLiteralsToMinimize(IVecInt literals) Set some literals whose sum must be minimized.
IConstr	addSoftClause(BigInteger weight, IVecInt literals)
IConstr	addSoftClause(int weight, IVecInt literals) Add a soft clause to the solver.
IConstr	addSoftClause(IVecInt literals) Add a soft clause in the solver, i.e. a clause with a weight of 1.
void	addWeightedLiteralsToMinimize(IVecInt literals, IVec<BigInteger> coefficients) Set some literals whose sum must be minimized.
void	addWeightedLiteralsToMinimize(IVecInt literals, IVecInt coefficients) Set some literals whose sum must be minimized.
boolean	admitABetterSolution() Look for a solution of the optimization problem.
boolean	admitABetterSolution(IVecInt assumps) Look for a solution of the optimization problem when some literals are satisfied.
Number	calculateObjective() Compute the value of the objective function for the current solution.
void	discard() Discard the current solution in the optimization problem.
void	discardCurrentSolution() Discard the current solution in the optimization problem.
void	forceObjectiveValueTo(Number forcedValue) Force the value of the objective function.
Number	getObjectiveValue() Read only access to the value of the objective function for the current solution.
boolean	hasNoObjectiveFunction() If the optimization problem has no objective function, then it is a simple decision problem.
int[]	model() Provide a model (if any) for a satisfiable formula.
boolean	model(int var) Provide the truth value of a specific variable in the model.
int	newVar(int howmany) Create howmany variables in the solver (and thus in the vocabulary).
boolean	nonOptimalMeansSatisfiable() A suboptimal solution has different meaning depending of the optimization problem considered.
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.
void	setTopWeight(BigInteger top)

Methods inherited from class org.sat4j.pb.PBSolverDecorator

addPseudoBoolean, getObjectiveFunction, setObjectiveFunction

Methods inherited from class org.sat4j.tools.SolverDecorator

addAllClauses, addAtLeast, addAtMost, addBlockingClause, clearDecorated, clearLearntClauses, decorated, expireTimeout, findModel, findModel, getLogPrefix, getSearchListener, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, isVerbose, nConstraints, newVar, nextFreeVarId, nVars, printInfos, printStat, printStat, removeConstr, removeSubsumedConstr, setDBSimplificationAllowed, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, toString, toString, 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.IProblem

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

Methods inherited from interface org.sat4j.specs.ISolver

addAllClauses, addAtLeast, addAtMost, addBlockingClause, clearLearntClauses, expireTimeout, getLogPrefix, getSearchListener, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isVerbose, newVar, nextFreeVarId, printStat, printStat, removeConstr, removeSubsumedConstr, setDBSimplificationAllowed, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, toString, unsatExplanation

Field Detail

SAT4J_MAX_BIG_INTEGER

public static final BigInteger SAT4J_MAX_BIG_INTEGER

nborigvars

protected int nborigvars

nbnewvar

protected int nbnewvar

prevmodel

protected int[] prevmodel

prevboolmodel

protected boolean[] prevboolmodel

prevfullmodel

protected int[] prevfullmodel

top

protected BigInteger top

Constructor Detail

WeightedMaxSatDecorator

public WeightedMaxSatDecorator(IPBSolver solver)

Method Detail

newVar

public int newVar(int howmany)

Description copied from interface: ISolver

Create howmany variables in the solver (and thus in the vocabulary).

Specified by:

newVar in interface ISolver

Overrides:

newVar in class SolverDecorator<IPBSolver>

Parameters:

howmany - number of variables to create

Returns:

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

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 SolverDecorator<IPBSolver>

Parameters:

nb - the expected number of clauses.

See Also:

ISolver.newVar(int)

model

public int[] model()

Description copied from interface: IProblem

Provide a model (if any) for a satisfiable formula. That method should be called AFTER isSatisfiable() or isSatisfiable(IVecInt) if the formula is satisfiable. Else an exception UnsupportedOperationException is launched.

Specified by:

model in interface IProblem

Overrides:

model in class SolverDecorator<IPBSolver>

Returns:

a model of the formula as an array of literals to satisfy.

See Also:

IProblem.isSatisfiable(), IProblem.isSatisfiable(IVecInt)

model

public boolean model(int var)

Description copied from interface: IProblem

Provide the truth value of a specific variable in the model. That method should be called AFTER isSatisfiable() if the formula is satisfiable. Else an exception UnsupportedOperationException is launched.

Specified by:

model in interface IProblem

Overrides:

model in class SolverDecorator<IPBSolver>

Parameters:

var - the variable id in Dimacs format

Returns:

the truth value of that variable in the model

See Also:

IProblem.model()

setTopWeight

public void setTopWeight(BigInteger top)

addClause

public IConstr addClause(IVecInt literals)
                  throws ContradictionException

Add a set of literals to the solver. Here the assumption is that the first literal (literals[0]) is the weight of the constraint as found in the MAXSAT evaluation. if the weight is greater or equal to the top weight, then the clause is hard, else it is soft.

Specified by:

addClause in interface ISolver

Overrides:

addClause in class SolverDecorator<IPBSolver>

Parameters:

literals - a weighted clause, the weight being the first element of the vector.

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:

#setTopWeight(int)

addHardClause

public IConstr addHardClause(IVecInt literals)
                      throws ContradictionException

Add a hard clause in the solver, i.e. a clause that must be satisfied.

Parameters:

literals - the clause

Returns:

the constraint is it is not trivially satisfied.

Throws:

ContradictionException

addSoftClause

public IConstr addSoftClause(IVecInt literals)
                      throws ContradictionException

Add a soft clause in the solver, i.e. a clause with a weight of 1.

Parameters:

literals - the clause.

Returns:

the constraint is it is not trivially satisfied.

Throws:

ContradictionException

addSoftClause

public IConstr addSoftClause(int weight,
                             IVecInt literals)
                      throws ContradictionException

Add a soft clause to the solver. if the weight of the clause is greater of equal to the top weight, the clause will be considered as a hard clause.

Parameters:

weight - the weight of the clause

literals - the clause

Returns:

the constraint is it is not trivially satisfied.

Throws:

ContradictionException

addSoftClause

public IConstr addSoftClause(BigInteger weight,
                             IVecInt literals)
                      throws ContradictionException

Throws:

ContradictionException

addLiteralsToMinimize

public void addLiteralsToMinimize(IVecInt literals)

Set some literals whose sum must be minimized.

Parameters:

literals - the sum of those literals must be minimized.

addWeightedLiteralsToMinimize

public void addWeightedLiteralsToMinimize(IVecInt literals,
                                          IVec<BigInteger> coefficients)

Set some literals whose sum must be minimized.

Parameters:

literals - the sum of those literals must be minimized.

coefficients - the weight of the literals.

addWeightedLiteralsToMinimize

public void addWeightedLiteralsToMinimize(IVecInt literals,
                                          IVecInt coefficients)

Set some literals whose sum must be minimized.

Parameters:

literals - the sum of those literals must be minimized.

coefficients - the weight of the literals.

admitABetterSolution

public boolean admitABetterSolution()
                             throws TimeoutException

Description copied from interface: IOptimizationProblem

Look for a solution of the optimization problem.

Specified by:

admitABetterSolution in interface IOptimizationProblem

Returns:

true if a better solution than current one can be found.

Throws:

TimeoutException - if the solver cannot answer in reasonable time.

See Also:

ISolver.setTimeout(int)

admitABetterSolution

public boolean admitABetterSolution(IVecInt assumps)
                             throws TimeoutException

Description copied from interface: IOptimizationProblem

Look for a solution of the optimization problem when some literals are satisfied.

Specified by:

admitABetterSolution in interface IOptimizationProblem

Parameters:

assumps - a set of literals in Dimacs format.

Returns:

true if a better solution than current one can be found.

Throws:

TimeoutException - if the solver cannot answer in reasonable time.

See Also:

ISolver.setTimeout(int)

reset

public void reset()

Description copied from interface: ISolver

Clean up the internal state of the solver.

Specified by:

reset in interface ISolver

Overrides:

reset in class SolverDecorator<IPBSolver>

hasNoObjectiveFunction

public boolean hasNoObjectiveFunction()

Description copied from interface: IOptimizationProblem

If the optimization problem has no objective function, then it is a simple decision problem.

Specified by:

hasNoObjectiveFunction in interface IOptimizationProblem

Returns:

true if the problem is a decision problem, false if the problem is an optimization problem.

nonOptimalMeansSatisfiable

public boolean nonOptimalMeansSatisfiable()

Description copied from interface: IOptimizationProblem

A suboptimal solution has different meaning depending of the optimization problem considered. For instance, in the case of MAXSAT, a suboptimal solution does not mean that the problem is satisfiable, while in pseudo boolean optimization, it is true.

Specified by:

nonOptimalMeansSatisfiable in interface IOptimizationProblem

Returns:

true if founding a suboptimal solution means that the problem is satisfiable.

calculateObjective

public Number calculateObjective()

Description copied from interface: IOptimizationProblem

Compute the value of the objective function for the current solution. A call to that method only makes sense if hasNoObjectiveFunction()==false. DO NOT CALL THAT METHOD THAT WILL BE CALLED AUTOMATICALLY. USE getObjectiveValue() instead!

Specified by:

calculateObjective in interface IOptimizationProblem

Returns:

the value of the objective function.

See Also:

IOptimizationProblem.getObjectiveValue()

discardCurrentSolution

public void discardCurrentSolution()
                            throws ContradictionException

Description copied from interface: IOptimizationProblem

Discard the current solution in the optimization problem.

Specified by:

discardCurrentSolution in interface IOptimizationProblem

Throws:

ContradictionException - if a trivial inconsistency is detected.

getObjectiveValue

public Number getObjectiveValue()

Description copied from interface: IOptimizationProblem

Read only access to the value of the objective function for the current solution.

Specified by:

getObjectiveValue in interface IOptimizationProblem

Returns:

the value of the objective function for the current solution.

discard

public void discard()
             throws ContradictionException

Description copied from interface: IOptimizationProblem

Discard the current solution in the optimization problem. THE NAME WAS NOT NICE. STILL AVAILABLE TO AVOID BREAKING THE API. PLEASE USE THE LONGER discardCurrentSolution() instead.

Specified by:

discard in interface IOptimizationProblem

Throws:

ContradictionException - if a trivial inconsistency is detected.

See Also:

IOptimizationProblem.discardCurrentSolution()

forceObjectiveValueTo

public void forceObjectiveValueTo(Number forcedValue)
                           throws ContradictionException

Description copied from interface: IOptimizationProblem

Force the value of the objective function. This is especially useful to iterate over optimal solutions.

Specified by:

forceObjectiveValueTo in interface IOptimizationProblem

Throws:

ContradictionException