org.sat4j.tools

Class GroupClauseSelectorSolver<T extends ISolver>

java.lang.Object

org.sat4j.tools.SolverDecorator<T>

org.sat4j.tools.AbstractClauseSelectorSolver<T>

org.sat4j.tools.GroupClauseSelectorSolver<T>

All Implemented Interfaces:

Serializable, IGroupSolver, IProblem, ISolver, RandomAccessModel

Direct Known Subclasses:

HighLevelXplain

public class GroupClauseSelectorSolver<T extends ISolver>
extends AbstractClauseSelectorSolver<T>
implements IGroupSolver

See Also:

Serialized Form

Constructor Summary

Constructors

Constructor and Description
GroupClauseSelectorSolver(T solver)

Method Summary

Methods

Modifier and Type	Method and Description
IConstr	addClause(IVecInt literals, int desc)
IConstr	addControlableClause(IVecInt literals, int desc)
IConstr	addNonControlableClause(IVecInt literals)
Collection<Integer>	getAddedVars()
Map<Integer,Integer>	getVarToHighLevel()
int[]	model() Provide a model (if any) for a satisfiable formula.

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, addClause, 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, 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.ISolver

addAllClauses, addAtLeast, addAtMost, addBlockingClause, addClause, addExactly, clearLearntClauses, expireTimeout, getLogPrefix, getSearchListener, getSolvingEngine, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSolverKeptHot, isVerbose, modelWithInternalVariables, newVar, nextFreeVarId, printStat, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, toString, unsatExplanation

Methods inherited from interface org.sat4j.specs.IProblem

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

Methods inherited from interface org.sat4j.specs.RandomAccessModel

model

Constructor Detail

GroupClauseSelectorSolver

public GroupClauseSelectorSolver(T solver)

Method Detail

addControlableClause

public IConstr addControlableClause(IVecInt literals,
                           int desc)
                             throws ContradictionException

Throws:

ContradictionException

addNonControlableClause

public IConstr addNonControlableClause(IVecInt literals)
                                throws ContradictionException

Throws:

ContradictionException

addClause

public IConstr addClause(IVecInt literals,
                int desc)
                  throws ContradictionException

Specified by:

addClause in interface IGroupSolver

Parameters:

literals - a clause

desc - the level of the clause set

Returns:

on object representing that clause in the solver.

Throws:

ContradictionException

getAddedVars

public Collection<Integer> getAddedVars()

Specified by:

getAddedVars in class AbstractClauseSelectorSolver<T extends ISolver>

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)

getVarToHighLevel

public Map<Integer,Integer> getVarToHighLevel()