2-SAT

2-SAT with \(N\) clauses can be solved with time complexity of \(O(N)\). SCC should be with this snippet in the code.

Example

use twosat::*;

fn main() {
// (not 0 or 1) and (not 1 or 2) and (0 or 2) and (2 or 1)
let mut ts = TwoSat::new(3);
for (a, b) in [((0, false), (1, true)), ((1, false), (2, true)), ((0, true), (2, true)), ((2, true), (1, true))] {
    ts.add_clause(a, b);
}
println!("{:?}", ts.solve()); // Some([false, true, true])

// (0 or 0) and (not 0 or not 0)
let mut ts = TwoSat::new(1);
for (a, b) in [((0, true), (0, true)), ((0, false), (0, false))] {
    ts.add_clause(a, b);
}
println!("{:?}", ts.solve()); // None
}

mod scc {
    struct SccStack {
        stack: Vec<u32>,
        check: Vec<u64>,
    }

    impl SccStack {
        fn new(cap: usize) -> Self {
            Self {
                stack: vec![0; cap],
                check: vec![0; (cap + 63) / 64],
            }
        }
        fn push(&mut self, n: usize) {
            self.stack.push(n as u32);
            self.check[n / 64] |= 1 << (n % 64);
        }
        fn pop(&mut self) -> Option<usize> {
            let tmp = self.stack.pop()? as usize;
            self.check[tmp / 64] &= !(1 << (tmp % 64));
            Some(tmp)
        }
        fn contains(&self, n: usize) -> bool {
            self.check[n / 64] & (1 << (n % 64)) != 0
        }
    }

    struct DfsPack {
        gid: usize,
        id: Vec<usize>,
        low: Vec<usize>,
        st: SccStack,
    }

    fn dfs(n: usize, graph: &[Vec<usize>], curr: usize, p: &mut DfsPack, list: &mut Vec<Vec<usize>>) {
        p.st.push(curr);
        p.id[curr] = p.gid;
        p.low[curr] = p.gid;
        p.gid += 1;

        for &next in graph[curr].iter() {
            if p.id[next] == n {
                dfs(n, graph, next, p, list);
            }
        }
        for &next in graph[curr].iter() {
            if p.st.contains(next) {
                p.low[curr] = p.low[curr].min(p.low[next]);
            }
        }

        if p.id[curr] == p.low[curr] {
            let mut newlist = vec![];
            while let Some(popped) = p.st.pop() {
                if popped == curr {
                    break;
                }
                newlist.push(popped);
            }
            newlist.push(curr);
            list.push(newlist);
        }
    }

    /// Returns a list of SCCs of `graph`.
    /// The returned list is a 2D vector of `usize`, which consists of a list of vertices within a same SCC.
    /// The order of the SCCs in the returned list is topologically sorted.
    ///
    /// The implementation uses Tarjan's SCC algorithm.
    pub fn find_scc(graph: &[Vec<usize>]) -> Vec<Vec<usize>> {
        let n = graph.len();
        let mut list = vec![];

        let mut p = DfsPack {
            gid: 0,
            id: vec![n; n],
            low: vec![usize::MAX; n],
            st: SccStack::new(n),
        };
        for x in 0..n {
            if p.id[x] != n {
                continue;
            }
            dfs(n, graph, x, &mut p, &mut list);
        }
        list.reverse();
        list
    }

    /// Returns a list about what SCC each vertices are in.
    /// `scc_list` has to be generated in advance from `find_scc`.
    pub fn gen_scc_ids(graph: &[Vec<usize>], scc_list: &[Vec<usize>]) -> Vec<usize> {
        let mut ids = vec![0; graph.len()];
        for (i, l) in scc_list.iter().enumerate() {
            for &v in l {
                ids[v] = i;
            }
        }
        ids
    }

    /// Returns a graph of SCCs. The number of vertices of the new graph will be the number of SCCs in the graph.
    /// `scc_list` and `scc_ids` have to be generated in advanced from `find_scc` and `gen_scc_ids`.
    pub fn gen_scc_graph(graph: &[Vec<usize>], scc_list: &[Vec<usize>], scc_ids: &[usize]) -> Vec<Vec<usize>> {
        let mut ret = vec![vec![]; scc_list.len()];
        for u in 0..graph.len() {
            let a = scc_ids[u];
            for &v in graph[u].iter() {
                let b = scc_ids[v];
                if a < b {
                    ret[a].push(b);
                }
            }
        }
        ret
    }
}

mod twosat {
    use super::scc::*;

    /// 2-SAT solver.
    pub struct TwoSat {
        n: usize,
        graph: Vec<Vec<usize>>,
    }

    impl TwoSat {
        /// Creates a new instance of 2-SAT solver.
        pub fn new(n: usize) -> Self {
            Self { n, graph: vec![vec![]; n << 1] }
        }

        /// Adds a clause of `(i, f) & (j, g)`.
        /// For example, `self.add_clause((0, false), (1, true))` is adding a clause `~x0 & x1` to the solver.
        pub fn add_clause(&mut self, (i, f): (usize, bool), (j, g): (usize, bool)) {
            let judge = |x: bool, a: usize, b: usize| if x { a } else { b };
            self.graph[i * 2 + judge(f, 0, 1)].push(j * 2 + judge(g, 1, 0));
            self.graph[j * 2 + judge(g, 0, 1)].push(i * 2 + judge(f, 1, 0));
        }

        /// Returns any possible solution of the 2-SAT problem if there's any in O(N) time.
        /// Returns `None` if the problem is unsolvable.
        pub fn solve(&self) -> Option<Vec<bool>> {
            let mut ans = vec![false; self.n];
            let scc_list = find_scc(&self.graph);
            let ids = gen_scc_ids(&self.graph, &scc_list);
            for i in 0..self.n {
                if ids[i * 2] == ids[i * 2 + 1] {
                    return None;
                }
                ans[i] = ids[i * 2] < ids[i * 2 + 1];
            }
            Some(ans)
        }
    }
}

Code

mod twosat {
    use super::scc::*;

    /// 2-SAT solver.
    pub struct TwoSat {
        n: usize,
        graph: Vec<Vec<usize>>,
    }

    impl TwoSat {
        /// Creates a new instance of 2-SAT solver.
        pub fn new(n: usize) -> Self {
            Self { n, graph: vec![vec![]; n << 1] }
        }

        /// Adds a clause of `(i, f) & (j, g)`.
        /// For example, `self.add_clause((0, false), (1, true))` is adding a clause `~x0 & x1` to the solver.
        pub fn add_clause(&mut self, (i, f): (usize, bool), (j, g): (usize, bool)) {
            let judge = |x: bool, a: usize, b: usize| if x { a } else { b };
            self.graph[i * 2 + judge(f, 0, 1)].push(j * 2 + judge(g, 1, 0));
            self.graph[j * 2 + judge(g, 0, 1)].push(i * 2 + judge(f, 1, 0));
        }

        /// Returns any possible solution of the 2-SAT problem if there's any in O(N) time.
        /// Returns `None` if the problem is unsolvable.
        pub fn solve(&self) -> Option<Vec<bool>> {
            let mut ans = vec![false; self.n];
            let scc_list = find_scc(&self.graph);
            let ids = gen_scc_ids(&self.graph, &scc_list);
            for i in 0..self.n {
                if ids[i * 2] == ids[i * 2 + 1] {
                    return None;
                }
                ans[i] = ids[i * 2] < ids[i * 2 + 1];
            }
            Some(ans)
        }
    }
}

Last modified on 231008.