Sat solver as in paper

cp-demo/SatSolver.scala

@@ -9,22 +9,32 @@ object SatSolver {
     List(4)
   )
 
+  def satSolve(problem : Seq[Seq[Int]]) = {
+    problem.map(l => l.map(i => {
+      val id = scala.math.abs(i)
+      val isPos = i > 0
+      val c : Constraint1[Map[Int,Boolean]] = ((m : Map[Int,Boolean]) => m(id) == isPos)
+      c
+    }).reduceLeft(_ || _)).reduceLeft(_ && _).find
+  }
+
   def main(args: Array[String]): Unit = {
 
     val problem: List[List[Int]] = if (args.length > 0 ) (for (line <- Source.fromFile(args(0)).getLines if (!line.startsWith("c") && !line.startsWith("p"))) yield {
         line.split(" ").toList.map(_.toInt)
     }).toList else defaultProblem
 
-    type CM = Constraint1[Map[Int,Boolean]]
-    val solution : CM =
-      problem.foldLeft[CM]((m:Map[Int,Boolean]) => true)((cons:CM,clause:List[Int]) => cons && clause.foldLeft[CM]((m:Map[Int,Boolean]) => false)((cons:CM,lit:Int) => {
-            val isPos = lit > 0
-            val abs = scala.math.abs(lit)
-            cons || ((m:Map[Int,Boolean]) => m(abs) == isPos)
-          }))
+    // type CM = Constraint1[Map[Int,Boolean]]
+    // val solution : CM =
+    //   problem.foldLeft[CM]((m:Map[Int,Boolean]) => true)((cons:CM,clause:List[Int]) => cons && clause.foldLeft[CM]((m:Map[Int,Boolean]) => false)((cons:CM,lit:Int) => {
+    //         val isPos = lit > 0
+    //         val abs = scala.math.abs(lit)
+    //         cons || ((m:Map[Int,Boolean]) => m(abs) == isPos)
+    //       }))
 
-    val answer = solution.solve
-    println("Solution map : " + answer)
-    (1 to 4).foreach(i => println("i : " + answer(i)))
+    // val answer = solution.solve
+    // println("Solution map : " + answer)
+    // (1 to 4).foreach(i => println("i : " + answer(i)))
+    println("satSolve(p)", satSolve(problem))
   }
 }