Do not freeze new variables by default

[Lipen]

Do not freeze new variables created via JMiniSat::newVar (and similar in JGlucose).

What's the case?

• "Not frozen" ("melted", in Cadical's terms) variables can be eliminated during the resolution, which in most cases greatly speeds up the solving process. In return, the programmer is responsible NOT TO "use" them in new clauses when solving incrementally, i.e. "do not add new clauses containing the eliminated variables after calling solve()". Note that this also includes "solving under assumptions" (because assumptions are, in fact, just "revertible" unit clauses), i.e. "do not use eliminated variables as assumptions when calling solve(assumptions)". Usage of eliminated variables may (and probably will) result in spurious SATs (i.e. the solver can produce the SAT result with a weird model, even when the problem is UNSAT).
• On the other hand, "frozen" variables are not eliminated (see "variable elimination" technique) by a SAT solver. If you are planning of adding new clauses incrementally (or using assumptions), you have to freeze all involved variables before calling solve(). Note that you can "melt" (via setFrozen(false)) them afterwards, when you are done "using" them.

Current behavior

Currently, kotlin-satlib tries to be maximally safe by default — it just freezes all new variables created via JMiniSat::newVar(). Maybe this is a sane default, but it also hits hard on performance, because the user is not capable of passing freeze=false in newVar() via the generic Solver interface, and is forced to live with everything frozen.
The same story can be said about the decision=true default argument, but this is less intrusive.

What we can/should do?

We should either change the default behavior to not freeze new vars (note that this IS the default behavior of any native solver) and force programmers to perform manual freezing of variables (I tend to think that this is preferable), or we need to provide a convenient generic interface for customizing variable creation (e.g., add overloads in MiniSatSolver interface, if not possible to lift it up to the Solver directly).