結果
| 問題 |
No.2536 同値性と充足可能性
|
| コンテスト | |
| ユーザー |
 haihamabossu
|
| 提出日時 | 2023-11-10 22:41:45 |
| 言語 | Rust (1.83.0 + proconio) |
| 結果 |
AC
|
| 実行時間 | 74 ms / 2,000 ms |
| コード長 | 12,790 bytes |
| コンパイル時間 | 12,882 ms |
| コンパイル使用メモリ | 377,808 KB |
| 実行使用メモリ | 20,780 KB |
| 最終ジャッジ日時 | 2024-09-26 01:58:04 |
| 合計ジャッジ時間 | 15,379 ms |
|
ジャッジサーバーID （参考情報） |
judge1 / judge4 |
（要ログイン）
| ファイルパターン | 結果 |
|---|---|
| other | AC * 31 |
ソースコード
//https://github.com/rust-lang-ja/ac-library-rs
pub mod internal_scc {
pub struct Csr<E> {
start: Vec<usize>,
elist: Vec<E>,
}
impl<E> Csr<E>
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<usize>) {
// 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<usize>,
low: Vec<usize>,
ord: Vec<Option<usize>>,
ids: Vec<usize>,
}
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<Vec<usize>> {
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<Vec<usize>> = (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<bool>,
}
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<String>,
}
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<T: std::str::FromStr>(&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<String> {
source
.split_whitespace()
.rev()
.map(String::from)
.collect::<Vec<_>>()
}
}
}
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<std::io::StdoutLock>) {
let n = scanner.next::<usize>();
let m = scanner.next::<usize>();
let mut t = TwoSat::new(n);
for _ in 0..m {
let i = scanner.next::<usize>() - 1;
let e = scanner.next::<String>();
let j = scanner.next::<usize>() - 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();
}