org.sat4j.tools

Class AbstractClauseSelectorSolver<T extends ISolver>

java.lang.Object

org.sat4j.tools.SolverDecorator<T>

org.sat4j.tools.AbstractClauseSelectorSolver<T>

All Implemented Interfaces:

Serializable, IProblem, ISolver, RandomAccessModel

Direct Known Subclasses:

FullClauseSelectorSolver, GroupClauseSelectorSolver, NegationDecorator

public abstract class AbstractClauseSelectorSolver<T extends ISolver>
extends SolverDecorator<T>

See Also:

Serialized Form

Constructor Summary

Constructors

Constructor and Description
AbstractClauseSelectorSolver(T solver)

Method Summary

Methods

Modifier and Type	Method and Description
protected int	createNewVar(IVecInt literals)
protected void	discardLastestVar()
void	externalState() In external state, the solver will prevent the selector variables to be satisfied.
abstract Collection<Integer>	getAddedVars()
void	internalState() In the internal state, the solver will allow the selector variables to be satisfied.
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.

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, isSolverKeptHot, isVerbose, model, model, modelWithInternalVariables, nConstraints, newVar, newVar, nextFreeVarId, nVars, primeImplicant, primeImplicant, printInfos, printInfos, printStat, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setUnitClauseProvider, setVerbose, toString, toString, unsatExplanation

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Constructor Detail

AbstractClauseSelectorSolver

public AbstractClauseSelectorSolver(T solver)

Method Detail

getAddedVars

public abstract Collection<Integer> getAddedVars()

createNewVar

protected int createNewVar(IVecInt literals)

Parameters:

literals -

Returns:

Since:

2.1

discardLastestVar

protected void discardLastestVar()

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<T extends 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<T extends 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()
                      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<T extends ISolver>

Returns:

true if the set of constraints is satisfiable, 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<T extends 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

internalState

public void internalState()

In the internal state, the solver will allow the selector variables to be satisfied. As such, the solver will answer "true" to isSatisfiable() on an UNSAT problem. it is the responsibility of the user to take into account the meaning of the selector variables.

externalState

public void externalState()

In external state, the solver will prevent the selector variables to be satisfied. As a consequence, from an external point of view, an UNSAT problem will answer "false" to isSatisfiable().