//https://github.com/rust-lang-ja/ac-library-rs pub mod internal_scc { pub struct Csr { start: Vec, elist: Vec, } impl Csr where E: Copy, { pub fn new(n: usize, edges: &[(usize, E)], init: E) -> Self { let mut csr = Csr { start: vec![0; n + 1], elist: vec![init; edges.len()], }; for e in edges.iter() { csr.start[e.0 + 1] += 1; } for i in 1..=n { csr.start[i] += csr.start[i - 1]; } let mut counter = csr.start.clone(); for e in edges.iter() { csr.elist[counter[e.0]] = e.1; counter[e.0] += 1; } csr } } #[derive(Copy, Clone)] struct _Edge { to: usize, } /// Reference: /// R. Tarjan, /// Depth-First Search and Linear Graph Algorithms pub struct SccGraph { n: usize, edges: Vec<(usize, _Edge)>, } impl SccGraph { pub fn new(n: usize) -> Self { SccGraph { n, edges: vec![] } } pub fn num_vertices(&self) -> usize { self.n } pub fn add_edge(&mut self, from: usize, to: usize) { self.edges.push((from, _Edge { to })); } /// return pair of (# of scc, scc id) pub fn scc_ids(&self) -> (usize, Vec) { // In C++ ac-library, this function is implemented by using recursive lambda functions. // Instead, we use fn and struct for capturing environments. struct _Env { g: Csr<_Edge>, now_ord: usize, group_num: usize, visited: Vec, low: Vec, ord: Vec>, ids: Vec, } let mut env = _Env { g: Csr::new(self.n, &self.edges, _Edge { to: 0 }), now_ord: 0, group_num: 0, visited: Vec::with_capacity(self.n), low: vec![0; self.n], ord: vec![None; self.n], ids: vec![0; self.n], }; fn dfs(v: usize, n: usize, env: &mut _Env) { env.low[v] = env.now_ord; env.ord[v] = Some(env.now_ord); env.now_ord += 1; env.visited.push(v); for i in env.g.start[v]..env.g.start[v + 1] { let to = env.g.elist[i].to; if let Some(x) = env.ord[to] { env.low[v] = std::cmp::min(env.low[v], x); } else { dfs(to, n, env); env.low[v] = std::cmp::min(env.low[v], env.low[to]); } } if env.low[v] == env.ord[v].unwrap() { loop { let u = *env.visited.last().unwrap(); env.visited.pop(); env.ord[u] = Some(n); env.ids[u] = env.group_num; if u == v { break; } } env.group_num += 1; } } for i in 0..self.n { if env.ord[i].is_none() { dfs(i, self.n, &mut env); } } for x in env.ids.iter_mut() { *x = env.group_num - 1 - *x; } (env.group_num, env.ids) } pub fn scc(&self) -> Vec> { let ids = self.scc_ids(); let group_num = ids.0; let mut counts = vec![0usize; group_num]; for &x in ids.1.iter() { counts[x] += 1; } let mut groups: Vec> = (0..ids.0).map(|_| vec![]).collect(); for i in 0..group_num { groups[i].reserve(counts[i]); } for i in 0..self.n { groups[ids.1[i]].push(i); } groups } } } pub mod twosat { //! 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::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, answer: vec![false; n], 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 { if id[2 * i] == id[2 * i + 1] { return false; } self.answer[i] = id[2 * i] < id[2 * i + 1]; } 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 } } #[cfg(test)] mod tests { #![allow(clippy::many_single_char_names)] use super::*; #[test] fn solve_alpc_h_sample1() { // https://atcoder.jp/contests/practice2/tasks/practice2_h let (n, d) = (3, 2); let x = [1, 2, 0i32]; let y = [4, 5, 6]; let mut t = TwoSat::new(n); for i in 0..n { for j in i + 1..n { if (x[i] - x[j]).abs() < d { t.add_clause(i, false, j, false); } if (x[i] - y[j]).abs() < d { t.add_clause(i, false, j, true); } if (y[i] - x[j]).abs() < d { t.add_clause(i, true, j, false); } if (y[i] - y[j]).abs() < d { t.add_clause(i, true, j, true); } } } assert!(t.satisfiable()); let answer = t.answer(); let mut res = vec![]; for (i, &v) in answer.iter().enumerate() { if v { res.push(x[i]) } else { res.push(y[i]); } } //Check the min distance between flags res.sort_unstable(); let mut min_distance = i32::max_value(); for i in 1..res.len() { min_distance = std::cmp::min(min_distance, res[i] - res[i - 1]); } assert!(min_distance >= d); } #[test] fn solve_alpc_h_sample2() { // https://atcoder.jp/contests/practice2/tasks/practice2_h let (n, d) = (3, 3); let x = [1, 2, 0i32]; let y = [4, 5, 6]; let mut t = TwoSat::new(n); for i in 0..n { for j in i + 1..n { if (x[i] - x[j]).abs() < d { t.add_clause(i, false, j, false); } if (x[i] - y[j]).abs() < d { t.add_clause(i, false, j, true); } if (y[i] - x[j]).abs() < d { t.add_clause(i, true, j, false); } if (y[i] - y[j]).abs() < d { t.add_clause(i, true, j, true); } } } assert!(!t.satisfiable()); } } } use twosat::*; pub mod scanner { pub struct Scanner { buf: Vec, } impl Scanner { pub fn new() -> Self { Self { buf: vec![] } } pub fn new_from(source: &str) -> Self { let source = String::from(source); let buf = Self::split(source); Self { buf } } pub fn next(&mut self) -> T { loop { if let Some(x) = self.buf.pop() { return x.parse().ok().expect(""); } let mut source = String::new(); std::io::stdin().read_line(&mut source).expect(""); self.buf = Self::split(source); } } fn split(source: String) -> Vec { source .split_whitespace() .rev() .map(String::from) .collect::>() } } } use crate::scanner::Scanner; use crate::TwoSat; use std::io::Write; fn main() { let mut scanner = Scanner::new(); let out = std::io::stdout(); let mut out = std::io::BufWriter::new(out.lock()); let t: usize = 1; for _ in 0..t { solve(&mut scanner, &mut out); } } fn solve(scanner: &mut Scanner, out: &mut std::io::BufWriter) { let n = scanner.next::(); let m = scanner.next::(); let mut t = TwoSat::new(n); for _ in 0..m { let i = scanner.next::() - 1; let e = scanner.next::(); let j = scanner.next::() - 1; if &e == "<==>" { t.add_clause(i, false, j, true); t.add_clause(i, true, j, false); } else { t.add_clause(i, false, j, false); t.add_clause(i, true, j, true); } } if !t.satisfiable() { writeln!(out, "No").unwrap(); return; } writeln!(out, "Yes").unwrap(); let mut ans1 = vec![]; let mut ans2 = vec![]; for i in 0..n { if t.answer()[i] { ans1.push(i + 1); } else { ans2.push(i + 1); } } let ans = if ans1.len() > ans2.len() { ans1 } else { ans2 }; writeln!(out, "{}", ans.len()).unwrap(); for i in 0..ans.len() { if i > 0 { write!(out, " ").unwrap(); } write!(out, "{}", ans[i]).unwrap(); } writeln!(out, "").unwrap(); }