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"

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:

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