Better management of forgotten variables for undo-based constraints
Sat4j allows to forget some variables during prime implicant computation. It performs that operation by falsifying both the positive and negative literal associated with a variable. It works fine for clauses and cardinality constraints. However, there is an issue for constraints requiring a call to undo when backtracking. The constraints to be considered when undoing an assignment is stored for a variable, not a literal. As such, when forgetting a variable, both the constraints where the positive and negative literal appears are part of that constraint. So a call to undo() on a constraint that does contains the literal will occur. Worst, it is necessary to perform the undo both on the literal and its oppositve in that case, to properly undo all constraints. In our testcases, the PB constraints are encoding the objective function and are deleted after each PI computation, so the current fix is simply to avoid a NPE that occurs when the undo() method is applied on a constraint not associated by such literal.
We are currently working on a new PI computation scheme, so that code with forget will eventually be removed. The current fix allows the solver to be correct, and prevents NPE to occur.