diff --git a/src/twosat.rs b/src/twosat.rs index ac5f8b6..1a6e464 100644 --- a/src/twosat.rs +++ b/src/twosat.rs @@ -1,11 +1,68 @@ +//! A 2-SAT Solver. use crate::internal_scc; +/// A 2-SAT Solver. +/// +/// For variables $x_0, x_1, \ldots, x_{N - 1}$ and clauses with from +/// +/// \\[ +/// (x_i = f) \lor (x_j = g) +/// \\] +/// +/// it decides whether there is a truth assignment that satisfies all clauses. +/// +/// # Example +/// +/// ``` +/// #![allow(clippy::many_single_char_names)] +/// +/// use ac_library_rs::TwoSat; +/// use proconio::{input, marker::Bytes, source::once::OnceSource}; +/// +/// input! { +/// from OnceSource::from( +/// "3\n\ +/// 3\n\ +/// a b\n\ +/// !b c\n\ +/// !a !a\n", +/// ), +/// n: usize, +/// pqs: [(Bytes, Bytes)], +/// } +/// +/// let mut twosat = TwoSat::new(n); +/// +/// for (p, q) in pqs { +/// fn parse(s: &[u8]) -> (usize, bool) { +/// match *s { +/// [c] => ((c - b'a').into(), true), +/// [b'!', c] => ((c - b'a').into(), false), +/// _ => unreachable!(), +/// } +/// } +/// let ((i, f), (j, g)) = (parse(&p), parse(&q)); +/// twosat.add_clause(i, f, j, g); +/// } +/// +/// assert!(twosat.satisfiable()); +/// assert_eq!(twosat.answer(), [false, true, true]); +/// ``` pub struct TwoSat { n: usize, scc: internal_scc::SccGraph, answer: Vec, } impl TwoSat { + /// Creates a new `TwoSat` of `n` variables and 0 clauses. + /// + /// # Constraints + /// + /// - $0 \leq n \leq 10^8$ + /// + /// # Complexity + /// + /// - $O(n)$ pub fn new(n: usize) -> Self { TwoSat { n, @@ -13,11 +70,30 @@ impl TwoSat { scc: internal_scc::SccGraph::new(2 * n), } } + /// Adds a clause $(x_i = f) \lor (x_j = g)$. + /// + /// # Constraints + /// + /// - $0 \leq i < n$ + /// - $0 \leq j < n$ + /// + /// # Panics + /// + /// Panics if the above constraints are not satisfied. + /// + /// # Complexity + /// + /// - $O(1)$ amortized pub fn add_clause(&mut self, i: usize, f: bool, j: usize, g: bool) { assert!(i < self.n && j < self.n); self.scc.add_edge(2 * i + !f as usize, 2 * j + g as usize); self.scc.add_edge(2 * j + !g as usize, 2 * i + f as usize); } + /// Returns whether there is a truth assignment that satisfies all clauses. + /// + /// # Complexity + /// + /// - $O(n + m)$ where $m$ is the number of added clauses pub fn satisfiable(&mut self) -> bool { let id = self.scc.scc_ids().1; for i in 0..self.n { @@ -28,6 +104,17 @@ impl TwoSat { } true } + /// Returns a truth assignment that satisfies all clauses **of the last call of [`satisfiable`]**. + /// + /// # Constraints + /// + /// - [`satisfiable`] is called after adding all clauses and it has returned `true`. + /// + /// # Complexity + /// + /// - $O(n)$ + /// + /// [`satisfiable`]: #method.satisfiable pub fn answer(&self) -> &[bool] { &self.answer }