org.sat4j.maxsat
Class WeightedMaxSatDecorator

java.lang.Object
  extended by org.sat4j.tools.SolverDecorator<IPBSolver>
      extended by org.sat4j.pb.PBSolverDecorator
          extended by 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


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