decdnnf_rs/algorithms/
counting.rs

1use crate::{
2    core::{EdgeIndex, Node, NodeIndex},
3    DecisionDNNF, Literal,
4};
5use rug::Integer;
6use std::sync::OnceLock;
7
8static INTEGER_ZERO: Integer = Integer::ZERO;
9
10/// A structure used to count the models of a [`DecisionDNNF`].
11///
12/// The algorithm takes a time polynomial in the size of the Decision-DNNF.
13///
14/// # Example
15///
16/// ```
17/// use decdnnf_rs::{DecisionDNNF, ModelCounter};
18///
19/// fn count_models(ddnnf: &DecisionDNNF) {
20///     let model_counter = ModelCounter::new(ddnnf, false);
21///     println!("the formula has {} models", model_counter.global_count());
22/// }
23/// # count_models(&decdnnf_rs::D4Reader::default().read("t 1 0".as_bytes()).unwrap())
24/// ```
25pub struct ModelCounter<'a> {
26    ddnnf: &'a DecisionDNNF,
27    assumptions: Option<Vec<Option<bool>>>,
28    n_models: OnceLock<Vec<Option<Integer>>>,
29    partial_models: bool,
30}
31
32impl<'a> ModelCounter<'a> {
33    /// Builds a new model counter given a formula.
34    ///
35    /// This function can both count the number of full or partial models.
36    #[must_use]
37    pub fn new(ddnnf: &'a DecisionDNNF, partial_models: bool) -> Self {
38        Self {
39            ddnnf,
40            assumptions: None,
41            n_models: OnceLock::new(),
42            partial_models,
43        }
44    }
45
46    /// Set assumption literals, reducing the number of models.
47    ///
48    /// The only models to be considered are the ones that contain all the literals marked as assumptions.
49    /// The set of assumptions must involved at most once each variable.
50    ///
51    /// # Panics
52    ///
53    /// This function panics if the set of assumptions involves the same variable multiple times.
54    pub fn set_assumptions(&mut self, assumptions: &[Literal]) {
55        let mut assumps = vec![None; self.ddnnf.n_vars()];
56        for a in assumptions {
57            assert!(a.var_index() < self.ddnnf.n_vars(), "undefined variable");
58            assert!(
59                assumps[a.var_index()].replace(a.polarity()).is_none(),
60                "multiple definition of the same variable in assumptions"
61            );
62        }
63        self.assumptions = Some(assumps);
64        self.n_models.take();
65    }
66
67    fn get_or_compute_n_models(&self) -> &[Option<Integer>] {
68        self.n_models.get_or_init(|| {
69            let (n_root_free_vars, or_children_free_vars_len) = self.free_vars_params();
70            let mut n_models = vec![None; self.ddnnf.nodes().as_slice().len()];
71            compute_models_from(
72                self.ddnnf,
73                n_root_free_vars,
74                &or_children_free_vars_len,
75                NodeIndex::from(0),
76                &mut n_models,
77                self.assumptions.as_deref(),
78            );
79            n_models
80        })
81    }
82
83    fn free_vars_params(&self) -> (usize, Vec<Vec<usize>>) {
84        if self.partial_models {
85            (
86                0,
87                self.ddnnf
88                    .nodes()
89                    .as_slice()
90                    .iter()
91                    .map(|n| {
92                        if let Node::Or(children) = n {
93                            vec![0; children.len()]
94                        } else {
95                            vec![]
96                        }
97                    })
98                    .collect::<Vec<_>>(),
99            )
100        } else {
101            let free_variables = self.ddnnf.free_vars();
102            if let Some(assumps) = &self.assumptions {
103                let n_free_vars = |lits: &[Literal]| {
104                    lits.iter()
105                        .filter(|l| assumps[l.var_index()].is_none())
106                        .count()
107                };
108                (
109                    n_free_vars(free_variables.root_free_vars()),
110                    (0..self.ddnnf.n_nodes())
111                        .map(|i| {
112                            free_variables
113                                .or_free_vars()
114                                .iter_child_free_vars(i)
115                                .map(n_free_vars)
116                                .collect::<Vec<_>>()
117                        })
118                        .collect::<Vec<_>>(),
119                )
120            } else {
121                (
122                    free_variables.root_free_vars().len(),
123                    (0..self.ddnnf.n_nodes())
124                        .map(|i| {
125                            free_variables
126                                .or_free_vars()
127                                .iter_child_free_vars_lengths(i)
128                                .collect::<Vec<_>>()
129                        })
130                        .collect::<Vec<_>>(),
131                )
132            }
133        }
134    }
135
136    /// Returns the number of counted elements of the whole formula.
137    #[must_use]
138    #[allow(clippy::missing_panics_doc)]
139    pub fn global_count(&self) -> &Integer {
140        self.get_or_compute_n_models()[0].as_ref().unwrap()
141    }
142
143    /// Returns the [`DecisionDNNF`] which elements are counted.
144    #[must_use]
145    pub fn ddnnf(&self) -> &DecisionDNNF {
146        self.ddnnf
147    }
148
149    /// Returns the number of counted elements of the subfomula rooted at the node which index is given.
150    ///
151    /// # Panics
152    ///
153    /// This function panics if the provided node index is greater or equal to the number of nodes of the formula.
154    #[must_use]
155    pub fn count_from(&self, index: NodeIndex) -> &Integer {
156        self.get_or_compute_n_models()[usize::from(index)]
157            .as_ref()
158            .unwrap()
159    }
160
161    /// Returns a Boolean value indicating if partial models are computed (`false` is returns in case full models are computed).
162    #[must_use]
163    pub fn partial_models(&self) -> bool {
164        self.partial_models
165    }
166}
167
168fn compute_models_from<'a>(
169    ddnnf: &'a DecisionDNNF,
170    n_root_free_vars: usize,
171    or_children_free_vars_len: &[Vec<usize>],
172    index: NodeIndex,
173    n_models: &mut [Option<Integer>],
174    assumptions: Option<&[Option<bool>]>,
175) {
176    if n_models[usize::from(index)].is_some() {
177        return;
178    }
179    let edge_indices = match &ddnnf.nodes()[index] {
180        Node::And(edge_indices) | Node::Or(edge_indices) => edge_indices.clone(),
181        Node::True | Node::False => vec![],
182    };
183    let in_contradiction_with_assumptions = |e: EdgeIndex| {
184        if let Some(assumps) = assumptions {
185            ddnnf.edges()[e]
186                .propagated()
187                .iter()
188                .any(|l| assumps[l.var_index()].is_some_and(|p| p != l.polarity()))
189        } else {
190            false
191        }
192    };
193    for e in edge_indices {
194        if in_contradiction_with_assumptions(e) {
195            continue;
196        }
197        let target = ddnnf.edges()[e].target();
198        compute_models_from(
199            ddnnf,
200            n_root_free_vars,
201            or_children_free_vars_len,
202            target,
203            n_models,
204            assumptions,
205        );
206    }
207    let iter_for_children = |c: &'a Vec<EdgeIndex>| {
208        c.iter().map(|e| {
209            if in_contradiction_with_assumptions(*e) {
210                return &INTEGER_ZERO;
211            }
212            n_models[usize::from(ddnnf.edges()[*e].target())]
213                .as_ref()
214                .unwrap()
215        })
216    };
217    let mut n = match &ddnnf.nodes()[index] {
218        Node::And(edge_indices) => iter_for_children(edge_indices).product(),
219        Node::Or(edge_indices) => iter_for_children(edge_indices)
220            .zip(or_children_free_vars_len[usize::from(index)].iter())
221            .map(|(n, w)| n.clone() << w)
222            .sum(),
223        Node::True => Integer::ONE.clone(),
224        Node::False => Integer::ZERO,
225    };
226    if index == NodeIndex::from(0) {
227        n <<= n_root_free_vars;
228    }
229    n_models[usize::from(index)] = Some(n);
230}
231
232#[cfg(test)]
233mod tests {
234    use super::*;
235    use crate::D4Reader;
236
237    fn assert_counts(
238        instance: &str,
239        n_vars: Option<usize>,
240        expected_model_count: usize,
241        expected_path_count: usize,
242    ) {
243        assert_counts_under_assumptions(
244            instance,
245            n_vars,
246            expected_model_count,
247            expected_path_count,
248            None,
249        );
250    }
251
252    fn assert_counts_under_assumptions(
253        instance: &str,
254        n_vars: Option<usize>,
255        expected_model_count: usize,
256        expected_path_count: usize,
257        assumptions: Option<Vec<isize>>,
258    ) {
259        let mut ddnnf = D4Reader::default().read(instance.as_bytes()).unwrap();
260        if let Some(n) = n_vars {
261            ddnnf.update_n_vars(n);
262        }
263        let mut model_counter = ModelCounter::new(&ddnnf, false);
264        if let Some(assumps) = assumptions.clone() {
265            model_counter.set_assumptions(
266                &assumps
267                    .iter()
268                    .map(|i| Literal::from(*i))
269                    .collect::<Vec<_>>(),
270            );
271        }
272        assert_eq!(
273            expected_model_count,
274            model_counter.global_count().to_usize_wrapping()
275        );
276        let mut path_counter = ModelCounter::new(&ddnnf, true);
277        if let Some(assumps) = assumptions {
278            path_counter.set_assumptions(
279                &assumps
280                    .iter()
281                    .map(|i| Literal::from(*i))
282                    .collect::<Vec<_>>(),
283            );
284        }
285        assert_eq!(
286            expected_path_count,
287            path_counter.global_count().to_usize_wrapping()
288        );
289    }
290
291    #[test]
292    fn test_ok() {
293        assert_counts(
294            "a 1 0\no 2 0\no 3 0\nt 4 0\n1 2 0\n1 3 0\n2 4 -1 0\n2 4 1 0\n3 4 -2 0\n3 4 2 0\n",
295            None,
296            4,
297            4,
298        );
299    }
300
301    #[test]
302    fn test_true_no_vars() {
303        assert_counts("t 1 0\n", None, 1, 1);
304    }
305
306    #[test]
307    fn test_true_one_var() {
308        assert_counts("t 1 0\n", Some(1), 2, 1);
309    }
310
311    #[test]
312    fn test_true_two_vars() {
313        assert_counts("t 1 0\n", Some(2), 4, 1);
314    }
315
316    #[test]
317    fn test_false() {
318        assert_counts("f 1 0\n", None, 0, 0);
319    }
320
321    #[test]
322    fn test_clause() {
323        assert_counts(
324            r"
325                o 1 0
326                o 2 0
327                t 3 0
328                2 3 -1 -2 0
329                2 3 1 0
330                1 2 0",
331            None,
332            3,
333            2,
334        );
335    }
336
337    #[test]
338    fn test_implied_lit() {
339        assert_counts(
340            r"
341                o 1 0
342                o 2 0
343                t 3 0
344                f 4 0
345                2 3 -1 0
346                2 4 1 0
347                1 2 0",
348            Some(2),
349            2,
350            1,
351        );
352    }
353
354    #[test]
355    fn test_assumptions() {
356        let instance = r"
357        o 1 0
358        a 2 0
359        a 3 0
360        t 4 0
361        1 2 0
362        1 3 0
363        2 4 1 2 0
364        3 4 -1 3 0
365        ";
366        let check = |assumptions, models, paths| {
367            assert_counts_under_assumptions(instance, None, models, paths, assumptions);
368        };
369        check(None, 4, 2);
370        check(Some(vec![-1]), 2, 1);
371        check(Some(vec![1]), 2, 1);
372        check(Some(vec![-2]), 1, 1);
373        check(Some(vec![2]), 3, 2);
374        check(Some(vec![-1, -2]), 1, 1);
375        check(Some(vec![-1, 2]), 1, 1);
376        check(Some(vec![1, -2]), 0, 0);
377        check(Some(vec![1, 2]), 2, 1);
378        check(Some(vec![-1, -2, -3]), 0, 0);
379        check(Some(vec![-1, -2, 3]), 1, 1);
380        check(Some(vec![-1, 2, -3]), 0, 0);
381        check(Some(vec![-1, 2, 3]), 1, 1);
382        check(Some(vec![1, -2, -3]), 0, 0);
383        check(Some(vec![1, -2, 3]), 0, 0);
384        check(Some(vec![1, 2, -3]), 1, 1);
385        check(Some(vec![1, 2, 3]), 1, 1);
386    }
387
388    #[test]
389    fn test_count_under_assumptions_top() {
390        let instance = "t 1 0\n";
391        let mut ddnnf = D4Reader::default().read(instance.as_bytes()).unwrap();
392        ddnnf.update_n_vars(1);
393        assert_counts_under_assumptions("t 1 0\n", Some(1), 2, 1, Some(vec![]));
394        assert_counts_under_assumptions("t 1 0\n", Some(1), 1, 1, Some(vec![-1]));
395        assert_counts_under_assumptions("t 1 0\n", Some(1), 1, 1, Some(vec![1]));
396    }
397}
decdnnf_rs/algorithms/counting.rs

decdnnf_rs/algorithms/
counting.rs
