competitive/graph/
two_satisfiability.rs

1use super::{DirectedSparseGraph, StronglyConnectedComponent};
2
3#[derive(Debug, Clone)]
4pub struct TwoSatisfiability {
5    vsize: usize,
6    edges: Vec<(usize, usize)>,
7}
8
9impl TwoSatisfiability {
10    pub fn new(vsize: usize) -> Self {
11        Self {
12            vsize,
13            edges: Vec::new(),
14        }
15    }
16    /// (p_x = f) | (p_y = g)
17    pub fn add_clause(&mut self, x: usize, f: bool, y: usize, g: bool) {
18        self.edges.push((2 * x + f as usize, 2 * y + !g as usize));
19        self.edges.push((2 * y + g as usize, 2 * x + !f as usize));
20    }
21    pub fn add_or(&mut self, x: usize, y: usize) {
22        self.add_clause(x, true, y, true);
23    }
24    pub fn add_nand(&mut self, x: usize, y: usize) {
25        self.add_clause(x, false, y, false);
26    }
27    pub fn set_true(&mut self, x: usize) {
28        self.edges.push((2 * x + 1, 2 * x));
29    }
30    pub fn set_false(&mut self, x: usize) {
31        self.edges.push((2 * x, 2 * x + 1));
32    }
33    pub fn two_satisfiability(self) -> Option<Vec<bool>> {
34        let graph = DirectedSparseGraph::from_edges(self.vsize * 2, self.edges);
35        let scc = StronglyConnectedComponent::new(&graph);
36        let mut res = vec![false; self.vsize];
37        for i in 0..self.vsize {
38            if scc[i * 2] == scc[i * 2 + 1] {
39                return None;
40            }
41            res[i] = scc[i * 2] > scc[i * 2 + 1];
42        }
43        Some(res)
44    }
45}
competitive/graph/two_satisfiability.rs

competitive/graph/
two_satisfiability.rs
