Obvious variable substitution preprocessor.

[lvella]

For satisfiability applications, maintaining the number of variables is not important as long as the problem is equivalent. In such case, reducing the number of variables might increase the execution speed of the solver.

Pending issue #2, as a preprocessing step, it might help to perform the trivial variable substitution in the cases where ax + by = 0, where a and b are constants and y is a variable or a constant, so that every x can be rewritten by -by/a, thus eliminating x from the problem.