Skip to main content

library_checker/other/
two_sat.rs

1use competitive::graph::TwoSatisfiability;
2use competitive::prelude::*;
3
4#[verify::library_checker("two_sat")]
5pub fn two_sat(reader: impl Read, writer: impl Write) {
6    prepare_io!(reader, writer);
7    sc!(_p: String,
8        _cnf: String,
9        n,
10        m,
11        ab: [(isize, isize, isize); iter m]);
12    let mut two_sat = TwoSatisfiability::new(n);
13    for (a, b, _) in ab {
14        two_sat.add_clause(a.unsigned_abs() - 1, a >= 0, b.unsigned_abs() - 1, b >= 0);
15    }
16    if let Some(v) = two_sat.two_satisfiability() {
17        let ans = v
18            .into_iter()
19            .enumerate()
20            .map(|(i, v)| if v { i as i32 + 1 } else { -(i as i32 + 1) });
21        pp!("s SATISFIABLE"; "v", @it ans, 0, !);
22    } else {
23        pp!("s UNSATISFIABLE");
24    }
25}