fork download
copy 
  1. // rw3sat.scala
  2.  
  3. import scala.util.Random
  4. // import scala.language.implicitConversions
  5.  
  6. object Main {
  7.   type Literal = (Int, Boolean)
  8.   object Literal {
  9.     def apply(index: Int, flag: Boolean): Literal = (index, flag)
  10.     def unapply(l: Literal) = Some(l)
  11.   }
  12.  
  13.   type Clause = Seq[Literal]
  14.   object Clause {
  15.     def apply(literals: Literal*): Clause = literals
  16.   }
  17.  
  18.   type CNF = Seq[Clause]
  19.   object CNF {
  20.     def apply(clauses: Clause*): CNF = clauses
  21.   }
  22.  
  23.   trait IsSatisfied[+A]
  24.   case object Satisfied extends IsSatisfied[Nothing]
  25.   case class Unsatisfied[A](x: A) extends IsSatisfied[A]
  26.   // implicit def isSatisfiedToBoolean[A](v: IsSatisfied[A]): Boolean = v match {
  27.   //   case Satisfied => true
  28.   //   case Unsatisfied(_) => false
  29.   // }
  30.  
  31.   def eval(l: Literal)(x: Seq[Boolean]): Boolean = {
  32.     val Literal(i, b) = l
  33.     b ^ x(i)
  34.   }
  35.   def eval(c: Clause)(x: Seq[Boolean]): Boolean = 
  36.     c.exists(eval(_)(x))
  37.   def eval(f: CNF)(x: Seq[Boolean]): IsSatisfied[CNF] =
  38.     f.filterNot(eval(_)(x)) match {
  39.       case Nil => Satisfied
  40.       case fs => Unsatisfied(fs)
  41.     }
  42.  
  43.   def sample[A](a: Seq[A]): A = a(Random.nextInt(a.length))
  44.  
  45.   def w4(n: Int): Seq[Boolean] = for (_ <- 0 until n) yield Random.nextBoolean  // W4
  46.  
  47.   def rw3sat(f: CNF, n: Int, r: Int): String = {
  48.     @annotation.tailrec
  49.     def loop(k: Int, r: Int, x: Seq[Boolean]): Option[Seq[Boolean]] = 
  50.       (eval(f)(x), k, r) match {
  51.         case (Satisfied, _, _) => Some(x)                           // W7,W8
  52.         case (_, 0, 0) => None                                      // W17
  53.         case (_, 0, _) => loop(n * 3, r - 1, w4(n))                 // W15,W16
  54.         case (Unsatisfied(fs), _, _) => {
  55.           val c = sample(fs)                                        // W10
  56.           val Literal(index, _) = sample(c)                         // W11
  57.           val x2 = x.updated(index, !x(index))                      // W12
  58.           loop(k - 1, r, x2)                                        // W13,W14
  59.         }
  60.       }
  61.  
  62.     loop(n * 3, r, w4(n)) match {                               // W2,W3,W5,W6
  63.       case Some(x) => "Satisfiable with [" + x.mkString(",") + "]"   // "充足可能である"
  64.       case _ => "Probably Unsatisfiable"    // "おそらく充足不可能である"
  65.     }
  66.   }
  67.  
  68.   def main(args: Array[String]): Unit = {
  69.     val p1 = Clause(Literal(0, false), Literal(1, false), Literal(2, false))
  70.     val p2 = Clause(Literal(3, false), Literal(1, false), Literal(2, true ))
  71.     val p3 = Clause(Literal(0, true ), Literal(3, false), Literal(2, false))
  72.     val p4 = Clause(Literal(0, true ), Literal(3, true ), Literal(1, false))
  73.     val p5 = Clause(Literal(3, true ), Literal(1, true ), Literal(2, false))
  74.     val p6 = Clause(Literal(0, true ), Literal(1, true ), Literal(2, true ))
  75.     val p7 = Clause(Literal(0, false), Literal(3, true ), Literal(2, true ))
  76.     val p8 = Clause(Literal(0, false), Literal(3, false), Literal(1, true ))
  77.  
  78.     val f = CNF(p1, p2, p3, p4, p5, p6, p7, p8)
  79.     // val f = CNF(p1, p2, p3, p4, p5, p6, p8)
  80.     println(rw3sat(f, 4, 3))
  81.     // => Probably Unsatisfiable
  82.   }
  83. }
Success #stdin #stdout 0.36s 322240KB
comments (?)
stdin
copy 
Standard input is empty
stdout
copy 
Probably Unsatisfiable
https://ideone.com/8hXATb
RW3SAT rev.20160724
language:
Scala (scala 2.12.8)
created:
7 years ago
visibility:
secret

Share or Embed source code

Discover > Sphere Engine API

The brand new service which powers Ideone!

Discover > IDE Widget

Widget for compiling and running the source code in a web browser!