From fcde1045f2291256df7702e59e6fcee5f7514553 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ali=20Sinan=20K=C3=B6ksal?= <alisinan@gmail.com>
Date: Sat, 17 Sep 2011 00:06:29 +0000
Subject: [PATCH] Sat solver accepting DIMACS format input
---
cp-demo/SatSolver.scala | 31 +++++++++++++++++++------------
1 file changed, 19 insertions(+), 12 deletions(-)
diff --git a/cp-demo/SatSolver.scala b/cp-demo/SatSolver.scala
index 698f6ea59..a3795dcb6 100644
--- a/cp-demo/SatSolver.scala
+++ b/cp-demo/SatSolver.scala
@@ -1,23 +1,30 @@
import cp.Definitions._
import cp.Terms._
+import scala.io.Source
-object SatSolver extends App {
- val problem : List[List[Int]] = List(
+object SatSolver {
+ val defaultProblem : List[List[Int]] = List(
List(-1, 2, 3),
List(1, -2),
List(4)
)
- 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)
- }))
+ def main(args: Array[String]): Unit = {
- val answer = solution.solve
- println("Solution map : " + answer)
- (1 to 4).foreach(i => println("i : " + answer(i)))
+ 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)
+ }))
+
+ val answer = solution.solve
+ println("Solution map : " + answer)
+ (1 to 4).foreach(i => println("i : " + answer(i)))
+ }
}
--
GitLab