public class Minimal4CardinalityModel extends AbstractMinimalModel
ISolver.addAtMost(IVecInt, int)
,
Serialized FormmodelListener, pLiterals
Constructor and Description |
---|
Minimal4CardinalityModel(ISolver solver) |
Minimal4CardinalityModel(ISolver solver,
IVecInt p) |
Minimal4CardinalityModel(ISolver solver,
IVecInt p,
SolutionFoundListener modelListener) |
Minimal4CardinalityModel(ISolver solver,
SolutionFoundListener modelListener) |
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.
|
negativeLiterals, positiveLiterals
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, setUnitClauseProvider, setVerbose, toString, toString, unsatExplanation
public Minimal4CardinalityModel(ISolver solver)
solver
- public Minimal4CardinalityModel(ISolver solver, IVecInt p, SolutionFoundListener modelListener)
public Minimal4CardinalityModel(ISolver solver, SolutionFoundListener modelListener)
public int[] model()
IProblem
model
in interface IProblem
model
in class SolverDecorator<ISolver>
IProblem.isSatisfiable()
,
IProblem.isSatisfiable(IVecInt)
public int[] modelWithInternalVariables()
ISolver
modelWithInternalVariables
in interface ISolver
modelWithInternalVariables
in class SolverDecorator<ISolver>
IProblem.model()
,
ModelIterator