twosat/
lib.rs

1use std::cmp::Ordering::{Equal, Greater, Less};
2
3use scc::Scc;
4
5pub fn twosat(
6    len: usize,
7    cnf: impl IntoIterator<Item = [(usize, bool); 2]>,
8) -> Option<Vec<bool>> {
9    let g = {
10        let mut g = vec![vec![]; 2 * len];
11        let index = |(index, not): (usize, bool)| 2 * index + not as usize;
12        for [(index_x, not_x), (index_y, not_y)] in cnf {
13            g[index((index_x, !not_x))].push(index((index_y, not_y)));
14            g[index((index_y, !not_y))].push(index((index_x, not_x)));
15        }
16        g
17    };
18
19    let index = |&v: &_| v;
20    let delta = |&v: &usize| g[v].iter().copied();
21    let scc = Scc::new(0..2 * len, 2 * len, index, delta);
22    let mut cert = vec![false; len];
23    for x in 0..len {
24        let x_true = 2 * x;
25        let x_false = 2 * x + 1;
26        match scc.comp_id(&x_true).cmp(&scc.comp_id(&x_false)) {
27            Less => cert[x] = false,
28            Equal => return None,
29            Greater => cert[x] = true,
30        }
31    }
32    Some(cert)
33}
34
35#[cfg(test)]
36mod tests {
37    use crate::*;
38
39    #[test]
40    fn sanity_check_sat() {
41        let cnf = vec![
42            [(0, true), (1, false)],
43            [(1, true), (2, true)],
44            [(2, false), (3, false)],
45            [(3, true), (0, false)],
46        ];
47
48        let res = twosat(4, cnf.clone());
49        assert!(res.is_some());
50        let cert = res.unwrap();
51        assert!(
52            cnf.iter()
53                .all(|&[(ix, vx), (iy, vy)]| cert[ix] == vx || cert[iy] == vy)
54        );
55    }
56
57    #[test]
58    fn sanity_check_unsat() {
59        let cnf = vec![
60            [(0, true), (1, true)],
61            [(0, true), (1, false)],
62            [(0, false), (1, true)],
63            [(0, false), (1, false)],
64        ];
65
66        let res = twosat(2, cnf);
67        assert!(res.is_none());
68    }
69}
twosat/lib.rs

twosat/
lib.rs
