Feature/next-sol-mechanism

src/main/scala/satify/update/Update.scala

@@ -118,13 +118,14 @@ object Update:
     * @return a state with the input, expression, and solution if no exception is thrown, otherwise a state with the error.
     */
   private def nextSolutionUpdate(currentState: State): State =
+    val nextAssignment: Assignment = Solver(DPLL).next()
     if currentState.problem.isDefined then
       safeUpdate(
         () =>
           State(
             Solution(
               currentState.solution.get.result,
-              currentState.solution.get.assignment.tail ::: List(currentState.solution.get.assignment.head)
+              nextAssignment :: currentState.solution.get.assignment
             ),
             currentState.problem.get
           ),
@@ -138,7 +139,9 @@ object Update:
             currentState.expression.get,
             Solution(
               currentState.solution.get.result,
-              currentState.solution.get.assignment.tail ::: List(currentState.solution.get.assignment.head)
+              nextAssignment match
+                case Assignment(Nil) => currentState.solution.get.assignment
+                case _ => nextAssignment :: currentState.solution.get.assignment
             )
           ),
         EmptySolution

src/main/scala/satify/update/solver/Solver.scala

@@ -2,12 +2,14 @@ package satify.update.solver
 
 import satify.model.Result.*
 import satify.model.cnf.CNF
+import satify.model.dpll.{DecisionTree, PartialModel}
 import satify.model.expression.Expression
 import satify.model.{Assignment, Solution}
 import satify.update.converters.ConverterType.*
 import satify.update.converters.{Converter, ConverterType}
 import satify.update.solver.SolverType.*
 import satify.update.solver.dpll.utils.DpllUtils.extractSolutions
+import satify.update.solver.dpll.DpllOneSol.dpll
 
 /** Entity providing the methods to solve the SAT problem.
   * @see [[satify.update.solver.DPLL]]
@@ -26,6 +28,12 @@ trait Solver:
     */
   def solve(exp: Expression): Solution
 
+  /** Finds the next assignment of the previous solution, if any.
+    * @return the solution to the SAT problem
+    * @throws IllegalStateException if the previous solution was not found
+    */
+  def next(): Assignment
+
   protected def memoize(f: CNF => Solution): CNF => Solution =
     new collection.mutable.HashMap[CNF, Solution]():
       override def apply(key: CNF): Solution = getOrElseUpdate(key, f(key))
@@ -44,11 +52,8 @@ object Solver:
 
   /** Private implementation of [[Solver]] */
   private case class DpllAlgorithm(converter: Converter) extends Solver:
-    override def solve(cnf: CNF): Solution = memoize(cnf =>
-      val s = extractSolutions(cnf)
-      s match
-        case _ if s.isEmpty => Solution(UNSAT)
-        case _ => Solution(SAT, s.map(Assignment.apply).toList)
-    )(cnf)
+    override def solve(cnf: CNF): Solution = memoize(cnf => dpll(cnf))(cnf)
 
     override def solve(exp: Expression): Solution = solve(converter.convert(exp))
+
+    override def next(): Assignment = dpll()

src/main/scala/satify/update/solver/dpll/Dpll.scala

@@ -1,21 +1,20 @@
 package satify.update.solver.dpll
 
 import satify.model.cnf.Bool.False
+import satify.model.cnf.CNF
 import satify.model.cnf.CNF.Symbol
 import satify.model.dpll.DecisionTree.{Branch, Leaf}
 import satify.model.dpll.{Constraint, Decision, DecisionTree, Variable}
+import satify.update.solver.dpll.DpllDecision.decide
 import satify.update.solver.dpll.cnf.CNFSimplification.simplifyCnf
 import satify.update.solver.dpll.cnf.CNFSat.{isSat, isUnsat}
-import satify.update.solver.dpll.Optimizations.{pureLiteralIdentification, unitLiteralIdentification}
-import satify.update.solver.dpll.utils.PartialModelUtils.*
+import satify.update.solver.dpll.utils.PartialModelUtils.extractModelFromCnf
 
-import java.util.concurrent.Executors
 import scala.annotation.tailrec
-import scala.util.Random
 
 object Dpll:
 
-  private val rnd = Random(64)
+  def dpll(cnf: CNF): DecisionTree = dpll(Decision(extractModelFromCnf(cnf), cnf))
 
   /** Main DPLL algorithm.
     * @param dec first decision
@@ -42,62 +41,3 @@ object Dpll:
       case Nil => throw new Error("Stack should never be empty")
 
     step(List(Frame(dec, Nil, decide(dec))))
-
-  /** Make decisions based on the previous one selecting the most appropriate variable and assignment.
-    * If no optimization can be applied, it makes a random decision.
-    * @param d previous decision.
-    * @return List of new Decisions
-    */
-  private def decide(d: Decision): List[Decision] = d match
-    case Decision(_, cnf) =>
-      unitLiteralIdentification(cnf) match
-        case Some(c) => unitPropagationDecision(d, c)
-        case _ =>
-          pureLiteralIdentification(d) match
-            case Some(c) => pureLiteralEliminationDecision(d, c)
-            case _ => randomDecisions(d)
-
-  /** Make random decisions based on the previous one given as parameter,
-    * by choosing a random variable assigning a random value to it.
-    * @param d previous decision
-    * @return List of new decisions
-    */
-  private def randomDecisions(d: Decision): List[Decision] = d match
-    case Decision(pm, cnf) =>
-      val fv = filterUnconstrVars(pm)
-      if fv.nonEmpty then
-        val v = rnd.nextBoolean()
-        fv(rnd.between(0, fv.size)) match
-          case Variable(n, _) =>
-            List(
-              Decision(updateParModel(pm, Constraint(n, v)), simplifyCnf(cnf, Constraint(n, v))),
-              Decision(updateParModel(pm, Constraint(n, !v)), simplifyCnf(cnf, Constraint(n, !v)))
-            )
-      else Nil
-
-  /** Make unit propagation decision based on the previous decision and the constraint provided.
-    * @param d previous decision.
-    * @param c constraint.
-    * @return List of new decisions
-    */
-  private def unitPropagationDecision(d: Decision, c: Constraint): List[Decision] =
-    d match
-      case Decision(pm, cnf) =>
-        List(
-          Decision(updateParModel(pm, c), simplifyCnf(cnf, c)),
-          Decision(updateParModel(pm, Constraint(c.name, !c.value)), Symbol(False))
-        )
-
-  /** Make pure literals elimination decisions based on the previous decision and the
-    * constraint provided.
-    * @param d previous decision.
-    * @param c constraint.
-    * @return List of new decisions
-    */
-  private def pureLiteralEliminationDecision(d: Decision, c: Constraint): List[Decision] =
-    d match
-      case Decision(pm, cnf) =>
-        List(
-          Decision(updateParModel(pm, c), simplifyCnf(cnf, c)),
-          Decision(updateParModel(pm, Constraint(c.name, !c.value)), simplifyCnf(cnf, Constraint(c.name, !c.value)))
-        )

src/main/scala/satify/update/solver/dpll/DpllDecision.scala

@@ -0,0 +1,79 @@
+package satify.update.solver.dpll
+
+import satify.model.cnf.Bool.False
+import satify.model.dpll.Variable
+import satify.model.cnf.CNF.Symbol
+import satify.model.dpll.{Constraint, Decision}
+import satify.update.solver.dpll.Optimizations.{pureLiteralIdentification, unitLiteralIdentification}
+import satify.update.solver.dpll.cnf.CNFSimplification.simplifyCnf
+import satify.update.solver.dpll.utils.PartialModelUtils.{filterUnconstrVars, updateParModel}
+
+import scala.util.Random
+
+object DpllDecision:
+
+  private val rnd = Random(42)
+
+  /** Make decisions based on the previous one selecting the most appropriate variable and assignment.
+    * If no optimization can be applied, it makes a random decision.
+    *
+    * @param d previous decision.
+    * @return List of new Decisions
+    */
+  def decide(d: Decision): List[Decision] = d match
+    case Decision(_, cnf) =>
+      unitLiteralIdentification(cnf) match
+        case Some(c) => unitPropagationDecision(d, c)
+        case _ =>
+          pureLiteralIdentification(d) match
+            case Some(c) =>
+              pureLiteralEliminationDecision(d, c)
+            case _ => randomDecisions(d)
+
+  /** Make random decisions based on the previous one given as parameter,
+    * by choosing a random variable assigning a random value to it.
+    *
+    * @param d previous decision
+    * @return List of new decisions
+    */
+  def randomDecisions(d: Decision): List[Decision] = d match
+    case Decision(pm, cnf) =>
+      val fv = filterUnconstrVars(pm)
+      if fv.nonEmpty then
+        val v = rnd.nextBoolean()
+        fv(rnd.between(0, fv.size)) match
+          case Variable(n, _) =>
+            List(
+              Decision(updateParModel(pm, Constraint(n, v)), simplifyCnf(cnf, Constraint(n, v))),
+              Decision(updateParModel(pm, Constraint(n, !v)), simplifyCnf(cnf, Constraint(n, !v)))
+            )
+      else Nil
+
+  /** Make unit propagation decision based on the previous decision and the constraint provided.
+    *
+    * @param d previous decision.
+    * @param c constraint.
+    * @return List of new decisions
+    */
+  def unitPropagationDecision(d: Decision, c: Constraint): List[Decision] =
+    d match
+      case Decision(pm, cnf) =>
+        List(
+          Decision(updateParModel(pm, c), simplifyCnf(cnf, c)),
+          Decision(updateParModel(pm, Constraint(c.name, !c.value)), Symbol(False))
+        )
+
+  /** Make pure literals elimination decisions based on the previous decision and the
+    * constraint provided.
+    *
+    * @param d previous decision.
+    * @param c constraint.
+    * @return List of new decisions
+    */
+  def pureLiteralEliminationDecision(d: Decision, c: Constraint): List[Decision] =
+    d match
+      case Decision(pm, cnf) =>
+        List(
+          Decision(updateParModel(pm, c), simplifyCnf(cnf, c)),
+          Decision(updateParModel(pm, Constraint(c.name, !c.value)), simplifyCnf(cnf, Constraint(c.name, !c.value)))
+        )

src/main/scala/satify/update/solver/dpll/DpllOneSol.scala

@@ -0,0 +1,98 @@
+package satify.update.solver.dpll
+
+import satify.model.{Assignment, Result, Solution}
+import satify.model.cnf.Bool.True
+import satify.model.cnf.CNF.*
+import satify.model.cnf.CNF
+import satify.model.Result.*
+import satify.model.dpll.{Constraint, Decision, DecisionTree, PartialModel, Variable}
+import satify.model.dpll.DecisionTree.{Branch, Leaf}
+import satify.update.solver.dpll.DpllDecision.decide
+import satify.update.solver.dpll.DpllOneSol.{dpll, resume}
+import satify.update.solver.dpll.cnf.CNFSat.{isSat, isUnsat}
+import satify.update.solver.dpll.cnf.CNFSimplification.simplifyCnf
+import satify.update.solver.dpll.utils.PartialModelUtils.*
+
+import scala.annotation.tailrec
+import scala.util.Random
+
+case class DpllRun(dt: DecisionTree, s: Solution)
+
+object DpllOneSol:
+
+  val rnd: Random = Random(42)
+  private var prevRun: Option[DpllRun] = None
+
+  def dpll(cnf: CNF): Solution =
+    buildTree(Decision(extractModelFromCnf(cnf), cnf)) match
+      case (dt, SAT) =>
+        val solution: Solution = Solution(SAT, List(extractSolution(dt, prevRun)))
+        prevRun = Some(DpllRun(dt, solution))
+        solution
+      case (_, UNSAT) => Solution(UNSAT, Nil)
+
+  def dpll(): Assignment =
+    prevRun match
+      case Some(DpllRun(dt, s)) =>
+        extractSolution(dt, prevRun) match
+          case Assignment(Nil) =>
+            resume(dt) match
+              case (dt, SAT) =>
+                val assignment: Assignment = extractSolution(dt, prevRun)
+                prevRun = Some(DpllRun(dt, Solution(SAT, assignment +: s.assignment)))
+                assignment
+              case (_, UNSAT) => Assignment(Nil)
+          case assignment @ _ =>
+            prevRun = Some(DpllRun(dt, Solution(SAT, assignment +: s.assignment)))
+            assignment
+      case None => throw new NoSuchElementException("No previous instance of DPLL")
+
+  def resume(dt: DecisionTree): (DecisionTree, Result) = dt match
+    case Leaf(d @ Decision(_, cnf)) =>
+      val checkUnsat = isUnsat(cnf)
+      val checkSat = isSat(cnf)
+      if !checkSat && !checkUnsat then buildTree(d)
+      else (dt, if checkSat then SAT else UNSAT)
+
+    case Branch(d, left, right) =>
+      resume(left) match
+        case (ldt, SAT) if ldt != left => (Branch(d, ldt, right), SAT)
+        case (ldt, lres) =>
+          resume(right) match
+            case (rdt, rres) => (Branch(d, ldt, rdt), if lres == SAT then SAT else rres)
+
+  private def buildTree(d: Decision): (DecisionTree, Result) =
+    if !isUnsat(d.cnf) && !isSat(d.cnf) then
+      decide(d) match
+        case ::(head, next) =>
+          buildTree(head) match
+            case (dtl, SAT) => (Branch(d, dtl, Leaf(next.head)), SAT)
+            case (dtl, UNSAT) =>
+              buildTree(next.head) match
+                case (dtr, res) => (Branch(d, dtl, dtr), res)
+        case Nil => (Leaf(d), if isSat(d.cnf) then SAT else UNSAT)
+    else (Leaf(d), if isSat(d.cnf) then SAT else UNSAT)
+
+  private def extractSolution(dt: DecisionTree, prevRun: Option[DpllRun]): Assignment =
+    dt match
+      case Leaf(Decision(pm, cnf)) =>
+        cnf match
+          case Symbol(True) =>
+            val allSolutions = explodeSolutions(
+              pm.filter(v =>
+                v match
+                  case Variable(name, _) if name.startsWith("ENC") || name.startsWith("TSTN") => false
+                  case _ => true
+              )
+            ).map(parModel => Assignment(parModel)).toList
+            prevRun match
+              case Some(pr) =>
+                val filteredList = allSolutions.filter(a => !(pr.s.assignment contains a))
+                if filteredList.nonEmpty then filteredList.head else Assignment(Nil)
+              case None if allSolutions.nonEmpty => allSolutions.head
+              case _ => Assignment(Nil)
+          case _ => Assignment(Nil)
+      case Branch(_, left, right) =>
+        extractSolution(left, prevRun) match
+          case s @ Assignment(l) if l.nonEmpty => s
+          case _ => extractSolution(right, prevRun)

src/main/scala/satify/update/solver/dpll/utils/DpllUtils.scala

@@ -9,6 +9,6 @@ object DpllUtils:
 
   def extractSolutions(cnf: CNF): Set[PartialModel] =
     val s =
-      for pmSet <- extractSolutionsFromDT(dpll(Decision(extractModelFromCnf(cnf), cnf)))
+      for pmSet <- extractSolutionsFromDT(dpll(cnf))
       yield explodeSolutions(pmSet)
     s.flatten

src/test/scala/satify/update/NextSolutionUpdateTest.scala

@@ -1,30 +1,27 @@
-package satify.update
+/*package satify.update
 
 import org.scalatest.flatspec.AnyFlatSpec
 import org.scalatest.matchers.should.Matchers
-import satify.model.State
+import satify.model.{Assignment, State}
 import satify.update.Message.*
 import satify.update.Update.update
 
 class NextSolutionUpdateTest extends AnyFlatSpec with Matchers:
 
-  /*  "When NextSolution message is sent to the update component it" should "return an updated State changing first solution assignment" in {
-    val multipleAssignmentsExpression: String = "a or b"
-    val currentState: State = update(State(), Solve(multipleAssignmentsExpression))
-    println(currentState)
-    val newState = update(currentState, NextSolution)
-    println(newState)
-    currentState.solution.get.assignment.head shouldNot be(newState.solution.get.assignment.head)
-  }
-
+  "When NextSolution message is sent to the update component it" should
+    "return an updated State changing first solution assignment" in {
+      val multipleAssignmentsExpression: String = "a or b"
+      val currentState: State = update(State(), Solve(multipleAssignmentsExpression))
+      val newState = update(currentState, NextSolution())
+      currentState.solution.get.assignment.head shouldNot be(newState.solution.get.assignment.head)
+    }
 
-  "When NextSolution message is sent but only one assigment is possible it" should "return the same solution assignment" in {
-    val singleAssignmentsExpression: String = "a and b"
-    val currentState: State = update(State(), Solve(singleAssignmentsExpression))
-    val newState = update(currentState, NextSolution)
-    println(newState)
-    currentState.solution.get.assignment.head should be(newState.solution.get.assignment.head)
-  }*/
+  "When NextSolution message is sent but only one assigment is possible it" should
+    "return an empty assignment" in {
+      val singleAssignmentsExpression: String = "a and b"
+      val currentState: State = update(State(), Solve(singleAssignmentsExpression))
+      currentState.solution.get.assignment.head should be(Assignment(Nil))
+    }
 
   "When NextSolution message is sent but no solution are present it" should "return an Error" in {
     val newState = update(State(), NextSolution())
@@ -36,3 +33,4 @@ class NextSolutionUpdateTest extends AnyFlatSpec with Matchers:
     && problem.isEmpty
     && error.isDefined shouldBe true
   }
+ */