1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
use num::{BigInt, One, Zero};
use super::super::node::NodeType::*;
use crate::Ddnnf;
impl Ddnnf {
#[inline]
pub(crate) fn annotate_partial_derivatives(&mut self) {
for node in self.nodes.iter_mut() {
node.partial_derivative.set_zero();
}
let total_nodes = self.nodes.len();
self.nodes[total_nodes - 1].partial_derivative.set_one();
for i in (0..total_nodes).rev() {
self.annotate_single_partial_derivative(i);
}
}
#[inline]
fn annotate_single_partial_derivative(&mut self, i: usize) {
match &self.nodes[i].ntype {
And { children } => {
let children_c = children.clone();
for &child in children_c.iter() {
let mut current_node_partial_derivative =
self.nodes[i].partial_derivative.clone();
for &other_child in children_c.iter() {
if child != other_child {
current_node_partial_derivative *= &self.nodes[other_child].count;
}
}
self.nodes[child].partial_derivative += ¤t_node_partial_derivative;
}
}
Or { children } => {
let current_node_partial_derivative = self.nodes[i].partial_derivative.clone();
for child in children.clone() {
self.nodes[child].partial_derivative += ¤t_node_partial_derivative;
}
}
_ => (), // True, False, and Literal
}
}
#[inline]
pub(crate) fn card_of_feature_with_partial_derivatives(&mut self, feature: i32) -> BigInt {
match self.literals.get(&-feature).cloned() {
Some(i) => self.rc() - &self.nodes[i].partial_derivative,
// there is no literal corresponding to the feature number and because of that we don't have to do anything besides returning the count of the model
None => self.rc(),
}
}
#[inline]
// Computes the cardinality of a node using the marking algorithm:
// And and Or nodes that base the computation on their child nodes use the
// .temp value if the child node is marked and the .count value if not
pub(crate) fn calc_count_marked_node(&mut self, i: usize) {
match &self.nodes[i].ntype {
And { children } => {
let marked_children = children
.iter()
.filter(|&&child| self.nodes[child].marker)
.collect::<Vec<&usize>>();
self.nodes[i].temp = if marked_children.len() <= children.len() / 2 {
marked_children
.iter()
.fold(self.nodes[i].count.clone(), |mut acc, &&index| {
let node = &self.nodes[index];
if !node.count.is_zero() {
acc /= &node.count;
}
acc *= &node.temp;
acc
})
} else {
children
.iter()
.map(|&index| {
let node = &self.nodes[index];
if node.marker { &node.temp } else { &node.count }
})
.product()
}
}
Or { children } => {
self.nodes[i].temp = children
.iter()
.map(|&index| {
let node = &self.nodes[index];
if node.marker { &node.temp } else { &node.count }
})
.sum()
}
False => self.nodes[i].temp.set_zero(),
_ => self.nodes[i].temp.set_one(), // True and Literal
}
}
#[inline]
// Computes the cardinality of a feature and partial configurations using the marking algorithm
fn operate_on_marker(&mut self, indexes: &[usize], operation: fn(&mut Ddnnf, usize)) -> BigInt {
self.mark_assumptions(indexes);
// calc the count for all marked nodes, respectevly all nodes that matter
for j in 0..self.md.len() {
operation(self, self.md[j]);
}
// reset everything
for index in &self.md {
self.nodes[*index].marker = false;
}
for &index in indexes {
self.nodes[index].marker = false;
}
self.md.clear();
// the result is propagated through the whole graph up to the root
self.rt()
}
#[inline]
/// Computes the cardinality of a feature using the marking algorithm.
/// The marking algorithm differs to the standard variation by only reomputing the
/// marked nodes. Further, the marked nodes use the .temp value of the childs nodes if they
/// are also marked and the .count value if they are not.
pub(crate) fn card_of_feature_with_marker(&mut self, feature: i32) -> BigInt {
if self.has_no_effect_on_query(&feature) {
self.rc()
} else if self.makes_query_unsat(&feature) {
BigInt::ZERO
} else {
match self.literals.get(&-feature).cloned() {
Some(i) => self.operate_on_marker(&[i], Ddnnf::calc_count_marked_node),
// there is no literal corresponding to the feature number and because of that we don't have to do anything besides returning the count of the model
None => self.rc(),
}
}
}
#[inline]
/// Computes the cardinality of a partial configuration using the marking algorithm.
/// Works analog to the card_of_feature_with_marker()
pub(crate) fn operate_on_partial_config_marker(
&mut self,
features: &[i32],
operation: fn(&mut Ddnnf, usize),
) -> BigInt {
if self.query_is_not_sat(features) {
BigInt::ZERO
} else {
let features: Vec<i32> = self.reduce_query(features);
let indexes: Vec<usize> = self.map_features_opposing_indexes(&features);
if indexes.is_empty() {
return self.rc();
}
self.operate_on_marker(&indexes, operation)
}
}
// creates a clone of the nodes which were marked when computing the cardinality
// for a given partial configuration
pub fn get_marked_nodes_clone(&mut self, features: &[i32]) -> Vec<usize> {
let opposing_indices = &self.map_features_opposing_indexes(features);
self.mark_assumptions(opposing_indices);
// add the literal nodes
for index in opposing_indices.iter() {
self.md.push(*index);
}
self.md.sort_unstable();
let marked_nodes = self.md.clone();
// reset everything
self.md.clear();
for node in self.nodes.iter_mut() {
node.marker = false;
}
marked_nodes
}
#[inline]
// marks the nodes under the assumptions that all nodes, provided via
// indexes are literals that are deselected
fn mark_assumptions(&mut self, indexes: &[usize]) {
for index in indexes.iter().copied() {
self.nodes[index].temp.set_zero(); // change the value of the node
self.mark_nodes_start(index); // go through the path til the root node is marked
}
// sort the marked nodes so that we make sure to first calculate the childnodes and then their parents
self.md.sort_unstable();
}
#[inline]
// marks the nodes starting from an initial Literal. All parents and parents of parents til
// the root nodes get marked
fn mark_nodes_start(&mut self, i: usize) {
self.nodes[i].marker = true;
for parent in self.nodes[i].parents.clone() {
// check for parent nodes and adjust their count resulting of the changes to their children
if !self.nodes[parent].marker {
// only mark those nodes which aren't already marked to specificly avoid marking nodes near the root multple times
self.mark_nodes(parent);
}
}
}
#[inline]
// marks the nodes starting from an initial Literal. All parents and parents of parents til
// the root nodes get marked
fn mark_nodes(&mut self, i: usize) {
self.nodes[i].marker = true;
self.md.push(i);
for parent in self.nodes[i].parents.clone() {
// check for parent nodes and adjust their count resulting of the changes to their children
if !self.nodes[parent].marker {
// only mark those nodes which aren't already marked to specificly avoid marking nodes near the root multple times
self.mark_nodes(parent);
}
}
}
}
#[cfg(test)]
mod test {
use crate::parser::build_ddnnf;
use std::path::Path;
#[test]
fn marking_nodes() {
let mut ddnnf = build_ddnnf(Path::new("tests/data/small_ex_c2d.nnf"), None);
ddnnf.mark_assumptions(&[0]);
assert_eq!(vec![11], ddnnf.md);
for node in ddnnf.nodes.iter_mut() {
node.marker = false;
}
ddnnf.md.clear();
ddnnf.mark_assumptions(&[2, 4]);
assert_eq!(vec![3, 6, 7, 11], ddnnf.md);
for node in ddnnf.nodes.iter_mut() {
node.marker = false;
}
ddnnf.md.clear();
assert!(ddnnf.get_marked_nodes_clone(&[]).is_empty());
assert_eq!(vec![4, 6, 7, 11], ddnnf.get_marked_nodes_clone(&[2]));
assert_eq!(vec![9, 10, 11], ddnnf.get_marked_nodes_clone(&[4]));
assert_eq!(
vec![4, 6, 7, 9, 10, 11],
ddnnf.get_marked_nodes_clone(&[2, 4])
);
assert_eq!(
vec![2, 3, 7, 9, 10, 11],
ddnnf.get_marked_nodes_clone(&[1, 3, 4])
);
}
}