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

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

Fields

Modifier and Type	Field and Description
protected int	nbnewvar
static BigInteger	SAT4J_MAX_BIG_INTEGER
protected BigInteger	top

Constructor Summary

Constructors

Constructor and Description
WeightedMaxSatDecorator(IPBSolver solver)
WeightedMaxSatDecorator(IPBSolver solver, boolean equivalence)

Method Summary

Methods

Modifier and Type	Method and Description
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.
protected void	checkMaxVarId()
void	forceObjectiveValueTo(Number forcedValue) Force the solver to find a solution with a specific value (nice to find all optimal solutions for instance).
Set<Integer>	getUnitClauses() Returns the set of unit clauses added to the solver.
boolean	isNoNewVarForUnitSoftClauses() Returns true if no new variable should be created when adding a soft unit clause, false otherwise.
int	newVar(int howmany) Declare howmany variables in the problem (and thus in the vocabulary), that will be represented using the Dimacs format by integers ranging from 1 to howmany.
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	setNoNewVarForUnitSoftClauses(boolean noNewVarForUnitSoftClauses) Sets whether new variables should be created when adding new clauses.
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, getSolvingEngine, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, isSolverKeptHot, isVerbose, model, model, modelWithInternalVariables, nConstraints, newVar, nextFreeVarId, nVars, primeImplicant, primeImplicant, printInfos, printInfos, printStat, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, setDBSimplificationAllowed, setKeepSolverHot, 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, getSolvingEngine, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSolverKeptHot, isVerbose, modelWithInternalVariables, newVar, nextFreeVarId, printStat, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, setDBSimplificationAllowed, setKeepSolverHot, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, toString, unsatExplanation

Methods inherited from interface org.sat4j.specs.IProblem

findModel, findModel, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, nConstraints, nVars, primeImplicant, primeImplicant, printInfos, printInfos

Methods inherited from interface org.sat4j.specs.RandomAccessModel

model

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)

WeightedMaxSatDecorator

public WeightedMaxSatDecorator(IPBSolver solver,
                       boolean equivalence)

Method Detail

newVar

public int newVar(int howmany)

Description copied from interface: IProblem

Declare howmany variables in the problem (and thus in the vocabulary), that will be represented using the Dimacs format by integers ranging from 1 to howmany. That feature allows encodings to create additional variables with identifier starting at howmany+1.

Specified by:

newVar in interface IProblem

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)

See Also:

IProblem.nVars()

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:

IProblem.newVar(int)

setTopWeight

public void setTopWeight(BigInteger top)

checkMaxVarId

protected void checkMaxVarId()

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.

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

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()

Description copied from interface: ISolver

Clean up the internal state of the solver. Note that such method should also be called when you no longer need the solver because the state of the solver may prevent the GC to proceed. There is a known issue for instance where failing to call reset() on a solver will keep timer threads alive and exhausts memory.

Specified by:

reset in interface ISolver

Overrides:

reset in class SolverDecorator<IPBSolver>

forceObjectiveValueTo

public void forceObjectiveValueTo(Number forcedValue)
                           throws ContradictionException

Force the solver to find a solution with a specific value (nice to find all optimal solutions for instance).

Parameters:

forcedValue - the expected value of the solution

Throws:

ContradictionException - if that value is trivially not possible.

getUnitClauses

public Set<Integer> getUnitClauses()

Returns the set of unit clauses added to the solver.

isNoNewVarForUnitSoftClauses

public boolean isNoNewVarForUnitSoftClauses()

Returns true if no new variable should be created when adding a soft unit clause, false otherwise. By default, this is set to true.

Returns:

setNoNewVarForUnitSoftClauses

public void setNoNewVarForUnitSoftClauses(boolean noNewVarForUnitSoftClauses)

Sets whether new variables should be created when adding new clauses. By default, this is set to true. This can be useful when computing all muses.

Parameters:

noNewVarForUnitSoftClauses -