org.sat4j.tools

Class FullClauseSelectorSolver<T extends ISolver>

java.lang.Object

org.sat4j.tools.SolverDecorator<T>

org.sat4j.tools.AbstractClauseSelectorSolver<T>

org.sat4j.tools.FullClauseSelectorSolver<T>

All Implemented Interfaces:

Serializable, IProblem, ISolver, RandomAccessModel

Direct Known Subclasses:

Xplain

public class FullClauseSelectorSolver<T extends ISolver>
extends AbstractClauseSelectorSolver<T>

See Also:

Serialized Form

Constructor Summary

Constructors

Constructor and Description
FullClauseSelectorSolver(T solver, boolean skipDuplicatedEntries)

Method Summary

Methods

Modifier and Type	Method and Description
IConstr	addClause(IVecInt literals) Create a clause from a set of literals The literals are represented by non null integers such that opposite literals a represented by opposite values.
IConstr	addControlableClause(IVecInt literals)
IConstr	addNonControlableClause(IVecInt literals)
Collection<Integer>	getAddedVars()
Collection<IConstr>	getConstraints()
Map<Integer,IConstr>	getConstrs()
IVecInt	getLastClause()
IConstr	getLastConstr()
boolean	isSkipDuplicatedEntries()
int[]	model() Provide a model (if any) for a satisfiable formula.
void	setLastConstr(IConstr lastConstr)

Methods inherited from class org.sat4j.tools.AbstractClauseSelectorSolver

createNewVar, discardLastestVar, externalState, internalState, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable

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, isSolverKeptHot, isVerbose, 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

FullClauseSelectorSolver

public FullClauseSelectorSolver(T solver,
                        boolean skipDuplicatedEntries)

Method Detail

addControlableClause

public IConstr addControlableClause(IVecInt literals)
                             throws ContradictionException

Throws:

ContradictionException

addNonControlableClause

public IConstr addNonControlableClause(IVecInt literals)
                                throws ContradictionException

Throws:

ContradictionException

addClause

public IConstr addClause(IVecInt literals)
                  throws ContradictionException

Description copied from interface: ISolver

Create a clause from a set of literals The literals are represented by non null integers such that opposite literals a represented by opposite values. (classical Dimacs way of representing literals).

Specified by:

addClause in interface ISolver

Overrides:

addClause in class SolverDecorator<T extends ISolver>

Parameters:

literals - a set of literals

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:

ISolver.removeConstr(IConstr)

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

Returns:

a model of the formula as an array of literals to satisfy.

See Also:

IProblem.isSatisfiable(), IProblem.isSatisfiable(IVecInt)

getConstraints

public Collection<IConstr> getConstraints()

Since:

2.1

getAddedVars

public Collection<Integer> getAddedVars()

Specified by:

getAddedVars in class AbstractClauseSelectorSolver<T extends ISolver>

getLastConstr

public IConstr getLastConstr()

setLastConstr

public void setLastConstr(IConstr lastConstr)

getConstrs

public Map<Integer,IConstr> getConstrs()

getLastClause

public IVecInt getLastClause()

isSkipDuplicatedEntries

public boolean isSkipDuplicatedEntries()