Merge pull request #137 from Mala1180/feature/tailrec-optimizations-p…

…ar-assignment

Feature/tailrec-optimizations-par-assignment

src/main/scala/satify/model/solver/PartialAssignment.scala

@@ -5,11 +5,13 @@ import satify.model.cnf.CNF.*
 import satify.model.solver.*
 import satify.model.{Assignment, Variable}
 
+import scala.annotation.tailrec
+
 /** Represents an [[Assignment]] where the variables could not be yet constrained by the DPLL algorithm.
   * @param optVariables optional variables.
   */
 case class PartialAssignment(optVariables: List[OptionalVariable]):
-  lazy val toAssignments: List[Assignment] = explodeAssignments(this)
+  lazy val toAssignments: List[Assignment] = explodeAssignments(this).distinct
 
   /** Cartesian product of all possible variable assignments to a partial assignment.
     * @param pa partial assignment
@@ -22,14 +24,14 @@ case class PartialAssignment(optVariables: List[OptionalVariable]):
           head match
             case OptionalVariable(name, None) =>
               if next.nonEmpty then
-                val assignments = PartialAssignment(next).toAssignments
+                val assignments = explodeAssignments(PartialAssignment(next))
                 assignments.flatMap { case Assignment(v) =>
                   Assignment(Variable(name, true) +: v) :: Assignment(Variable(name, false) +: v) :: Nil
                 }
               else Assignment(List(Variable(name, true))) :: Assignment(List(Variable(name, false))) :: Nil
             case v @ OptionalVariable(_, Some(_)) =>
               if next.nonEmpty then
-                PartialAssignment(next).toAssignments
+                explodeAssignments(PartialAssignment(next))
                   .map { case Assignment(variables) => Assignment(v.toVariable +: variables) }
               else List(Assignment(List(v.toVariable)))
         case Nil => Nil

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

@@ -26,20 +26,18 @@ private[dpll] object Optimizations:
     */
   def unitLiteralIdentification(cnf: CNF): Option[Constraint] =
 
-    val f: (CNF, Option[Constraint]) => Option[Constraint] =
-      (cnf, d) =>
-        cnf match
-          case Symbol(name: String) => Some(Constraint(name, true))
-          case Not(Symbol(name: String)) => Some(Constraint(name, false))
-          case _ => d
+    @tailrec
+    def loop(cnfList: List[CNF], result: Option[Constraint] = None): Option[Constraint] =
+      cnfList match
+        case Nil => result
+        case And(left, right) :: tail => loop(left :: right :: tail, None)
+        case head :: tail =>
+          head match
+            case Symbol(name: String) => Some(Constraint(name, true))
+            case Not(Symbol(name: String)) => Some(Constraint(name, false))
+            case _ => loop(tail, None)
 
-    f(
-      cnf,
-      cnf match
-        case And(left, right) => f(left, f(right, unitLiteralIdentification(right)))
-        case Or(_, _) => None
-        case _ => None
-    )
+    loop(cnf :: Nil)
 
   /** Identify a pure literal.
     * @param dec previous decision
@@ -51,36 +49,36 @@ private[dpll] object Optimizations:
 
     /** Get the literal type, if it is present inside the given CNF.
       * @param name of the symbol.
-      * @param cnf where to search.
+      * @param cnfList where to search.
       * @return a filled Option with the literal type if it is present, an empty one otherwise.
       */
-    def getLiteralType(name: String, cnf: CNF): Option[LitType] =
-
-      val recursiveStep: (String, CNF, CNF) => Option[LitType] = (n, left, right) =>
-        getLiteralType(n, left) match
-          case Some(Pure(cLeft)) =>
-            getLiteralType(n, right) match
-              case Some(Pure(cRight)) if cLeft == cRight => Some(Pure(cLeft))
-              case None => Some(Pure(cLeft))
-              case _ => Some(Impure)
-          case None => getLiteralType(n, right)
-          case impure @ _ => impure
-
-      cnf match
-        case Symbol(n: String) if name == n => Some(Pure(Constraint(n, true)))
-        case Not(Symbol(n: String)) if name == n => Some(Pure(Constraint(n, false)))
-        case And(left, right) => recursiveStep(name, left, right)
-        case Or(left, right) => recursiveStep(name, left, right)
-        case _ => None
+    @tailrec
+    def getLiteralType(name: String, cnfList: List[CNF], result: Option[LitType] = None): Option[LitType] =
+      cnfList match
+        case ::(head, tail) =>
+          head match
+            case Symbol(n: String) if name == n =>
+              result match
+                case Some(Pure(Constraint(_, false))) => Some(Impure)
+                case _ => getLiteralType(n, tail, Some(Pure(Constraint(n, true))))
+            case Not(Symbol(n: String)) if name == n =>
+              result match
+                case Some(Pure(Constraint(_, true))) => Some(Impure)
+                case _ => getLiteralType(n, tail, Some(Pure(Constraint(n, false))))
+            case And(left, right) => getLiteralType(name, left :: right :: tail, result)
+            case Or(left, right) => getLiteralType(name, left :: right :: tail, result)
+            case _ => getLiteralType(name, tail, result)
+        case Nil => result
 
     dec match
       case Decision(PartialAssignment(optVariables), cnf) =>
         optVariables match
-          case ::(head, next) =>
+          case ::(head, tail) =>
             head match
               case OptionalVariable(name, None) =>
-                getLiteralType(name, cnf) match
+                getLiteralType(name, cnf :: Nil) match
                   case Some(Pure(c)) => Some(c)
-                  case _ => pureLiteralIdentification(Decision(PartialAssignment(next), cnf))
-              case OptionalVariable(_, _) => pureLiteralIdentification(Decision(PartialAssignment(next), cnf))
+                  case _ => pureLiteralIdentification(Decision(PartialAssignment(tail), cnf))
+              case OptionalVariable(_, _) =>
+                pureLiteralIdentification(Decision(PartialAssignment(tail), cnf))
           case Nil => None

src/main/scala/satify/update/solver/dpll/cnf/CNFSat.scala

@@ -4,6 +4,8 @@ import satify.model.cnf.Bool.{False, True}
 import satify.model.cnf.CNF.{And, Not, Or, Symbol}
 import satify.model.cnf.{Bool, CNF}
 
+import scala.annotation.tailrec
+
 private[dpll] object CNFSat:
 
   /** Check if the given CNF is UNSAT.
@@ -12,25 +14,17 @@ private[dpll] object CNFSat:
     */
   def isUnsat(cnf: CNF): Boolean =
 
-    /** Returns true if CNF is a Symbol(False), d otherwise. */
-    val f: (CNF, Boolean) => Boolean = (cnf, d) =>
-      cnf match
-        case Symbol(False) => true
-        case _ => d
+    @tailrec
+    def loop(cnfList: List[CNF], result: Boolean = false): Boolean =
+      cnfList match
+        case Nil => result
+        case And(left, right) :: tail => loop(left :: right :: tail)
+        case head :: tail =>
+          head match
+            case Not(Symbol(True)) | Symbol(False) => true
+            case _ => loop(tail)
 
-    cnf match
-      case Not(Symbol(_: String)) | Symbol(_: String) | Not(Symbol(False)) | Symbol(True) | Or(_, _) => false
-      case Not(Symbol(True)) | Symbol(False) => true
-      case And(left, right) =>
-        f(
-          left,
-          f(
-            right,
-            if isUnsat(left) then true
-            else if isUnsat(right) then true
-            else false
-          )
-        )
+    loop(cnf :: Nil)
 
   /** Check if the given CNF is SAT.
     * @param cnf expression in Conjunctive Normal Form.

src/main/scala/satify/update/solver/dpll/cnf/CNFSimplification.scala

@@ -1,10 +1,12 @@
 package satify.update.solver.dpll.cnf
 
 import satify.model.cnf.Bool.{False, True}
-import satify.model.cnf.CNF
+import satify.model.cnf.{CNF, Literal}
 import satify.model.cnf.CNF.*
 import satify.model.solver.Constraint
 
+import scala.annotation.tailrec
+
 private[dpll] object CNFSimplification:
 
   /** Simplify the CNF applying the constraint given as parameter.
@@ -41,8 +43,7 @@ private[dpll] object CNFSimplification:
       ).asInstanceOf[T]
 
     (f(cnf, cnf) match
-      case And(left, right) =>
-        And(simplifyUppermostOr(left, constr), simplifyUppermostOr(right, constr))
+      case And(left, right) => And(simplifyUppermostOr(left, constr), simplifyUppermostOr(right, constr))
       case Or(left, right) =>
         /*
         1. Check if left branch is a True constant or the constrained Variable:

src/main/scala/satify/update/solver/dpll/impl/DpllFinder.scala

@@ -15,6 +15,7 @@ import satify.update.solver.dpll.cnf.CNFSimplification.simplifyCnf
 import satify.update.solver.dpll.impl.DpllFinder.{findNext, resume}
 import satify.update.solver.dpll.utils.PartialAssignmentUtils.*
 
+import scala.annotation.tailrec
 import scala.util.Random
 
 private[solver] object DpllFinder:
@@ -42,32 +43,40 @@ private[solver] object DpllFinder:
       case (_, UNSAT) => Solution(UNSAT, COMPLETED, Nil)
 
   /** Runs the DPLL algorithm resuming a previous run, if present.
+    *
     * @return an assignment, different from the previous ones, filled with a list
     *         of variables if there's another satisfiable, an empty list otherwise.
     */
+  @tailrec
   def findNext(): Option[Assignment] =
     prevRun match
-      case Some(DpllRun(dt, s)) =>
-        extractAssignment(dt, prevRun) match
+      case Some(DpllRun(prevDt, s @ Solution(SAT, PARTIAL, _))) =>
+        extractAssignment(prevDt, prevRun) match
           case None =>
-            resume(dt) match
+            resume(prevDt) match
               case (dt, SAT) =>
-                val optAssignment = extractAssignment(dt, prevRun)
-                optAssignment match
+                extractAssignment(dt, prevRun) match
                   case Some(assignment) =>
                     prevRun = Some(DpllRun(dt, Solution(SAT, PARTIAL, assignment +: s.assignments)))
-                  case _ =>
-                optAssignment
-              case (_, UNSAT) => None
+                    Some(assignment)
+                  case _ if dt != prevDt =>
+                    prevRun = Some(DpllRun(dt, s))
+                    findNext()
+                  case _ => None
+              case (dt, UNSAT) =>
+                prevRun = Some(DpllRun(dt, Solution(SAT, COMPLETED, s.assignments)))
+                None
           case optAssignment @ Some(assignment) =>
-            prevRun = Some(DpllRun(dt, Solution(SAT, PARTIAL, assignment +: s.assignments)))
+            prevRun = Some(DpllRun(prevDt, Solution(SAT, PARTIAL, assignment +: s.assignments)))
             optAssignment
+      case Some(_) => None
       case None => throw new NoSuchElementException("No previous instance of DPLL")
 
   /** Finder DPLL algorithm.
     * It returns a new decision tree with a new SAT leaf, if any.
     * Otherwise, the updated decision tree with all UNSAT leafs.
-    * @param d decision to be made
+    *
+    * @param d   decision to be made
     * @param rnd random number generator to make pseudo random decisions.
     * @return updated decision tree along with the result
     */
@@ -84,6 +93,7 @@ private[solver] object DpllFinder:
     else (Leaf(d), if isSat(d.cnf) then SAT else UNSAT)
 
   /** Resume the computation of DPLL given an existing instance of decision tree.
+    *
     * @param dt decision tree returned on the previous run.
     * @return the updated decision tree along with the new result.
     */
@@ -103,49 +113,16 @@ private[solver] object DpllFinder:
 
   /** Extract a new assignment from the decision tree s.t. it is not contained in the previous
     * DPLL run given in input.
-    * @param dt decision tree where to extract the assignment
+    *
+    * @param dt      decision tree where to extract the assignment
     * @param prevRun previous DPLL run with the current extracted solution.
     * @return a filled assignment if it exists, or an empty one.
     */
   private def extractAssignment(dt: DecisionTree, prevRun: Option[DpllRun]): Option[Assignment] =
-
-    /** Filter generated variables (from encodings / converter) and do the cartesian product
-      * of all the possible assignments
-      * @param pa partial assignment
-      * @return assignments
-      */
-    def filterAndExplore(pa: PartialAssignment): List[Assignment] = pa match
-      case PartialAssignment(optVariables) =>
-        PartialAssignment(
-          optVariables.filter(v =>
-            v match
-              case OptionalVariable(name, _)
-                  if name.startsWith(encodingVarPrefix) || name.startsWith(converterVarPrefix) =>
-                false
-              case _ => true
-          )
-        ).toAssignments
-
-    /** Returns the next assignment.
-      * @param assignments to filter
-      * @param prevRun filters assignments.
-      * @return a filled assignment from the list of [[assignments]] given in input s.t. it is
-      *        not containted in [[prevRun]], an empty one otherwise.
-      */
-    def nextAssignment(assignments: List[Assignment], prevRun: Option[DpllRun]): Option[Assignment] =
-      prevRun match
-        case Some(pr) =>
-          val newAssignments = assignments.filter(a => !(pr.s.assignments contains a))
-          if newAssignments.nonEmpty then Some(newAssignments.head) else None
-        case None if assignments.nonEmpty => Some(assignments.head)
-        case _ => None
-
-    dt match
-      case Leaf(Decision(s @ PartialAssignment(_), cnf)) =>
-        cnf match
-          case Symbol(True) => nextAssignment(filterAndExplore(s), prevRun)
-          case _ => None
-      case Branch(_, left, right) =>
-        extractAssignment(left, prevRun) match
-          case a @ Some(_) => a
-          case _ => extractAssignment(right, prevRun)
+    (for
+      pa <- extractParAssignments(dt)
+      assignment <- pa.toAssignments
+      if prevRun.fold(true)(run => !(run.s.assignments contains assignment))
+    yield assignment).distinct match
+      case ::(head, _) => Some(head)
+      case Nil => None