org.sat4j.tools
Class Minimal4CardinalityModel

java.lang.Object
  org.sat4j.tools.SolverDecorator<ISolver>
      org.sat4j.tools.Minimal4CardinalityModel

All Implemented Interfaces:

Serializable, IProblem, ISolver

public class Minimal4CardinalityModel
extends SolverDecorator<ISolver>

Computes models with a minimal number (with respect to cardinality) of negative literals. This is done be adding a constraint on the number of negative literals each time a model if found (the number of negative literals occuring in the model minus one).

Author:

leberre

See Also:

ISolver.addAtMost(IVecInt, int), Serialized Form

Constructor Summary

Minimal4CardinalityModel(ISolver solver)

Method Summary

int[]

model() Provide a model (if any) for a satisfiable formula.

Methods inherited from class org.sat4j.tools.SolverDecorator

addAllClauses, addAtLeast, addAtMost, addBlockingClause, addClause, addExactly, clearDecorated, clearLearntClauses, decorated, expireTimeout, findModel, findModel, getLogPrefix, getSearchListener, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, isSolverKeptHot, isVerbose, model, modelWithInternalVariables, nConstraints, newVar, newVar, nextFreeVarId, nVars, primeImplicant, primeImplicant, printInfos, 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

Minimal4CardinalityModel

public Minimal4CardinalityModel(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)