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"

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 it contains more than degree satisfied literals after unit propagation
See also:

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();) {
            return addAtLeast(opliterals, n - degree);

Generated by  Doxygen 1.6.0   Back to index