diff --git a/src/main/scala/io/github/acl4s/TwoSAT.scala b/src/main/scala/io/github/acl4s/TwoSAT.scala new file mode 100644 index 0000000..77c2dc6 --- /dev/null +++ b/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 + } +} diff --git a/src/test/scala/io/github/acl4s/TwoSATSuite.scala b/src/test/scala/io/github/acl4s/TwoSATSuite.scala new file mode 100644 index 0000000..07b77ae --- /dev/null +++ b/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) + } + }) + }) + } + +} diff --git a/src/test/scala/io/github/acl4s/Utils.scala b/src/test/scala/io/github/acl4s/Utils.scala index 1dc0be0..dca5c76 100644 --- a/src/test/scala/io/github/acl4s/Utils.scala +++ b/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