Feature/problems-nqueens

src/main/resources/cnf/nqueens3.txt

@@ -0,0 +1,37 @@
+c SAT Expression for N=3 queens
+c Chess board has 9 positions
+p cnf 9 34
+1 2 3 0
+-1 -2 0
+-1 -3 0
+-2 -3 0
+4 5 6 0
+-4 -5 0
+-4 -6 0
+-5 -6 0
+7 8 9 0
+-7 -8 0
+-7 -9 0
+-8 -9 0
+1 4 7 0
+-1 -4 0
+-1 -7 0
+-4 -7 0
+2 5 8 0
+-2 -5 0
+-2 -8 0
+-5 -8 0
+3 6 9 0
+-3 -6 0
+-3 -9 0
+-6 -9 0
+-4 -8 0
+-1 -5 0
+-1 -9 0
+-5 -9 0
+-2 -6 0
+-6 -8 0
+-3 -5 0
+-3 -7 0
+-5 -7 0
+-2 -4 0

src/main/resources/cnf/nqueens4.txt

@@ -0,0 +1,87 @@
+c SAT Expression for N=4 queens
+c Chess board has 16 positions
+p cnf 16 84
+1 2 3 4 0
+-1 -2 0
+-1 -3 0
+-1 -4 0
+-2 -3 0
+-2 -4 0
+-3 -4 0
+5 6 7 8 0
+-5 -6 0
+-5 -7 0
+-5 -8 0
+-6 -7 0
+-6 -8 0
+-7 -8 0
+9 10 11 12 0
+-9 -10 0
+-9 -11 0
+-9 -12 0
+-10 -11 0
+-10 -12 0
+-11 -12 0
+13 14 15 16 0
+-13 -14 0
+-13 -15 0
+-13 -16 0
+-14 -15 0
+-14 -16 0
+-15 -16 0
+1 5 9 13 0
+-1 -5 0
+-1 -9 0
+-1 -13 0
+-5 -9 0
+-5 -13 0
+-9 -13 0
+2 6 10 14 0
+-2 -6 0
+-2 -10 0
+-2 -14 0
+-6 -10 0
+-6 -14 0
+-10 -14 0
+3 7 11 15 0
+-3 -7 0
+-3 -11 0
+-3 -15 0
+-7 -11 0
+-7 -15 0
+-11 -15 0
+4 8 12 16 0
+-4 -8 0
+-4 -12 0
+-4 -16 0
+-8 -12 0
+-8 -16 0
+-12 -16 0
+-9 -14 0
+-5 -10 0
+-5 -15 0
+-10 -15 0
+-1 -6 0
+-1 -11 0
+-1 -16 0
+-6 -11 0
+-6 -16 0
+-11 -16 0
+-2 -7 0
+-2 -12 0
+-7 -12 0
+-3 -8 0
+-12 -15 0
+-8 -11 0
+-8 -14 0
+-11 -14 0
+-4 -7 0
+-4 -10 0
+-4 -13 0
+-7 -10 0
+-7 -13 0
+-10 -13 0
+-3 -6 0
+-3 -9 0
+-6 -9 0
+-2 -5 0

src/main/scala/satify/dsl/Conversion.scala

@@ -1,6 +1,6 @@
 package satify.dsl
 
-import satify.model.Expression.Symbol
+import satify.model.expression.Expression.Symbol
 object Conversion:
 
   given Conversion[String, Symbol] with

src/main/scala/satify/dsl/DSL.scala

@@ -1,7 +1,7 @@
 package satify.dsl
 
 object DSL:
-  export satify.dsl.Conversion.given
-  export satify.dsl.Operators.*
-  export satify.dsl.Numbers.*
-  export satify.dsl.SatEncodings.*
+  export Conversion.given
+  export Operators.*
+  export Numbers.*
+  export Encodings.*

src/main/scala/satify/dsl/Encodings.scala

@@ -0,0 +1,29 @@
+package satify.dsl
+
+import satify.model.expression.Expression
+import satify.model.expression.Expression.*
+
+object Encodings:
+
+  /** Converts a tuple to a list of [[Symbol]]
+    * @param tuple the input [[Tuple]]
+    * @return the list of [[Symbol]]
+    */
+  private def tupleToSymbols(tuple: Tuple): List[Symbol] =
+    tuple.productIterator.toList.map(_.toString).map(Symbol.apply)
+
+  extension (expressions: Tuple)
+
+    /** Calls [[atMostOne]] if k is 1, [[atMostK]] otherwise.
+      * @see [[atMostOne]] and [[atMostK]]
+      */
+    def atMost(k: Int): Expression = k match
+      case 1 => atMostOne(tupleToSymbols(expressions): _*)
+      case _ => atMostK(k)(tupleToSymbols(expressions): _*)
+
+    /** Calls [[atLeastOne]] if k is 1, [[atLeastK]] otherwise.
+      * @see [[atLeastOne]] and [[atLeastK]]
+      */
+    def atLeast(k: Int): Expression = k match
+      case 1 => atLeastOne(tupleToSymbols(expressions): _*)
+      case _ => atLeastK(k)(tupleToSymbols(expressions): _*)

src/main/scala/satify/dsl/Operators.scala

@@ -1,6 +1,7 @@
 package satify.dsl
-import satify.model.Expression
-import satify.model.Expression.*
+
+import satify.model.expression.Expression
+import satify.model.expression.Expression.*
 
 import scala.annotation.targetName
 

src/main/scala/satify/dsl/Reflection.scala

@@ -1,13 +1,13 @@
 package satify.dsl
 
-import satify.model.Expression
-import satify.model.Expression.Symbol
+import satify.model.expression.Expression
+import satify.model.expression.Expression.Symbol
 
 object Reflection:
 
   private def getDSLKeywords: List[String] =
     val operators = classOf[Operators.type].getMethods.map(_.getName).toList
-    val encodings = classOf[SatEncodings.type].getMethods.map(_.getName).toList
+    val encodings = classOf[Encodings.type].getMethods.map(_.getName).toList
     val numbers = classOf[Numbers.type].getMethods.map(_.getName).toList
     val objectMethods = classOf[Object].getMethods.map(_.getName).toList
     (operators ::: encodings ::: numbers).filterNot(objectMethods.contains(_))

src/main/scala/satify/model/State.scala

@@ -1,9 +1,13 @@
 package satify.model
 
+import satify.model
+import satify.model.expression.Expression
+import satify.model.problems.Problem
+
 /** The immutable entity representing the application state (Model). */
 trait State:
   /** A general expression of boolean logic, it is the user input */
-  type Expression = satify.model.Expression
+  type Expression = satify.model.expression.Expression
   val expression: Option[Expression] = None
 
   /** The input expression converted to Conjunctive Normal Form (CNF) */
@@ -15,7 +19,7 @@ trait State:
   val solution: Option[Solution] = None
 
   /** An entity representing the problem to solve */
-  type Problem = satify.model.Problem
+  type Problem = problems.Problem
   val problem: Option[Problem] = None
 
 /** Factory for [[State]] instances. */

src/main/scala/satify/dsl/SatEncodings.scala → src/main/scala/satify/model/expression/Encodings.scala

@@ -1,10 +1,9 @@
-package satify.dsl
+package satify.model.expression
 
-import satify.dsl.DSL.*
-import satify.model.Expression
-import satify.model.Expression.*
+import satify.model.expression.Expression.{And, Not, Or, Symbol}
+import satify.model.expression.Utils.symbolGenerator
 
-object SatEncodings:
+object Encodings:
 
   private def requireVariables(vars: Seq[Symbol], minimum: Int, method: String): Unit =
     require(vars.length >= minimum, s"$method encoding requires at least two variables")
@@ -13,16 +12,18 @@ object SatEncodings:
 
   /** Encodes the constraint that at least one of the given variables is true.
     * It is implemented concatenating the expressions with the OR operator.
+    *
     * @param variables the input variables
     * @return the [[satify.model.Expression]] that encodes the constraint
     */
   def atLeastOne(variables: Symbol*): Expression =
     val vars: Seq[Symbol] = removeDuplicates(variables)
     requireVariables(vars, 2, "atLeastOne")
-    vars.reduceLeft(_ or _)
+    vars.reduceLeft(Or(_, _))
 
   /** Encodes the constraint that at most one of the given variables is true.
     * It uses the sequential encoding that produces 3n − 4 clauses (O(n) complexity).
+    *
     * @param variables the input variables
     * @return the [[satify.model.Expression]] that encodes the constraint
     */
@@ -33,25 +34,25 @@ object SatEncodings:
     // removing duplicates
     // generate new n - 1 variables
     val newVars = (1 until vars.length).map(_ => generator()).toList
-    val startingClauses = (not(vars.head) or newVars.head) and (not(vars.last) or newVars.last)
+    val startingClauses = And(Or(Not(vars.head), newVars.head), Or(Not(vars.last), newVars.last))
     val middleClauses = for (x, i) <- vars.zipWithIndex if i > 0 && i < vars.length - 1
-    yield (not(x) or newVars(i)) and
-      (not(newVars(i - 1)) or newVars(i)) and
-      (not(x) or not(newVars(i - 1)))
-    middleClauses.foldLeft(startingClauses)(_ and _)
+    yield And(And(Or(Not(x), newVars(i)), Or(Not(newVars(i - 1)), newVars(i))), Or(Not(x), Not(newVars(i - 1))))
+    middleClauses.foldLeft(startingClauses)(And(_, _))
 
   /** Encodes the constraint that exactly one of the given variables is true.
+    *
     * @param variables the input variables
     * @return the [[satify.model.Expression]] that encodes the constraint
     */
   def exactlyOne(variables: Symbol*): Expression =
     val vars: Seq[Symbol] = removeDuplicates(variables)
     requireVariables(vars, 2, "exactlyOne")
-    atLeastOne(vars: _*) and atMostOne(vars: _*)
+    And(atLeastOne(vars: _*), atMostOne(vars: _*))
 
   /** Encodes the constraint that at most k of the given variables are true.
     * It is implemented using sequential encoding that produces 2nk + n − 3k − 1 clauses (O(n) complexity).
-    * @param k the number of variables that must be true
+    *
+    * @param k         the number of variables that must be true
     * @param variables the input variables
     * @return the [[satify.model.Expression]] that encodes the constraint
     */
@@ -64,14 +65,16 @@ object SatEncodings:
 
   /** Encodes the constraint that at least k of the given variables are true.
     * It is implemented using the pairwise encoding that produces O(n&#94;2) clauses.
-    * @param k the number of variables that must be true
+    *
+    * @param k         the number of variables that must be true
     * @param variables the input variables
     * @return the [[satify.model.Expression]] that encodes the constraint
     */
   def atLeastK(k: Int)(variables: Symbol*): Expression =
     val vars: Seq[Symbol] = removeDuplicates(variables)
     requireVariables(vars, 2, "atLeastK")
     require(k <= vars.length, "atLeastK encoding requires k <= n")
+
     def combinations(vars: Seq[Symbol], k: Int): Seq[Seq[Expression]] =
       if (k == 0) Seq(Seq())
       else if (k == 1) vars.map(Seq(_))
@@ -81,7 +84,8 @@ object SatEncodings:
           subCombination <- combinations(vars.drop(i + 1), k - 1)
         yield vars(i) +: subCombination
 
-    combinations(vars, k).map(_.reduceLeft(_ and _)).reduceLeft(_ or _)
+    combinations(vars, k).map(_.reduceLeft(And(_, _))).reduceLeft(Or(_, _))
+
 
   extension (expressions: Seq[Symbol])