Class Minimal4CardinalityModel

  extended by
      extended by
All Implemented Interfaces:, IProblem, ISolver

public class Minimal4CardinalityModel
extends SolverDecorator

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).

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
addAllClauses, addAtLeast, addAtMost, addClause, addPseudoBoolean, decorated, getStat, getTimeout, isSatisfiable, isSatisfiable, model, nConstraints, newVar, newVar, nVars, printStat, printStat, removeConstr, reset, setExpectedNumberOfClauses, setTimeout, toString
Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail


public Minimal4CardinalityModel(ISolver solver)
solver -
Method Detail


public int[] model()
Description copied from interface: IProblem
Provide a model (if any) for a satisfiable formula. That method should be called AFTER isSatisfiable() if the formula is satisfiable. Else an exception UnsupportedOperationException is launched.

Specified by:
model in interface IProblem
model in class SolverDecorator
a model of the formula as an array of literals to satisfy.