added side effect note in SATSolver for assumption solving

CHANGELOG.md

@@ -4,6 +4,10 @@ LogicNG uses [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
 ## [2.4.2] - 2023-xx-xx
 
+### Changed
+
+- Added side effect note in `SATSolver` for the four assumption solving methods. 
+
 ### Fixed
 
 - Fixed edge case in method `add(Formula formula, Proposition proposition)` in `MiniSat`. If a formula is added to the SAT solver, it can happen that a variable is not added to the solver because it was removed during the CNF transformation. A `model()` call or model enumeration will not produce models containing this variable since it was not added to the solver. The fix ensures that all variables of the original formula are added to the solver and thus, a found model includes the variable. 

src/main/java/org/logicng/solvers/SATSolver.java

@@ -234,6 +234,12 @@ public Tristate sat() {
     /**
      * Returns {@code Tristate.TRUE} if the current formula in the solver and a given literal are satisfiable,
      * {@code Tristate.FALSE} if it is unsatisfiable, or {@code UNDEF} if the solving process was aborted.
+     * <p>
+     * Side effect: Solving with assumptions adds the assumption literals as known variables to the solver if not already known.
+     * This change lasts beyond the assumption solving call and can have unintended results for subsequent solver calls.
+     * For example, a subsequent model enumeration call will produce models containing the now known variables.
+     * A reliable workaround for this side effect is to save the state of the solver with {@link #saveState()}
+     * and load the state of the solver after the assumption call(s) with {@link #loadState(SolverState)}.
      * @param literal the assumed literal
      * @return the satisfiability of the formula in the solver
      */
@@ -246,6 +252,12 @@ public Tristate sat(final Literal literal) {
      * are satisfiable, {@code Tristate.FALSE} if it is unsatisfiable, or {@code UNDEF} if the solving process was aborted.
      * The assumptions can be seen as an additional conjunction of literals.
      * Note: Use ordered collections to ensure determinism in the solving process and thus in the resulting model or conflict.
+     * <p>
+     * Side effect: Solving with assumptions adds the assumption literals as known variables to the solver if not already known.
+     * This change lasts beyond the assumption solving call and can have unintended results for subsequent solver calls.
+     * For example, a subsequent model enumeration call will produce models containing the now known variables.
+     * A reliable workaround for this side effect is to save the state of the solver with {@link #saveState()}
+     * and load the state of the solver after the assumption call(s) with {@link #loadState(SolverState)}.
      * @param assumptions a collection of literals
      * @return the satisfiability of the formula in the solver
      */
@@ -256,6 +268,12 @@ public Tristate sat(final Collection<? extends Literal> assumptions) {
     /**
      * Returns {@code Tristate.TRUE} if the current formula in the solver and a given literal are satisfiable,
      * {@code Tristate.FALSE} if it is unsatisfiable, or {@code UNDEF} if the solving process was aborted.
+     * <p>
+     * Side effect: Solving with assumptions adds the assumption literals as known variables to the solver if not already known.
+     * This change lasts beyond the assumption solving call and can have unintended results for subsequent solver calls.
+     * For example, a subsequent model enumeration call will produce models containing the now known variables.
+     * A reliable workaround for this side effect is to save the state of the solver with {@link #saveState()}
+     * and load the state of the solver after the assumption call(s) with {@link #loadState(SolverState)}.
      * @param handler the SAT handler
      * @param literal the assumed literal
      * @return the satisfiability of the formula in the solver
@@ -267,6 +285,12 @@ public Tristate sat(final Collection<? extends Literal> assumptions) {
      * are satisfiable, {@code Tristate.FALSE} if it is unsatisfiable, or {@code UNDEF} if the solving process was aborted.
      * The assumptions can be seen as an additional conjunction of literals.
      * Note: Use ordered collections to ensure determinism in the solving process and thus in the resulting model or conflict.
+     * <p>
+     * Side effect: Solving with assumptions adds the assumption literals as known variables to the solver if not already known.
+     * This change lasts beyond the assumption solving call and can have unintended results for subsequent solver calls.
+     * For example, a subsequent model enumeration call will produce models containing the now known variables.
+     * A reliable workaround for this side effect is to save the state of the solver with {@link #saveState()}
+     * and load the state of the solver after the assumption call(s) with {@link #loadState(SolverState)}.
      * @param handler     the SAT handler
      * @param assumptions a collection of literals
      * @return the satisfiability of the formula in the solver