haar_lib/algo/
two_sat.rs

1//! 2-SAT
2use crate::graph::{scc::*, *};
3
4/// 2-SATを解く。
5pub struct TwoSat {
6    size: usize,
7    g: Graph<Directed, Edge<(), ()>>,
8}
9
10impl TwoSat {
11    /// **Time complexity** $O(size)$
12    pub fn new(size: usize) -> Self {
13        Self {
14            size,
15            g: Graph::new(2 * size),
16        }
17    }
18
19    fn check(&self, x: isize) -> usize {
20        assert!(x != 0);
21        assert!(x.unsigned_abs() <= self.size);
22
23        if x > 0 {
24            x as usize - 1
25        } else {
26            x.unsigned_abs() + self.size - 1
27        }
28    }
29
30    /// $a \Rightarrow b$
31    pub fn add_if(&mut self, a: isize, b: isize) {
32        self.g.add(Edge::new(self.check(a), self.check(b), (), ()));
33    }
34
35    /// $a \lor b$
36    pub fn add_or(&mut self, a: isize, b: isize) {
37        self.add_if(-a, b);
38        self.add_if(-b, a);
39    }
40
41    /// $\lnot (a \land b)$
42    pub fn not_coexist(&mut self, a: isize, b: isize) {
43        self.add_or(-a, -b);
44    }
45
46    /// **Time complexity** $O(size + E)$
47    pub fn solve(&self) -> Option<Vec<bool>> {
48        let s = SCC::new(&self.g);
49        let s = s.index();
50
51        let (a, b) = s.split_at(self.size);
52        if a.iter().zip(b).any(|(a, b)| a == b) {
53            return None;
54        }
55
56        Some(a.iter().zip(b).map(|(a, b)| a > b).collect())
57    }
58}
haar_lib/algo/two_sat.rs

haar_lib/algo/
two_sat.rs
