Investigate usage of plain CNF rather than custom cardinality of PB constraints
Sat4j uses by default a custom constraint for cardinality and PB constraints. The main advantage is to reduce the memory needed to represent the constraints. However, it requires ad hoc propagation and analysis procedure. Many solvers for solving MaxSat problems rely on cardinality of PB translation into SAT. It would be nice to be able to easily try in sat4j the effect of pure clausal encodings against current solution.