library_checker/math/
two_sat.rs

1#[doc(no_inline)]
2pub use competitive::graph::TwoSatisfiability;
3use competitive::prelude::*;
4
5#[verify::library_checker("two_sat")]
6pub fn two_sat(reader: impl Read, mut writer: impl Write) {
7    let s = read_all_unchecked(reader);
8    let mut scanner = Scanner::new(&s);
9    scan!(
10        scanner,
11        _p: String,
12        _cnf: String,
13        n,
14        m,
15        ab: [(isize, isize, isize)]
16    );
17    let mut two_sat = TwoSatisfiability::new(n);
18    for (a, b, _) in ab.take(m) {
19        two_sat.add_clause(a.unsigned_abs() - 1, a >= 0, b.unsigned_abs() - 1, b >= 0);
20    }
21    if let Some(v) = two_sat.two_satisfiability() {
22        writeln!(writer, "s SATISFIABLE").ok();
23        write!(writer, "v").ok();
24        for (i, v) in v.into_iter().enumerate() {
25            write!(
26                writer,
27                " {}",
28                if v { i as i32 + 1 } else { -(i as i32 + 1) }
29            )
30            .ok();
31        }
32        write!(writer, " 0").ok();
33    } else {
34        writeln!(writer, "s UNSATISFIABLE").ok();
35    }
36}
library_checker/math/two_sat.rs

library_checker/math/
two_sat.rs
