Add TwoSAT

Author: harry0000

src/main/scala/io/github/acl4s/TwoSAT.scala

@@ -0,0 +1,39 @@
+package io.github.acl4s
+
+/**
+ * Reference:
+ * B. Aspvall, M. Plass, and R. Tarjan,
+ * A Linear-Time Algorithm for Testing the Truth of Certain Quantified Boolean Formulas
+ *
+ * @param n
+ */
+class TwoSAT(private val n: Int) {
+  val answer = new Array[Boolean](n)
+  private val scc = io.github.acl4s.internal.SccGraph(2 * n)
+
+  def addClause(i: Int, f: Boolean, j: Int, g: Boolean): Unit = {
+    assert(0 <= i && i < n)
+    assert(0 <= j && j < n)
+    scc.addEdge(2 * i + (if (f) { 0 }
+                         else { 1 }),
+                2 * j + (if (g) { 1 }
+                         else { 0 })
+    )
+    scc.addEdge(2 * j + (if (g) { 0 }
+                         else { 1 }),
+                2 * i + (if (f) { 1 }
+                         else { 0 })
+    )
+  }
+
+  def satisfiable(): Boolean = {
+    val (_, id) = scc.sccIds()
+    (0 until n).foreach(i => {
+      if (id(2 * i) == id(2 * i + 1)) {
+        return false
+      }
+      answer(i) = id(2 * i) < id(2 * i + 1)
+    })
+    true
+  }
+}

src/test/scala/io/github/acl4s/TwoSATSuite.scala

@@ -0,0 +1,141 @@
+package io.github.acl4s
+
+class TwoSATSuite extends munit.FunSuite {
+
+  /**
+   * @see https://atcoder.jp/contests/practice2/tasks/practice2_h
+   */
+  test("AtCoder Library Practice Contest H - Two SAT") {
+    val n = 3
+    val x = Array(1, 2, 0)
+    val y = Array(4, 5, 6)
+
+    {
+      // Sample Input 1
+      val d = 2
+
+      val ts = TwoSAT(n)
+      for {
+        i <- 0 until n
+        j <- i + 1 until n
+      } {
+        if ((x(i) - x(j)).abs < d) {
+          ts.addClause(i, false, j, false)
+        }
+        if ((x(i) - y(j)).abs < d) {
+          ts.addClause(i, false, j, true)
+        }
+        if ((y(i) - x(j)).abs < d) {
+          ts.addClause(i, true, j, false)
+        }
+        if ((y(i) - y(j)).abs < d) {
+          ts.addClause(i, true, j, true)
+        }
+      }
+
+      assertEquals(ts.satisfiable(), true)
+
+      val res = ts.answer.zipWithIndex
+        .map((v, i) =>
+          if (v) { x(i) }
+          else { y(i) }
+        )
+        .sorted
+      val min_distance = (1 until n).map(i => res(i) - res(i - 1)).min
+      assert(min_distance >= d)
+    }
+
+    {
+      // Sample Input 2
+      val d = 3
+
+      val ts = TwoSAT(n)
+      for {
+        i <- 0 until n
+        j <- i + 1 until n
+      } {
+        if ((x(i) - x(j)).abs < d) {
+          ts.addClause(i, false, j, false)
+        }
+        if ((x(i) - y(j)).abs < d) {
+          ts.addClause(i, false, j, true)
+        }
+        if ((y(i) - x(j)).abs < d) {
+          ts.addClause(i, true, j, false)
+        }
+        if ((y(i) - y(j)).abs < d) {
+          ts.addClause(i, true, j, true)
+        }
+      }
+
+      assertEquals(ts.satisfiable(), false)
+    }
+  }
+
+  test("zero") {
+    val ts = TwoSAT(0)
+    assertEquals(ts.satisfiable(), true)
+    assertEquals(ts.answer.toSeq, Seq())
+  }
+
+  test("one") {
+    {
+      val ts = TwoSAT(1)
+      ts.addClause(0, true, 0, true)
+      ts.addClause(0, false, 0, false)
+      assertEquals(ts.satisfiable(), false)
+    }
+    {
+      val ts = TwoSAT(1)
+      ts.addClause(0, true, 0, true)
+      assertEquals(ts.satisfiable(), true)
+      assertEquals(ts.answer.toSeq, Seq(true))
+    }
+    {
+      val ts = TwoSAT(1)
+      ts.addClause(0, false, 0, false)
+      assertEquals(ts.satisfiable(), true)
+      assertEquals(ts.answer.toSeq, Seq(false))
+    }
+  }
+
+  test("stress ok") {
+    (0 until 10_000).foreach(phase => {
+      val n = randomInt(1, 20)
+      val m = randomInt(1, 100)
+      val expect = Array.fill(n)(randomBoolean())
+      val ts = TwoSAT(n)
+
+      val xs = new Array[Int](m)
+      val ys = new Array[Int](m)
+      val types = new Array[Int](m)
+      (0 until m).foreach(i => {
+        val x = randomInt(0, n - 1)
+        val y = randomInt(0, n - 1)
+        val ty = randomInt(0, 2)
+        xs(i) = x
+        ys(i) = y
+        types(i) = ty
+        ty match {
+          case 0 => ts.addClause(x, expect(x), y, expect(y))
+          case 1 => ts.addClause(x, !expect(x), y, expect(y))
+          case _ => ts.addClause(x, expect(x), y, !expect(y))
+        }
+      })
+
+      assertEquals(ts.satisfiable(), true)
+
+      val actual = ts.answer
+      (0 until m).foreach(i => {
+        val x = xs(i)
+        val y = ys(i)
+        types(i) match {
+          case 0 => assertEquals(actual(x) == expect(x) || actual(y) == expect(y), true)
+          case 1 => assertEquals(actual(x) != expect(x) || actual(y) == expect(y), true)
+          case _ => assertEquals(actual(x) == expect(x) || actual(y) != expect(y), true)
+        }
+      })
+    })
+  }
+
+}

src/test/scala/io/github/acl4s/Utils.scala

@@ -1,6 +1,7 @@
 package io.github.acl4s
 
 import scala.annotation.tailrec
+import scala.util.Random
 
 @tailrec
 def gcd(a: Long, b: Long): Long = {
@@ -11,3 +12,9 @@ def gcd(a: Long, b: Long): Long = {
     gcd(b, a % b)
   }
 }
+
+def randomInt(min: Int, max: Int): Int =
+  Random.between(min, max + 1)
+
+def randomBoolean(): Boolean =
+  randomInt(0, 1) == 0