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)
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).