Trivial inconsistency in cardinality constraints not properly handled
When doing optimization with cardinality constraints (at least), at some point the degree of the constraint is strictly bigger than the number of literals in the constraints. In that case, the constraint cannot be satisfied: x& + x2 + x3 >= 4 cannot be satisfied. As such, sat4j should throw a ContradictionException when that constraint is created. While it is the case in the AtLeast implementation of the card constraint, it is not the case for MaxWatchPb and MinWatchPb.