Use a specific data structure to locate efficiently the weight associated to a literal in a counter based constraint
After checking the reason for inefficiency of Sat4j on specific benchmarks, it turns out that large counter based constraints have a bottleneck:
// finding the index for p in the array of literals int indiceP = 0; while ((lits[indiceP] ^ 1) != p) indiceP++;
Using an auxiliary array or map to store the location of the literals instead of going through that loop will probably make the propagation and undo much faster. (hint: use an array when the size of the constraint contains at least half of the variables, else use a map).