org.sat4j.opt
Class AbstractSelectorVariablesDecorator

java.lang.Object
  extended by org.sat4j.tools.SolverDecorator<ISolver>
      extended by org.sat4j.opt.AbstractSelectorVariablesDecorator
All Implemented Interfaces:
Serializable, IOptimizationProblem, IProblem, ISolver
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

Field Summary
protected  boolean isSolutionOptimal
           
protected  boolean[] prevboolmodel
           
protected  int[] prevfullmodel
           
protected  int[] prevmodel
           
 
Constructor Summary
AbstractSelectorVariablesDecorator(ISolver solver)
           
 
Method Summary
 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()
           
 boolean isOptimal()
          Allows to check afterwards if the solution provided by the solver is optimal or not.
 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.
 
Methods inherited from class org.sat4j.tools.SolverDecorator
addAllClauses, addAtLeast, addAtMost, addBlockingClause, addClause, addExactly, clearDecorated, clearLearntClauses, decorated, expireTimeout, findModel, findModel, getLogPrefix, getSearchListener, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, isVerbose, modelWithInternalVariables, nConstraints, newVar, newVar, nextFreeVarId, nVars, primeImplicant, printInfos, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, reset, 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.IOptimizationProblem
calculateObjective, discard, discardCurrentSolution, forceObjectiveValueTo, getObjectiveValue, hasNoObjectiveFunction, nonOptimalMeansSatisfiable
 
Methods inherited from interface org.sat4j.specs.IProblem
findModel, findModel, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, nConstraints, newVar, nVars, primeImplicant, printInfos
 

Field Detail

prevfullmodel

protected int[] prevfullmodel

prevmodel

protected int[] prevmodel
Since:
2.1

prevboolmodel

protected boolean[] prevboolmodel
Since:
2.1

isSolutionOptimal

protected boolean isSolutionOptimal
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: IProblem
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 IProblem
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:
IProblem.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:


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