org.sat4j.tools
Class OptToSatAdapter

java.lang.Object
  extended by org.sat4j.tools.SolverDecorator<ISolver>
      extended by org.sat4j.tools.OptToSatAdapter
All Implemented Interfaces:
Serializable, IProblem, ISolver

public class OptToSatAdapter
extends SolverDecorator<ISolver>

See Also:
Serialized Form

Constructor Summary
OptToSatAdapter(IOptimizationProblem problem)
           
 
Method Summary
 boolean isOptimal()
          Allow to easily check is the solution returned by isSatisfiable is optimal or not.
 boolean isSatisfiable()
          Check the satisfiability of the set of constraints contained inside the solver.
 boolean isSatisfiable(boolean global)
          Check the satisfiability of the set of constraints contained inside the solver.
 boolean isSatisfiable(IVecInt assumps)
          Check the satisfiability of the set of constraints contained inside the solver.
 boolean isSatisfiable(IVecInt assumps, boolean global)
          Check the satisfiability of the set of constraints contained inside the solver.
 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 reset()
          Clean up the internal state of the solver.
 String toString(String prefix)
          Display a textual representation of the solver configuration.
 
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, isSolverKeptHot, isVerbose, modelWithInternalVariables, nConstraints, newVar, newVar, nextFreeVarId, nVars, primeImplicant, primeImplicant, printInfos, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, toString, unsatExplanation
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Constructor Detail

OptToSatAdapter

public OptToSatAdapter(IOptimizationProblem problem)
Method Detail

isSatisfiable

public boolean isSatisfiable()
                      throws TimeoutException
Description copied from interface: IProblem
Check the satisfiability of the set of constraints contained inside the solver.

Specified by:
isSatisfiable in interface IProblem
Overrides:
isSatisfiable in class SolverDecorator<ISolver>
Returns:
true if the set of constraints is satisfiable, else false.
Throws:
TimeoutException

reset

public void reset()
Description copied from interface: ISolver
Clean up the internal state of the solver.

Specified by:
reset in interface ISolver
Overrides:
reset in class SolverDecorator<ISolver>

isSatisfiable

public boolean isSatisfiable(boolean global)
                      throws TimeoutException
Description copied from interface: IProblem
Check the satisfiability of the set of constraints contained inside the solver.

Specified by:
isSatisfiable in interface IProblem
Overrides:
isSatisfiable in class SolverDecorator<ISolver>
Parameters:
global - whether that call is part of a global process (i.e. optimization) or not. if (global), the timeout will not be reset between each call.
Returns:
true if the set of constraints is satisfiable, else false.
Throws:
TimeoutException

isSatisfiable

public boolean isSatisfiable(IVecInt assumps,
                             boolean global)
                      throws TimeoutException
Description copied from interface: IProblem
Check the satisfiability of the set of constraints contained inside the solver.

Specified by:
isSatisfiable in interface IProblem
Overrides:
isSatisfiable in class SolverDecorator<ISolver>
Parameters:
assumps - a set of literals (represented by usual non null integers in Dimacs format).
global - whether that call is part of a global process (i.e. optimization) or not. if (global), the timeout will not be reset between each call.
Returns:
true if the set of constraints is satisfiable when literals are satisfied, else false.
Throws:
TimeoutException

isSatisfiable

public boolean isSatisfiable(IVecInt assumps)
                      throws TimeoutException
Description copied from interface: IProblem
Check the satisfiability of the set of constraints contained inside the solver.

Specified by:
isSatisfiable in interface IProblem
Overrides:
isSatisfiable in class SolverDecorator<ISolver>
Parameters:
assumps - a set of literals (represented by usual non null integers in Dimacs format).
Returns:
true if the set of constraints is satisfiable when literals are satisfied, else false.
Throws:
TimeoutException

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

toString

public String toString(String prefix)
Description copied from interface: ISolver
Display a textual representation of the solver configuration.

Specified by:
toString in interface ISolver
Overrides:
toString in class SolverDecorator<ISolver>
Parameters:
prefix - the prefix to use on each line.
Returns:
a textual description of the solver internals.

isOptimal

public boolean isOptimal()
Allow to easily check is the solution returned by isSatisfiable is optimal or not.

Returns:
true is the solution found is indeed optimal.


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