Allow the solver to decide on a subset of the variables
In some cases, it is necessary to force the solver to decide on a subset of the variables. This can be done for checking that a set of variables constitutes a backdoor set for instance.
Adding that feature in Sat4j should not be a problem if the restriction is applied to the heuristics (IOrder subclass).
The main changes required for that are:
- Add a new IOrder subclass that allows the end user to specific a subset of the variables to choose from
- Ask the solver to return UNKNOWN when no variables can be selected for branching.