// rw3sat_oo.scala
 
import scala.util.Random
 
object Main {
  class Literal(val index: Int, val flag: Boolean) {
    def apply(x: Seq[Boolean]) = this.flag ^ x(this.index)
  }
  object Literal {
    def apply(index: Int, flag: Boolean) = new Literal(index, flag)
  }
 
  class Clause(val literals: Seq[Literal]) {
    def apply(x: Seq[Boolean]) = this.literals.exists(_(x))
  }
  object Clause {
    def apply(literals: Literal*) = new Clause(literals)
  }
 
  class CNF(val clauses: Seq[Clause]) {
    def apply(x: Seq[Boolean]) = this.clauses.forall(_(x))
  }
  object CNF {
    def apply(clauses: Clause*) = new CNF(clauses)
  }
 
  def sample[A](a: Seq[A]): A = a(Random.nextInt(a.length))
 
  def w4(n: Int): Seq[Boolean] = for (_ <- 0 until n) yield Random.nextBoolean  // W4
 
  def rw3sat(f: CNF, n: Int, r: Int): String = {
    @annotation.tailrec
    def loop(k: Int, r: Int, x: Seq[Boolean]): Option[Seq[Boolean]] = 
      (f(x), k, r) match {
        case (true, _, _) => Some(x)                                // W7,W8
        case (_, 0, 0) => None                                      // W17
        case (_, 0, _) => loop(n * 3, r - 1, w4(n))                 // W15,W16
        case _ => {
          val c = sample(f.clauses.filterNot(_(x)))                 // W10
          val index = sample(c.literals).index                      // W11
          val x2 = x.updated(index, !x(index))                      // W12
          loop(k - 1, r, x2)                                        // W13,W14
        }
      }
 
    loop(n * 3, r, w4(n)) match {                               // W2,W3,W5,W6
      case Some(x) => "Satisfiable with [" + x.mkString(",") + "]"   // "充足可能である"
      case _ => "Probably Unsatisfiable"    // "おそらく充足不可能である"
    }
  }
 
  def main(args: Array[String]): Unit = {
    val p1 = Clause(Literal(0, false), Literal(1, false), Literal(2, false))
    val p2 = Clause(Literal(3, false), Literal(1, false), Literal(2, true ))
    val p3 = Clause(Literal(0, true ), Literal(3, false), Literal(2, false))
    val p4 = Clause(Literal(0, true ), Literal(3, true ), Literal(1, false))
    val p5 = Clause(Literal(3, true ), Literal(1, true ), Literal(2, false))
    val p6 = Clause(Literal(0, true ), Literal(1, true ), Literal(2, true ))
    val p7 = Clause(Literal(0, false), Literal(3, true ), Literal(2, true ))
    val p8 = Clause(Literal(0, false), Literal(3, false), Literal(1, true ))
 
    val f = CNF(p1, p2, p3, p4, p5, p6, p7, p8)
    // val f = CNF(p1, p2, p3, p4, p5, p6, p8)
    println(rw3sat(f, 4, 3))
    // => Probably Unsatisfiable
  }
}

Ly8gcnczc2F0X29vLnNjYWxhCgppbXBvcnQgc2NhbGEudXRpbC5SYW5kb20KCm9iamVjdCBNYWluIHsKICBjbGFzcyBMaXRlcmFsKHZhbCBpbmRleDogSW50LCB2YWwgZmxhZzogQm9vbGVhbikgewogICAgZGVmIGFwcGx5KHg6IFNlcVtCb29sZWFuXSkgPSB0aGlzLmZsYWcgXiB4KHRoaXMuaW5kZXgpCiAgfQogIG9iamVjdCBMaXRlcmFsIHsKICAgIGRlZiBhcHBseShpbmRleDogSW50LCBmbGFnOiBCb29sZWFuKSA9IG5ldyBMaXRlcmFsKGluZGV4LCBmbGFnKQogIH0KCiAgY2xhc3MgQ2xhdXNlKHZhbCBsaXRlcmFsczogU2VxW0xpdGVyYWxdKSB7CiAgICBkZWYgYXBwbHkoeDogU2VxW0Jvb2xlYW5dKSA9IHRoaXMubGl0ZXJhbHMuZXhpc3RzKF8oeCkpCiAgfQogIG9iamVjdCBDbGF1c2UgewogICAgZGVmIGFwcGx5KGxpdGVyYWxzOiBMaXRlcmFsKikgPSBuZXcgQ2xhdXNlKGxpdGVyYWxzKQogIH0KCiAgY2xhc3MgQ05GKHZhbCBjbGF1c2VzOiBTZXFbQ2xhdXNlXSkgewogICAgZGVmIGFwcGx5KHg6IFNlcVtCb29sZWFuXSkgPSB0aGlzLmNsYXVzZXMuZm9yYWxsKF8oeCkpCiAgfQogIG9iamVjdCBDTkYgewogICAgZGVmIGFwcGx5KGNsYXVzZXM6IENsYXVzZSopID0gbmV3IENORihjbGF1c2VzKQogIH0KCiAgZGVmIHNhbXBsZVtBXShhOiBTZXFbQV0pOiBBID0gYShSYW5kb20ubmV4dEludChhLmxlbmd0aCkpCgogIGRlZiB3NChuOiBJbnQpOiBTZXFbQm9vbGVhbl0gPSBmb3IgKF8gPC0gMCB1bnRpbCBuKSB5aWVsZCBSYW5kb20ubmV4dEJvb2xlYW4gIC8vIFc0CgogIGRlZiBydzNzYXQoZjogQ05GLCBuOiBJbnQsIHI6IEludCk6IFN0cmluZyA9IHsKICAgIEBhbm5vdGF0aW9uLnRhaWxyZWMKICAgIGRlZiBsb29wKGs6IEludCwgcjogSW50LCB4OiBTZXFbQm9vbGVhbl0pOiBPcHRpb25bU2VxW0Jvb2xlYW5dXSA9IAogICAgICAoZih4KSwgaywgcikgbWF0Y2ggewogICAgICAgIGNhc2UgKHRydWUsIF8sIF8pID0+IFNvbWUoeCkgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIC8vIFc3LFc4CiAgICAgICAgY2FzZSAoXywgMCwgMCkgPT4gTm9uZSAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgLy8gVzE3CiAgICAgICAgY2FzZSAoXywgMCwgXykgPT4gbG9vcChuICogMywgciAtIDEsIHc0KG4pKSAgICAgICAgICAgICAgICAgLy8gVzE1LFcxNgogICAgICAgIGNhc2UgXyA9PiB7CiAgICAgICAgICB2YWwgYyA9IHNhbXBsZShmLmNsYXVzZXMuZmlsdGVyTm90KF8oeCkpKSAgICAgICAgICAgICAgICAgLy8gVzEwCiAgICAgICAgICB2YWwgaW5kZXggPSBzYW1wbGUoYy5saXRlcmFscykuaW5kZXggICAgICAgICAgICAgICAgICAgICAgLy8gVzExCiAgICAgICAgICB2YWwgeDIgPSB4LnVwZGF0ZWQoaW5kZXgsICF4KGluZGV4KSkgICAgICAgICAgICAgICAgICAgICAgLy8gVzEyCiAgICAgICAgICBsb29wKGsgLSAxLCByLCB4MikgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgLy8gVzEzLFcxNAogICAgICAgIH0KICAgICAgfQoKICAgIGxvb3AobiAqIDMsIHIsIHc0KG4pKSBtYXRjaCB7ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIC8vIFcyLFczLFc1LFc2CiAgICAgIGNhc2UgU29tZSh4KSA9PiAiU2F0aXNmaWFibGUgd2l0aCBbIiArIHgubWtTdHJpbmcoIiwiKSArICJdIiAgIC8vICLlhYXotrPlj6/og73jgafjgYLjgosiCiAgICAgIGNhc2UgXyA9PiAiUHJvYmFibHkgVW5zYXRpc2ZpYWJsZSIgICAgLy8gIuOBiuOBneOCieOBj+WFhei2s+S4jeWPr+iDveOBp+OBguOCiyIKICAgIH0KICB9CgogIGRlZiBtYWluKGFyZ3M6IEFycmF5W1N0cmluZ10pOiBVbml0ID0gewogICAgdmFsIHAxID0gQ2xhdXNlKExpdGVyYWwoMCwgZmFsc2UpLCBMaXRlcmFsKDEsIGZhbHNlKSwgTGl0ZXJhbCgyLCBmYWxzZSkpCiAgICB2YWwgcDIgPSBDbGF1c2UoTGl0ZXJhbCgzLCBmYWxzZSksIExpdGVyYWwoMSwgZmFsc2UpLCBMaXRlcmFsKDIsIHRydWUgKSkKICAgIHZhbCBwMyA9IENsYXVzZShMaXRlcmFsKDAsIHRydWUgKSwgTGl0ZXJhbCgzLCBmYWxzZSksIExpdGVyYWwoMiwgZmFsc2UpKQogICAgdmFsIHA0ID0gQ2xhdXNlKExpdGVyYWwoMCwgdHJ1ZSApLCBMaXRlcmFsKDMsIHRydWUgKSwgTGl0ZXJhbCgxLCBmYWxzZSkpCiAgICB2YWwgcDUgPSBDbGF1c2UoTGl0ZXJhbCgzLCB0cnVlICksIExpdGVyYWwoMSwgdHJ1ZSApLCBMaXRlcmFsKDIsIGZhbHNlKSkKICAgIHZhbCBwNiA9IENsYXVzZShMaXRlcmFsKDAsIHRydWUgKSwgTGl0ZXJhbCgxLCB0cnVlICksIExpdGVyYWwoMiwgdHJ1ZSApKQogICAgdmFsIHA3ID0gQ2xhdXNlKExpdGVyYWwoMCwgZmFsc2UpLCBMaXRlcmFsKDMsIHRydWUgKSwgTGl0ZXJhbCgyLCB0cnVlICkpCiAgICB2YWwgcDggPSBDbGF1c2UoTGl0ZXJhbCgwLCBmYWxzZSksIExpdGVyYWwoMywgZmFsc2UpLCBMaXRlcmFsKDEsIHRydWUgKSkKCiAgICB2YWwgZiA9IENORihwMSwgcDIsIHAzLCBwNCwgcDUsIHA2LCBwNywgcDgpCiAgICAvLyB2YWwgZiA9IENORihwMSwgcDIsIHAzLCBwNCwgcDUsIHA2LCBwOCkKICAgIHByaW50bG4ocnczc2F0KGYsIDQsIDMpKQogICAgLy8gPT4gUHJvYmFibHkgVW5zYXRpc2ZpYWJsZQogIH0KfQ==