org.sat4j.opt

Class AbstractSelectorVariablesDecorator

java.lang.Object

org.sat4j.tools.SolverDecorator<ISolver>

org.sat4j.opt.AbstractSelectorVariablesDecorator

All Implemented Interfaces:

Serializable, IOptimizationProblem, IProblem, ISolver, RandomAccessModel

Direct Known Subclasses:

MaxSatDecorator

public abstract class AbstractSelectorVariablesDecorator
extends SolverDecorator<ISolver>
implements IOptimizationProblem

Abstract class which adds a new "selector" variable for each clause entered in the solver. As a consequence, an original problem with n variables and m clauses will end up with n+m variables.

Author:

daniel

See Also:

Serialized Form

Constructor Summary

Constructors

Constructor and Description
AbstractSelectorVariablesDecorator(ISolver solver)

Method Summary

Methods

Modifier and Type	Method and Description
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.
int	getExpectedNumberOfClauses()
int	getNbexpectedclauses()
boolean[]	getPrevboolmodel()
int[]	getPrevfullmodel()
int[]	getPrevmodel()
boolean	isOptimal() Allows to check afterwards if the solution provided by the solver is optimal or not.
boolean	isSolutionOptimal()
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.
void	setExpectedNumberOfClauses(int nb) To inform the solver of the expected number of clauses to read.
void	setNbexpectedclauses(int nbexpectedclauses)
void	setPrevboolmodel(boolean[] prevboolmodel)
void	setPrevfullmodel(int[] prevfullmodel)
void	setPrevmodel(int[] prevmodel)
void	setSolutionOptimal(boolean isSolutionOptimal)

Methods inherited from class org.sat4j.tools.SolverDecorator

addAllClauses, addAtLeast, addAtMost, addBlockingClause, addClause, addExactly, clearDecorated, clearLearntClauses, decorated, expireTimeout, findModel, findModel, getLogPrefix, getSearchListener, getSolvingEngine, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, isSolverKeptHot, isVerbose, modelWithInternalVariables, nConstraints, newVar, newVar, nextFreeVarId, nVars, primeImplicant, primeImplicant, printInfos, printInfos, printStat, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, reset, 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.IOptimizationProblem

calculateObjective, discard, discardCurrentSolution, forceObjectiveValueTo, getObjectiveValue, hasNoObjectiveFunction, nonOptimalMeansSatisfiable, setTimeoutForFindingBetterSolution

Methods inherited from interface org.sat4j.specs.IProblem

findModel, findModel, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, nConstraints, newVar, nVars, primeImplicant, primeImplicant, printInfos, printInfos

Constructor Detail

AbstractSelectorVariablesDecorator

public AbstractSelectorVariablesDecorator(ISolver solver)

Method Detail

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

Parameters:

nb - the expected number of clauses.

See Also:

IProblem.newVar(int)

getExpectedNumberOfClauses

public int getExpectedNumberOfClauses()

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.

Since:

2.1

See Also:

ISolver.setTimeout(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<ISolver>

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: RandomAccessModel

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 RandomAccessModel

Overrides:

model in class SolverDecorator<ISolver>

Parameters:

var - the variable id in Dimacs format

Returns:

the truth value of that variable in the model

See Also:

#model()

isOptimal

public boolean isOptimal()

Description copied from interface: IOptimizationProblem

Allows to check afterwards if the solution provided by the solver is optimal or not.

Specified by:

isOptimal in interface IOptimizationProblem

Returns:

getNbexpectedclauses

public int getNbexpectedclauses()

setNbexpectedclauses

public void setNbexpectedclauses(int nbexpectedclauses)

getPrevfullmodel

public int[] getPrevfullmodel()

setPrevfullmodel

public void setPrevfullmodel(int[] prevfullmodel)

getPrevmodel

public int[] getPrevmodel()

setPrevmodel

public void setPrevmodel(int[] prevmodel)

getPrevboolmodel

public boolean[] getPrevboolmodel()

setPrevboolmodel

public void setPrevboolmodel(boolean[] prevboolmodel)

isSolutionOptimal

public boolean isSolutionOptimal()

setSolutionOptimal

public void setSolutionOptimal(boolean isSolutionOptimal)