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()
boolean	admitABetterSolution(IVecInt assumps)
Number	calculateObjective()
void	discard()
void	discardCurrentSolution()
void	forceObjectiveValueTo(Number forcedValue)
Number	getObjectiveValue()
boolean	hasNoObjectiveFunction()
int[]	model()
boolean	model(int var)
int	newVar(int howmany)
boolean	nonOptimalMeansSatisfiable()
void	reset()
void	setExpectedNumberOfClauses(int nb)
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)

Specified by:

newVar in interface ISolver

Overrides:

newVar in class SolverDecorator<IPBSolver>

setExpectedNumberOfClauses

public void setExpectedNumberOfClauses(int nb)

Specified by:

setExpectedNumberOfClauses in interface ISolver

Overrides:

setExpectedNumberOfClauses in class SolverDecorator<IPBSolver>

model

public int[] model()

Specified by:

model in interface IProblem

Overrides:

model in class SolverDecorator<IPBSolver>

model

public boolean model(int var)

Specified by:

model in interface IProblem

Overrides:

model in class SolverDecorator<IPBSolver>

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.

Throws:

ContradictionException

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

Specified by:

admitABetterSolution in interface IOptimizationProblem

Throws:

TimeoutException

admitABetterSolution

public boolean admitABetterSolution(IVecInt assumps)
                             throws TimeoutException

Specified by:

admitABetterSolution in interface IOptimizationProblem

Throws:

TimeoutException

reset

public void reset()

Specified by:

reset in interface ISolver

Overrides:

reset in class SolverDecorator<IPBSolver>

hasNoObjectiveFunction

public boolean hasNoObjectiveFunction()

Specified by:

hasNoObjectiveFunction in interface IOptimizationProblem

nonOptimalMeansSatisfiable

public boolean nonOptimalMeansSatisfiable()

Specified by:

nonOptimalMeansSatisfiable in interface IOptimizationProblem

calculateObjective

public Number calculateObjective()

Specified by:

calculateObjective in interface IOptimizationProblem

discardCurrentSolution

public void discardCurrentSolution()
                            throws ContradictionException

Specified by:

discardCurrentSolution in interface IOptimizationProblem

Throws:

ContradictionException

getObjectiveValue

public Number getObjectiveValue()

Specified by:

getObjectiveValue in interface IOptimizationProblem

discard

public void discard()
             throws ContradictionException

Specified by:

discard in interface IOptimizationProblem

Throws:

ContradictionException

forceObjectiveValueTo

public void forceObjectiveValueTo(Number forcedValue)
                           throws ContradictionException

Specified by:

forceObjectiveValueTo in interface IOptimizationProblem

Throws:

ContradictionException