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, IProblem, ISolver

public class WeightedMaxSatDecorator
extends PBSolverDecorator

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
           
static BigInteger SAT4J_MAX_BIG_INTEGER
           
protected  BigInteger top
           
 
Constructor Summary
WeightedMaxSatDecorator(IPBSolver solver)
           
 
Method Summary
 IConstr addClause(IVecInt literals)
          Add a soft clause 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 addSoftAtLeast(BigInteger weight, IVecInt literals, int degree)
          Allow adding a new soft cardinality constraint in the solver.
 IConstr addSoftAtLeast(int weight, IVecInt literals, int degree)
          Allow adding a new soft cardinality constraint in the solver.
 IConstr addSoftAtLeast(IVecInt literals, int degree)
          Allow adding a new soft cardinality constraint in the solver.
 IConstr addSoftAtMost(BigInteger weight, IVecInt literals, int degree)
          Allow adding a new soft cardinality constraint in the solver.
 IConstr addSoftAtMost(int weight, IVecInt literals, int degree)
          Allow adding a new soft cardinality constraint in the solver.
 IConstr addSoftAtMost(IVecInt literals, int degree)
          Allow adding a new soft cardinality constraint in the solver.
 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.
 void forceObjectiveValueTo(Number forcedValue)
           
 void reset()
           
 void setExpectedNumberOfClauses(int nb)
           
 void setTopWeight(BigInteger top)
           
 
Methods inherited from class org.sat4j.pb.PBSolverDecorator
addAtLeast, addAtLeast, addAtMost, addAtMost, addExactly, addExactly, addPseudoBoolean, getObjectiveFunction, setObjectiveFunction
 
Methods inherited from class org.sat4j.tools.SolverDecorator
addAllClauses, addAtLeast, addAtMost, addBlockingClause, addExactly, clearDecorated, clearLearntClauses, decorated, expireTimeout, findModel, findModel, getLogPrefix, getSearchListener, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, isVerbose, model, model, modelWithInternalVariables, nConstraints, newVar, newVar, nextFreeVarId, nVars, primeImplicant, printInfos, printStat, printStat, realNumberOfVariables, registerLiteral, 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.ISolver
addAllClauses, addAtLeast, addAtMost, addBlockingClause, addExactly, clearLearntClauses, expireTimeout, getLogPrefix, getSearchListener, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isVerbose, modelWithInternalVariables, newVar, nextFreeVarId, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, setDBSimplificationAllowed, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, toString, unsatExplanation
 
Methods inherited from interface org.sat4j.specs.IProblem
findModel, findModel, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, model, nConstraints, newVar, nVars, primeImplicant, printInfos
 

Field Detail

SAT4J_MAX_BIG_INTEGER

public static final BigInteger SAT4J_MAX_BIG_INTEGER

nbnewvar

protected int nbnewvar

top

protected BigInteger top
Constructor Detail

WeightedMaxSatDecorator

public WeightedMaxSatDecorator(IPBSolver solver)
Method Detail

setExpectedNumberOfClauses

public void setExpectedNumberOfClauses(int nb)
Specified by:
setExpectedNumberOfClauses in interface ISolver
Overrides:
setExpectedNumberOfClauses in class SolverDecorator<IPBSolver>

setTopWeight

public void setTopWeight(BigInteger top)

addClause

public IConstr addClause(IVecInt literals)
                  throws ContradictionException
Add a soft clause to the solver. That method allows to read a clause in a CNF and to consider it as soft, in order to solve MAXSAT problems. Note that the behavior of that method changed in release 2.3.1. Prior to that, the method was expecting a weight as first element of the list of literals.

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

addSoftAtLeast

public IConstr addSoftAtLeast(IVecInt literals,
                              int degree)
                       throws ContradictionException
Allow adding a new soft cardinality constraint in the solver.

Parameters:
literals - the literals of the cardinality constraint.
degree - the degree of the cardinality constraint.
Returns:
a pseudo boolean constraint encoding that soft constraint.
Throws:
ContradictionException - if a trivial contradiction is found.
Since:
2.3

addSoftAtLeast

public IConstr addSoftAtLeast(int weight,
                              IVecInt literals,
                              int degree)
                       throws ContradictionException
Allow adding a new soft cardinality constraint in the solver.

Parameters:
weight - the weight of the constraint.
literals - the literals of the cardinality constraint.
degree - the degree of the cardinality constraint.
Returns:
a pseudo boolean constraint encoding that soft constraint.
Throws:
ContradictionException - if a trivial contradiction is found.
Since:
2.3

addSoftAtLeast

public IConstr addSoftAtLeast(BigInteger weight,
                              IVecInt literals,
                              int degree)
                       throws ContradictionException
Allow adding a new soft cardinality constraint in the solver.

Parameters:
weight - the weight of the constraint.
literals - the literals of the cardinality constraint.
degree - the degree of the cardinality constraint.
Returns:
a pseudo boolean constraint encoding that soft constraint.
Throws:
ContradictionException - if a trivial contradiction is found.
Since:
2.3

addSoftAtMost

public IConstr addSoftAtMost(IVecInt literals,
                             int degree)
                      throws ContradictionException
Allow adding a new soft cardinality constraint in the solver.

Parameters:
literals - the literals of the cardinality constraint.
degree - the degree of the cardinality constraint.
Returns:
a pseudo boolean constraint encoding that soft constraint.
Throws:
ContradictionException - if a trivial contradiction is found.
Since:
2.3

addSoftAtMost

public IConstr addSoftAtMost(int weight,
                             IVecInt literals,
                             int degree)
                      throws ContradictionException
Allow adding a new soft cardinality constraint in the solver.

Parameters:
weight - the weight of the constraint.
literals - the literals of the cardinality constraint.
degree - the degree of the cardinality constraint.
Returns:
a pseudo boolean constraint encoding that soft constraint.
Throws:
ContradictionException - if a trivial contradiction is found.
Since:
2.3

addSoftAtMost

public IConstr addSoftAtMost(BigInteger weight,
                             IVecInt literals,
                             int degree)
                      throws ContradictionException
Allow adding a new soft cardinality constraint in the solver.

Parameters:
weight - the weight of the constraint.
literals - the literals of the cardinality constraint.
degree - the degree of the cardinality constraint.
Returns:
a pseudo boolean constraint encoding that soft constraint.
Throws:
ContradictionException - if a trivial contradiction is found.
Since:
2.3

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.

reset

public void reset()
Specified by:
reset in interface ISolver
Overrides:
reset in class SolverDecorator<IPBSolver>

forceObjectiveValueTo

public void forceObjectiveValueTo(Number forcedValue)
                           throws ContradictionException
Throws:
ContradictionException


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