1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
use std::cmp::Ordering::{Equal, Greater, Less};

use scc::Scc;

pub fn twosat(
    len: usize,
    cnf: impl IntoIterator<Item = [(usize, bool); 2]>,
) -> Option<Vec<bool>> {
    let g = {
        let mut g = vec![vec![]; 2 * len];
        let index = |(index, not): (usize, bool)| 2 * index + not as usize;
        for [(index_x, not_x), (index_y, not_y)] in cnf {
            g[index((index_x, !not_x))].push(index((index_y, not_y)));
            g[index((index_y, !not_y))].push(index((index_x, not_x)));
        }
        g
    };

    let index = |&v: &_| v;
    let delta = |&v: &usize| g[v].iter().copied();
    let scc = Scc::new(0..2 * len, 2 * len, index, delta);
    let mut cert = vec![false; len];
    for x in 0..len {
        let x_true = 2 * x;
        let x_false = 2 * x + 1;
        match scc.comp_id(&x_true).cmp(&scc.comp_id(&x_false)) {
            Less => cert[x] = false,
            Equal => return None,
            Greater => cert[x] = true,
        }
    }
    Some(cert)
}

#[cfg(test)]
mod tests {
    use crate::*;

    #[test]
    fn sanity_check_sat() {
        let cnf = vec![
            [(0, true), (1, false)],
            [(1, true), (2, true)],
            [(2, false), (3, false)],
            [(3, true), (0, false)],
        ];

        let res = twosat(4, cnf.clone());
        assert!(res.is_some());
        let cert = res.unwrap();
        assert!(
            cnf.iter()
                .all(|&[(ix, vx), (iy, vy)]| cert[ix] == vx || cert[iy] == vy)
        );
    }

    #[test]
    fn sanity_check_unsat() {
        let cnf = vec![
            [(0, true), (1, true)],
            [(0, true), (1, false)],
            [(0, false), (1, true)],
            [(0, false), (1, false)],
        ];

        let res = twosat(2, cnf);
        assert!(res.is_none());
    }
}