org.sat4j.tools

Class Minimal4InclusionModel

java.lang.Object

org.sat4j.tools.SolverDecorator<ISolver>

org.sat4j.tools.AbstractMinimalModel

org.sat4j.tools.Minimal4InclusionModel

All Implemented Interfaces:

Serializable, IProblem, ISolver, RandomAccessModel

public class Minimal4InclusionModel
extends AbstractMinimalModel

Computes models with a minimal subset (with respect to set inclusion) of negative literals. This is done be adding a clause containing the negation of the negative literals appearing in the model found (which prevents any interpretation containing that subset of negative literals to be a model of the formula). Computes only one model minimal for inclusion, since there is currently no way to save the state of the solver.

Author:

leberre

See Also:

ISolver.addClause(IVecInt), Serialized Form

Field Summary

Fields inherited from class org.sat4j.tools.AbstractMinimalModel

modelListener, pLiterals

Constructor Summary

Constructors

Constructor and Description
Minimal4InclusionModel(ISolver solver)
Minimal4InclusionModel(ISolver solver, IVecInt p)
Minimal4InclusionModel(ISolver solver, IVecInt p, SolutionFoundListener modelListener)

Method Summary

Methods

Modifier and Type	Method and Description
int[]	model() Provide a model (if any) for a satisfiable formula.
int[]	modelWithInternalVariables() That method is designed to be used to retrieve the real model of the current set of constraints, i.e. to provide the truth value of boolean variables used internally in the solver (for encoding purposes for instance).

Methods inherited from class org.sat4j.tools.AbstractMinimalModel

negativeLiterals, positiveLiterals

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

Constructor Detail

Minimal4InclusionModel

public Minimal4InclusionModel(ISolver solver,
                      IVecInt p,
                      SolutionFoundListener modelListener)

Parameters:

solver -

p - the set of literals on which the minimality for inclusion is computed.

modelListener - an object to be notified when a new model is found.

Minimal4InclusionModel

public Minimal4InclusionModel(ISolver solver,
                      IVecInt p)

Parameters:

solver -

p - the set of literals on which the minimality for inclusion is computed.

Minimal4InclusionModel

public Minimal4InclusionModel(ISolver solver)

Parameters:

solver -

Method Detail

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)

modelWithInternalVariables

public int[] modelWithInternalVariables()

Description copied from interface: ISolver

That method is designed to be used to retrieve the real model of the current set of constraints, i.e. to provide the truth value of boolean variables used internally in the solver (for encoding purposes for instance). If no variables are added in the solver, then Arrays.equals(model(),modelWithInternalVariables()). In case new variables are added to the solver, then the number of models returned by that method is greater of equal to the number of models returned by model() when using a ModelIterator.

Specified by:

modelWithInternalVariables in interface ISolver

Overrides:

modelWithInternalVariables in class SolverDecorator<ISolver>

Returns:

an array of literals, in Dimacs format, corresponding to a model of the formula over all the variables declared in the solver.

See Also:

IProblem.model(), ModelIterator