Support for unconstrained decision variables in rustsat

[Shikhar-Srivastava-16]

The adaptation process for building SAT models does not currently support unconstrained variables, such as:

find a : bool

As far as I can tell at the moment, there is no way to do this using only rustsat. Of course, it is possible there is a way to do so and I just haven't found it. If there is, please let me know so that I can update the codebase.

In case there is indeed no way to do this, we can accomplish this using a rewriting rule which accomplishes the following type of change:

for example, this:

find a : bool

becomes this:

find a : bool
such that (a \/ !a)

[niklasdewally]

One possibility: you call RustSAT for a single solution, then for each DontCare or unconstrained variable in the output, you iterate through the possible assignments for those variables, giving the user a new solution for each one.

Once you've exhausted those, then you run rustsat again.