nekolib/math/
two_sat.rs

1//! 2-SAT。
2
3use super::super::graph::scc_;
4
5use scc_::scc;
6
7/// 2-SAT。
8///
9/// $f(x\_1, \\dots, x\_n) = \\bigwedge (\\bullet \\vee \\bullet)$
10/// の形の論理式を $\\top$ にするような $x\_1, \\dots, x\_n$ の割り当てがあるか判定する。
11/// ただし、各々の $\\bullet$ は $x\_1, \\dots, x\_n, \\lnot x\_1, \\dots \\lnot x\_n$
12/// のうちのいずれかである。
13///
14/// # Examples
15/// ```
16/// use nekolib::math::TwoSat;
17///
18/// let mut ts = TwoSat::new(4);
19/// ts.add_clause(1, 1);
20/// ts.add_clause(-2, -2);
21/// ts.add_clause(3, -4);
22///
23/// let w = ts.witness().unwrap();
24/// assert!(w[1]);
25/// assert!(!w[2]);
26/// assert!(w[3] || !w[4]);
27///
28/// ts.add_clause(-1, -1);
29/// assert_eq!(ts.witness(), None);
30/// ```
31pub struct TwoSat {
32    n: usize,
33    cnf: Vec<(isize, isize)>,
34}
35
36impl TwoSat {
37    /// $f(x\_1, \\dots, x\_n) = \\top$ で初期化する。
38    ///
39    /// # Examples
40    /// ```
41    /// use nekolib::math::TwoSat;
42    ///
43    /// let ts = TwoSat::new(1);
44    /// assert!(ts.witness().is_some());
45    /// ```
46    pub fn new(n: usize) -> Self { Self { n, cnf: vec![] } }
47    /// $f(x\_1, \\dots, x\_n) \\xleftarrow{\\wedge} (x\_i \\vee x\_j)$ で更新する。
48    ///
49    /// ただし、$i \\lt 0$ のとき $x\_i$ は $\\lnot x\_{-i}$ を指すとする。
50    ///
51    /// # Examples
52    /// ```
53    /// use nekolib::math::TwoSat;
54    ///
55    /// let mut ts = TwoSat::new(3);
56    /// ts.add_clause(-1, 2);
57    /// ts.add_clause(1, 3);
58    /// ```
59    pub fn add_clause(&mut self, i: isize, j: isize) { self.cnf.push((i, j)); }
60    /// 充足可能性を判定し、可能なら解を返す。
61    ///
62    /// # Examples
63    /// ```
64    /// use nekolib::math::TwoSat;
65    ///
66    /// let mut ts = TwoSat::new(3);
67    /// ts.add_clause(-1, 2);
68    /// ts.add_clause(-2, 3);
69    /// ts.add_clause(-3, -2);
70    /// let w = ts.witness().unwrap();
71    /// assert!(!w[1] || w[2]);
72    /// assert!(!w[2] || w[3]);
73    /// assert!(!w[3] || !w[2]);
74    /// // w == [_, false, false, true], for example.
75    ///
76    /// ts.add_clause(2, 1);
77    /// assert_eq!(ts.witness(), None);
78    pub fn witness(&self) -> Option<Vec<bool>> {
79        let n = self.n;
80        let g = {
81            let mut g = vec![vec![]; 2 * (n + 1)];
82            for &(i, j) in &self.cnf {
83                let (i, not_i) = Self::enc(i);
84                let (j, not_j) = Self::enc(j);
85                g[not_i].push(j);
86                g[not_j].push(i);
87            }
88            g
89        };
90        let index = |&v: &usize| v;
91        let delta = |&v: &usize| g[v].iter().cloned();
92        let comp_id = scc(g.len(), 2..g.len(), index, delta);
93        if (1..=n).any(|i| comp_id[2 * i] == comp_id[2 * i + 1]) {
94            return None;
95        }
96        Some(
97            std::iter::once(true)
98                .chain((1..=n).map(|i| comp_id[2 * i + 1] < comp_id[2 * i]))
99                .collect(),
100        )
101    }
102    fn enc(i: isize) -> (usize, usize) {
103        let ii = 2 * i.abs() as usize;
104        if i < 0 {
105            (ii + 1, ii)
106        } else {
107            (ii, ii + 1)
108        }
109    }
110}
nekolib/math/two_sat.rs

nekolib/math/
two_sat.rs
