Create a cardinality constraint of the type "at least n of those literals must be satisfied"
|literals ||a set of literals. The vector can be reused since the solver is not supposed to keep a reference to that vector. |
|degree ||the degree of the cardinality constraint |
- a reference to the constraint added in the solver, to use in removeConstr().
|ContradictionException ||iff the vector of literals is empty or if degree literals are not remaining unfalsified after unit propagation |
- See also:
Definition at line 337 of file Solver.java.
IVecInt vlits = dimacs2internal(literals);
return addConstr(dsfactory.createCardinalityConstraint(vlits, degree));