Logo Search packages:      
Sourcecode: sat4j version File versions

IConstr org::sat4j::minisat::core::Solver< L extends ILits, D extends DataStructureFactory< L >>::addAtLeast ( IVecInt  literals,
int  degree 
) throws ContradictionException [inline]

Create a cardinality constraint of the type "at least n of those literals must be satisfied"

Parameters:
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
Returns:
a reference to the constraint added in the solver, to use in removeConstr().
Exceptions:
ContradictionException iff the vector of literals is empty or if degree literals are not remaining unfalsified after unit propagation
See also:
removeConstr(IConstr)

Implements org::sat4j::specs::ISolver.

Definition at line 337 of file Solver.java.

                                                {
            IVecInt vlits = dimacs2internal(literals);
            return addConstr(dsfactory.createCardinalityConstraint(vlits, degree));
      }


Generated by  Doxygen 1.6.0   Back to index