monolith

/// A 2-SAT instance over boolean variables, solved through strongly

/// connected components of the implication graph.

pub(crate) struct TwoSat {

    vars: usize,

    clauses: Vec<(Lit, Lit)>,

}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]

pub(crate) struct Lit {

    pub var: usize,

    pub value: bool,

}

impl Lit {

    pub fn new(var: usize, value: bool) -> Self {

        Self { var, value }

    }

    fn node(self) -> usize {

        2 * self.var + usize::from(self.value)

    }

    fn negated(self) -> Self {

        Self {

            var: self.var,

            value: !self.value,

        }

    }

}

impl TwoSat {

    pub fn new(vars: usize) -> Self {

        Self {

            vars,

            clauses: Vec::new(),

        }

    }

    pub fn either(&mut self, a: Lit, b: Lit) {

        self.clauses.push((a, b));

    }

    pub fn require(&mut self, a: Lit) {

        self.clauses.push((a, a));

    }

    pub fn solve(&self) -> Option<Vec<bool>> {

        let n = 2 * self.vars;

        let mut graph = vec![Vec::new(); n];

        for &(a, b) in &self.clauses {

            graph[a.negated().node()].push(b.node());

            graph[b.negated().node()].push(a.node());

        }

        let comp = tarjan(&graph);

        let mut out = Vec::with_capacity(self.vars);

        for v in 0..self.vars {

            let (f, t) = (comp[2 * v], comp[2 * v + 1]);

            if f == t {

                return None;

            }

            out.push(t < f);

        }

        Some(out)

    }

    /// A solution that takes each variable's preferred value, in order,

    /// whenever that stays satisfiable.

    pub fn solve_preferring(mut self, preferred: &[bool]) -> Option<Vec<bool>> {

        self.solve()?;

        for (var, &value) in preferred.iter().enumerate() {

            self.require(Lit::new(var, value));

            if self.solve().is_none() {

                self.clauses.pop();

                self.require(Lit::new(var, !value));

            }

        }

        self.solve()

    }

}

/// Tarjan's algorithm, iterative. Components come out in reverse

/// topological order, so a lower index means later in the implication order.

fn tarjan(graph: &[Vec<usize>]) -> Vec<usize> {

    struct State {

        index: Vec<usize>,

        low: Vec<usize>,

        on_stack: Vec<bool>,

        stack: Vec<usize>,

        next: usize,

    }

    impl State {

        fn enter(&mut self, v: usize, work: &mut Vec<(usize, usize)>) {

            self.index[v] = self.next;

            self.low[v] = self.next;

            self.next += 1;

            self.stack.push(v);

            self.on_stack[v] = true;

            work.push((v, 0));

        }

    }

    let n = graph.len();

    let mut st = State {

        index: vec![usize::MAX; n],

        low: vec![0; n],

        on_stack: vec![false; n],

        stack: Vec::new(),

        next: 0,

    };

    let mut comp = vec![usize::MAX; n];

    let mut next_comp = 0;

    let mut work = Vec::new();

    for root in 0..n {

        if st.index[root] != usize::MAX {

            continue;

        }

        st.enter(root, &mut work);

        while let Some(&(v, edge)) = work.last() {

            if let Some(&w) = graph[v].get(edge) {

                if let Some(top) = work.last_mut() {

                    top.1 += 1;

                }

                if st.index[w] == usize::MAX {

                    st.enter(w, &mut work);

                } else if st.on_stack[w] {

                    st.low[v] = st.low[v].min(st.index[w]);

                }

                continue;

            }

            work.pop();

            if let Some(&(parent, _)) = work.last() {

                st.low[parent] = st.low[parent].min(st.low[v]);

            }

            if st.low[v] == st.index[v] {

                while let Some(w) = st.stack.pop() {

                    st.on_stack[w] = false;

                    comp[w] = next_comp;

                    if w == v {

                        break;

                    }

                }

                next_comp += 1;

            }

        }

    }

    comp

}

#[cfg(test)]

mod tests {

    use super::*;

    #[test]

    fn unsatisfiable() {

        let mut s = TwoSat::new(1);

        s.require(Lit::new(0, true));

        s.require(Lit::new(0, false));

        assert!(s.solve().is_none());

    }

}