Logo Search packages:      
Sourcecode: sat4j version File versions

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

Create a cardinality constraint of the type "at most 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 it contains more than degree satisfied literals after unit propagation
See also:
removeConstr(IConstr)

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

Definition at line 327 of file Solver.java.

References org::sat4j::specs::IVecInt::push().

                                                {
            int n = literals.size();
            IVecInt opliterals = new VecInt(n);
            for (IteratorInt iterator = literals.iterator(); iterator.hasNext();) {
                  opliterals.push(-iterator.next());
            }
            return addAtLeast(opliterals, n - degree);
      }


Generated by  Doxygen 1.6.0   Back to index