From 6cb1643a0d1848c1f8b3ce760aac1b34c4492541 Mon Sep 17 00:00:00 2001
From: Rouven Walter <rouven.walter@booleworks.com>
Date: Mon, 6 Feb 2023 09:45:42 +0100
Subject: [PATCH] added side effect note in SATSolver for assumption solving

---
 CHANGELOG.md                                  |  4 ++++
 .../java/org/logicng/solvers/SATSolver.java   | 24 +++++++++++++++++++
 2 files changed, 28 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index df47d769..163dd220 100644
--- a/CHANGELOG.md
+++ b/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. 
diff --git a/src/main/java/org/logicng/solvers/SATSolver.java b/src/main/java/org/logicng/solvers/SATSolver.java
index 5cd7c6d4..d3cd4348 100644
--- a/src/main/java/org/logicng/solvers/SATSolver.java
+++ b/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