competitive/algorithm/
horn_satisfiability.rs

1/// Horn Satisfiability
2///
3/// $\wedge(\wedge_i v_{p_i}\rightarrow v_q = f)$
4pub struct HornSatisfiability {
5    literals: Vec<Option<bool>>,
6    clauses: Vec<(usize, usize, bool)>,
7    idx: Vec<Vec<usize>>,
8    satisfiable: bool,
9    stack: Vec<usize>,
10}
11
12impl HornSatisfiability {
13    pub fn new(size: usize) -> Self {
14        Self {
15            literals: vec![None; size],
16            clauses: vec![],
17            idx: vec![vec![]; size],
18            satisfiable: true,
19            stack: vec![],
20        }
21    }
22
23    pub fn add_clause(&mut self, p: impl IntoIterator<Item = usize>, q: usize, f: bool) {
24        let mut count = 0;
25        let id = self.clauses.len();
26        for p_i in p.into_iter() {
27            if self.literals[p_i] != Some(true) {
28                self.idx[p_i].push(id);
29                count += 1;
30            }
31        }
32        self.clauses.push((count, q, f));
33        if count == 0 {
34            self.stack.push(id);
35            self.resolve();
36        }
37    }
38
39    pub fn is_satisfiable(&self) -> bool {
40        self.satisfiable
41    }
42
43    pub fn solve(&self) -> Option<Vec<bool>> {
44        if !self.satisfiable {
45            return None;
46        }
47        Some(self.literals.iter().map(|&x| x.unwrap_or(false)).collect())
48    }
49
50    fn resolve(&mut self) {
51        while let Some(id) = self.stack.pop() {
52            let (_count, q, f) = self.clauses[id];
53            self.satisfiable &= self.literals[q] != Some(!f);
54            self.literals[q] = Some(f);
55            if f {
56                while let Some(i) = self.idx[q].pop() {
57                    let (ref mut count, _, _) = self.clauses[i];
58                    *count -= 1;
59                    if *count == 0 {
60                        self.stack.push(i);
61                    }
62                }
63            }
64        }
65    }
66}
67
68#[cfg(test)]
69mod tests {
70    use super::*;
71    use crate::tools::Xorshift;
72
73    #[test]
74    fn test_horn_satisfiability() {
75        let mut rng = Xorshift::default();
76        for _ in 0..100 {
77            let n = rng.random(1..=10);
78            let mut clauses = vec![];
79            let mut hs = HornSatisfiability::new(n);
80            for _ in 0..100 {
81                let prob = rng.randf();
82                let mut clause: Vec<_> = (0..n).filter(|_| rng.randf() < prob).collect();
83                let cand_q: Vec<_> = (0..n).filter(|x| !clause.contains(x)).collect();
84                let q = if clause.len() == n {
85                    clause.remove(rng.random(0..n))
86                } else {
87                    cand_q[rng.random(0..cand_q.len())]
88                };
89                let f = rng.gen_bool(0.5);
90                hs.add_clause(clause.iter().cloned(), q, f);
91                clauses.push((clause, q, f));
92
93                let check = |lits: &Vec<bool>| -> bool {
94                    for (p, q, f) in &clauses {
95                        if p.iter().all(|&p| lits[p]) && lits[*q] != *f {
96                            return false;
97                        }
98                    }
99                    true
100                };
101                let res = hs.solve();
102                let satisfiable = (0..1 << n)
103                    .map(|bits| (0..n).map(|i| (bits & (1 << i)) != 0).collect())
104                    .any(|lits| check(&lits));
105                assert_eq!(res.is_some(), satisfiable);
106                if let Some(lits) = res {
107                    assert!(check(&lits));
108                }
109            }
110        }
111    }
112}
competitive/algorithm/horn_satisfiability.rs

competitive/algorithm/
horn_satisfiability.rs
