From 0e97bfb05092b43586a38ff5ea35b7cbaf582d7a Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Sun, 10 Jul 2011 12:46:06 +0000
Subject: [PATCH] little Sat solver in one (big, fat) line
---
cp-demo/SatSolver.scala | 23 +++++++++++++++++++++++
1 file changed, 23 insertions(+)
create mode 100644 cp-demo/SatSolver.scala
diff --git a/cp-demo/SatSolver.scala b/cp-demo/SatSolver.scala
new file mode 100644
index 000000000..698f6ea59
--- /dev/null
+++ b/cp-demo/SatSolver.scala
@@ -0,0 +1,23 @@
+import cp.Definitions._
+import cp.Terms._
+
+object SatSolver extends App {
+ val problem : 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)
+ }))
+
+ val answer = solution.solve
+ println("Solution map : " + answer)
+ (1 to 4).foreach(i => println("i : " + answer(i)))
+
+}
--
GitLab