///|
/// Boolean 2-SAT over clauses (x_i = f) OR (x_j = g).
pub struct TwoSat {
  priv n : Int
  priv graph : @scc.SccGraph
  priv assignment : Array[Bool]
} derive(Debug)

///|
pub fn TwoSat::new(n : Int) -> TwoSat {
  guard 0 <= n && n <= 50000000 else { panic() }
  { n, graph: @scc.SccGraph::new(2 * n), assignment: Array::make(n, false), }
}

///|
pub fn TwoSat::add_clause(
  self : TwoSat,
  i : Int,
  f : Bool,
  j : Int,
  g : Bool,
) -> Unit {
  guard 0 <= i && i < self.n && 0 <= j && j < self.n else { panic() }
  self.graph.add_edge(
    2 * i + (if f { 0 } else { 1 }),
    2 * j + (if g { 1 } else { 0 }),
  )
  self.graph.add_edge(
    2 * j + (if g { 0 } else { 1 }),
    2 * i + (if f { 1 } else { 0 }),
  )
}

///|
pub fn TwoSat::satisfiable(self : TwoSat) -> Bool {
  let groups = self.graph.scc()
  let ids = Array::make(2 * self.n, 0)
  for i = 0; i < groups.length(); i = i + 1 {
    for v in groups[i] {
      ids[v] = i
    }
  }
  for i = 0; i < self.n; i = i + 1 {
    if ids[2 * i] == ids[2 * i + 1] {
      return false
    }
    self.assignment[i] = ids[2 * i] < ids[2 * i + 1]
  }
  true
}

///|
/// A snapshot of the last satisfying assignment; only meaningful after a successful check.
pub fn TwoSat::answer(self : TwoSat) -> Array[Bool] {
  self.assignment.copy()
}