xlog_prob/kc/
ddnnf.rs

1//! Decision-DNNF parser and CPU reference evaluator.
2
3use std::collections::{BTreeMap, BTreeSet, HashMap, HashSet};
4
5use xlog_core::{Result, XlogError};
6
7use crate::logsumexp::{
8    circuit_logsumexp, validate_circuit_log_weight_pair, validate_circuit_value,
9};
10
11#[derive(Debug, Clone, Copy, PartialEq, Eq)]
12/// Logical operator represented by a decision-DNNF node.
13pub enum DdnnfNodeKind {
14    /// Deterministic disjunction.
15    Or,
16    /// Decomposable conjunction.
17    And,
18    /// Boolean true terminal.
19    True,
20    /// Boolean false terminal.
21    False,
22}
23
24#[derive(Debug, Clone)]
25/// A node in a parsed decision-DNNF circuit.
26pub struct DdnnfNode {
27    /// Logical operator of the node.
28    pub kind: DdnnfNodeKind,
29}
30
31#[derive(Debug, Clone)]
32/// Directed circuit edge annotated with signed DIMACS literals.
33pub struct DdnnfEdge {
34    /// Source node identifier.
35    pub from: u32,
36    /// Target node identifier.
37    pub to: u32,
38    /// Conjunctive literals attached to this edge.
39    pub lits: Vec<i32>,
40}
41
42#[derive(Debug, Clone)]
43/// Parsed decision-DNNF circuit with indexed outgoing edges.
44pub struct DecisionDnnf {
45    root: u32,
46    nodes: BTreeMap<u32, DdnnfNode>,
47    edges: Vec<DdnnfEdge>,
48    outgoing: BTreeMap<u32, Vec<usize>>,
49    max_var: u32,
50}
51
52impl DecisionDnnf {
53    /// Returns the circuit root identifier.
54    pub fn root(&self) -> u32 {
55        self.root
56    }
57
58    /// Returns the largest DIMACS variable referenced by the circuit.
59    pub fn max_var(&self) -> u32 {
60        self.max_var
61    }
62
63    /// Returns the operator of `node_id`, if the node exists.
64    pub fn node_kind(&self, node_id: u32) -> Option<DdnnfNodeKind> {
65        self.nodes.get(&node_id).map(|n| n.kind)
66    }
67
68    /// Returns indices of edges leaving `node_id`.
69    pub fn outgoing_edge_indices(&self, node_id: u32) -> Option<&[usize]> {
70        self.outgoing.get(&node_id).map(|v| v.as_slice())
71    }
72
73    /// Returns an edge by its stable index.
74    pub fn edge(&self, edge_idx: usize) -> Option<&DdnnfEdge> {
75        self.edges.get(edge_idx)
76    }
77
78    /// Parses and validates a textual decision-DNNF circuit.
79    pub fn parse_str(input: &str) -> Result<Self> {
80        let mut nodes: BTreeMap<u32, DdnnfNode> = BTreeMap::new();
81        let mut edges: Vec<DdnnfEdge> = Vec::new();
82        let mut targets: HashSet<u32> = HashSet::new();
83        let mut max_var: u32 = 0;
84
85        for (line_no, raw_line) in input.lines().enumerate() {
86            let line = raw_line.trim();
87            if line.is_empty() {
88                continue;
89            }
90
91            let mut tokens: Vec<&str> = line.split_whitespace().collect();
92            if tokens.is_empty() {
93                continue;
94            }
95
96            if tokens.last() != Some(&"0") {
97                return Err(XlogError::Compilation(format!(
98                    "Decision-DNNF parse error at line {}: missing 0 terminator",
99                    line_no + 1
100                )));
101            }
102            tokens.pop();
103            if tokens.is_empty() {
104                return Err(XlogError::Compilation(format!(
105                    "Decision-DNNF parse error at line {}: empty record before terminator",
106                    line_no + 1
107                )));
108            }
109
110            match tokens[0] {
111                "o" | "a" | "t" | "f" => {
112                    if tokens.len() < 2 {
113                        return Err(XlogError::Compilation(format!(
114                            "Decision-DNNF parse error at line {}: node record missing id",
115                            line_no + 1
116                        )));
117                    }
118                    let id: u32 = tokens[1].parse().map_err(|_| {
119                        XlogError::Compilation(format!(
120                            "Decision-DNNF parse error at line {}: invalid node id '{}'",
121                            line_no + 1,
122                            tokens[1]
123                        ))
124                    })?;
125
126                    let kind = match tokens[0] {
127                        "o" => DdnnfNodeKind::Or,
128                        "a" => DdnnfNodeKind::And,
129                        "t" => DdnnfNodeKind::True,
130                        "f" => DdnnfNodeKind::False,
131                        _ => unreachable!(),
132                    };
133
134                    if nodes.insert(id, DdnnfNode { kind }).is_some() {
135                        return Err(XlogError::Compilation(format!(
136                            "Decision-DNNF parse error at line {}: duplicate node id {}",
137                            line_no + 1,
138                            id
139                        )));
140                    }
141                }
142                _ => {
143                    if tokens.len() < 2 {
144                        return Err(XlogError::Compilation(format!(
145                            "Decision-DNNF parse error at line {}: edge record missing dst",
146                            line_no + 1
147                        )));
148                    }
149                    let from: u32 = tokens[0].parse().map_err(|_| {
150                        XlogError::Compilation(format!(
151                            "Decision-DNNF parse error at line {}: invalid edge src '{}'",
152                            line_no + 1,
153                            tokens[0]
154                        ))
155                    })?;
156                    let to: u32 = tokens[1].parse().map_err(|_| {
157                        XlogError::Compilation(format!(
158                            "Decision-DNNF parse error at line {}: invalid edge dst '{}'",
159                            line_no + 1,
160                            tokens[1]
161                        ))
162                    })?;
163
164                    let mut lits: Vec<i32> = Vec::new();
165                    for &tok in &tokens[2..] {
166                        let lit: i32 = tok.parse().map_err(|_| {
167                            XlogError::Compilation(format!(
168                                "Decision-DNNF parse error at line {}: invalid literal '{}'",
169                                line_no + 1,
170                                tok
171                            ))
172                        })?;
173                        if lit == 0 {
174                            return Err(XlogError::Compilation(format!(
175                                "Decision-DNNF parse error at line {}: literal cannot be 0",
176                                line_no + 1
177                            )));
178                        }
179                        max_var = max_var.max(lit.unsigned_abs());
180                        lits.push(lit);
181                    }
182
183                    let edge_id = edges.len();
184                    edges.push(DdnnfEdge { from, to, lits });
185                    targets.insert(to);
186
187                    // outgoing filled later after validation.
188                    let _ = edge_id;
189                }
190            }
191        }
192
193        if nodes.is_empty() {
194            return Err(XlogError::Compilation(
195                "Decision-DNNF parse error: no nodes found".to_string(),
196            ));
197        }
198
199        for edge in &edges {
200            let from_kind = nodes.get(&edge.from).ok_or_else(|| {
201                XlogError::Compilation(format!(
202                    "Decision-DNNF parse error: edge references unknown src node {}",
203                    edge.from
204                ))
205            })?;
206            let _to_kind = nodes.get(&edge.to).ok_or_else(|| {
207                XlogError::Compilation(format!(
208                    "Decision-DNNF parse error: edge references unknown dst node {}",
209                    edge.to
210                ))
211            })?;
212
213            match from_kind.kind {
214                DdnnfNodeKind::Or | DdnnfNodeKind::And => {}
215                DdnnfNodeKind::True | DdnnfNodeKind::False => {
216                    return Err(XlogError::Compilation(format!(
217                        "Decision-DNNF parse error: leaf node {} cannot have outgoing edges",
218                        edge.from
219                    )));
220                }
221            }
222        }
223
224        let declared: BTreeSet<u32> = nodes.keys().copied().collect();
225        let target_set: BTreeSet<u32> = targets.into_iter().collect();
226        let roots: Vec<u32> = declared.difference(&target_set).copied().collect();
227        let root = match roots.as_slice() {
228            [only] => *only,
229            [] => {
230                return Err(XlogError::Compilation(
231                    "Decision-DNNF parse error: could not infer root (no root candidates)"
232                        .to_string(),
233                ))
234            }
235            many => {
236                return Err(XlogError::Compilation(format!(
237                    "Decision-DNNF parse error: could not infer unique root (candidates: {:?})",
238                    many
239                )))
240            }
241        };
242
243        let mut outgoing: BTreeMap<u32, Vec<usize>> = BTreeMap::new();
244        for (idx, edge) in edges.iter().enumerate() {
245            outgoing.entry(edge.from).or_default().push(idx);
246        }
247
248        // Optional cycle check (defensive).
249        Self::check_acyclic(root, &nodes, &edges, &outgoing)?;
250
251        Ok(Self {
252            root,
253            nodes,
254            edges,
255            outgoing,
256            max_var,
257        })
258    }
259
260    fn check_acyclic(
261        root: u32,
262        nodes: &BTreeMap<u32, DdnnfNode>,
263        edges: &[DdnnfEdge],
264        outgoing: &BTreeMap<u32, Vec<usize>>,
265    ) -> Result<()> {
266        let mut visiting: HashSet<u32> = HashSet::new();
267        let mut visited: HashSet<u32> = HashSet::new();
268
269        fn dfs(
270            node_id: u32,
271            nodes: &BTreeMap<u32, DdnnfNode>,
272            edges: &[DdnnfEdge],
273            outgoing: &BTreeMap<u32, Vec<usize>>,
274            visiting: &mut HashSet<u32>,
275            visited: &mut HashSet<u32>,
276        ) -> Result<()> {
277            if visited.contains(&node_id) {
278                return Ok(());
279            }
280            if !visiting.insert(node_id) {
281                return Err(XlogError::Compilation(format!(
282                    "Decision-DNNF parse error: cycle detected at node {}",
283                    node_id
284                )));
285            }
286
287            let node = nodes.get(&node_id).ok_or_else(|| {
288                XlogError::Compilation(format!(
289                    "Decision-DNNF parse error: unknown node {} during cycle check",
290                    node_id
291                ))
292            })?;
293
294            match node.kind {
295                DdnnfNodeKind::True | DdnnfNodeKind::False => {}
296                DdnnfNodeKind::Or | DdnnfNodeKind::And => {
297                    if let Some(out) = outgoing.get(&node_id) {
298                        for &edge_idx in out {
299                            let edge = &edges[edge_idx];
300                            dfs(edge.to, nodes, edges, outgoing, visiting, visited)?;
301                        }
302                    }
303                }
304            }
305
306            visiting.remove(&node_id);
307            visited.insert(node_id);
308            Ok(())
309        }
310
311        dfs(root, nodes, edges, outgoing, &mut visiting, &mut visited)
312    }
313
314    /// Evaluates the circuit's weighted model count in log space.
315    pub fn eval_log_wmc<F>(&self, var_log_weights: F) -> Result<f64>
316    where
317        F: Fn(u32) -> (f64, f64),
318    {
319        let mut memo: HashMap<u32, f64> = HashMap::new();
320
321        fn eval_node<F>(
322            node_id: u32,
323            ddnnf: &DecisionDnnf,
324            memo: &mut HashMap<u32, f64>,
325            var_log_weights: &F,
326        ) -> Result<f64>
327        where
328            F: Fn(u32) -> (f64, f64),
329        {
330            if let Some(&v) = memo.get(&node_id) {
331                return Ok(v);
332            }
333
334            let node = ddnnf.nodes.get(&node_id).ok_or_else(|| {
335                XlogError::Compilation(format!(
336                    "Decision-DNNF eval error: unknown node {}",
337                    node_id
338                ))
339            })?;
340
341            let value = match node.kind {
342                DdnnfNodeKind::True => 0.0,
343                DdnnfNodeKind::False => f64::NEG_INFINITY,
344                DdnnfNodeKind::And => {
345                    let out = ddnnf.outgoing.get(&node_id).ok_or_else(|| {
346                        XlogError::Compilation(format!(
347                            "Decision-DNNF eval error: AND node {} has no children",
348                            node_id
349                        ))
350                    })?;
351
352                    let mut acc = 0.0;
353                    for &edge_idx in out {
354                        let edge = &ddnnf.edges[edge_idx];
355                        let child = eval_node(edge.to, ddnnf, memo, var_log_weights)?;
356                        let mut lit_sum = 0.0;
357                        for &lit in &edge.lits {
358                            let var = lit.unsigned_abs();
359                            let (t, f) = validate_circuit_log_weight_pair(var_log_weights(var))?;
360                            lit_sum += if lit > 0 { t } else { f };
361                        }
362                        acc += lit_sum + child;
363                    }
364                    acc
365                }
366                DdnnfNodeKind::Or => {
367                    let out = ddnnf.outgoing.get(&node_id).ok_or_else(|| {
368                        XlogError::Compilation(format!(
369                            "Decision-DNNF eval error: OR node {} has no children",
370                            node_id
371                        ))
372                    })?;
373
374                    let mut branch_vals: Vec<f64> = Vec::with_capacity(out.len());
375                    for &edge_idx in out {
376                        let edge = &ddnnf.edges[edge_idx];
377                        let child = eval_node(edge.to, ddnnf, memo, var_log_weights)?;
378                        let mut lit_sum = 0.0;
379                        for &lit in &edge.lits {
380                            let var = lit.unsigned_abs();
381                            let (t, f) = validate_circuit_log_weight_pair(var_log_weights(var))?;
382                            lit_sum += if lit > 0 { t } else { f };
383                        }
384                        branch_vals.push(lit_sum + child);
385                    }
386                    circuit_logsumexp(&branch_vals)?
387                }
388            };
389
390            let value = validate_circuit_value(value)?;
391            memo.insert(node_id, value);
392            Ok(value)
393        }
394
395        eval_node(self.root, self, &mut memo, &var_log_weights)
396    }
397}
398
399#[cfg(test)]
400mod tests {
401    use super::*;
402
403    #[test]
404    fn test_parse_and_eval_identity_variable() {
405        // Represents the formula: x1
406        let nnf = r#"
407o 1 0
408t 2 0
409f 3 0
4101 2 1 0
4111 3 -1 0
412"#;
413
414        let ddnnf = DecisionDnnf::parse_str(nnf).unwrap();
415        assert_eq!(ddnnf.root(), 1);
416        assert_eq!(ddnnf.max_var(), 1);
417
418        let p = 0.3_f64;
419        let log_wmc = ddnnf
420            .eval_log_wmc(|var| match var {
421                1 => (p.ln(), (1.0 - p).ln()),
422                _ => panic!("unexpected var {}", var),
423            })
424            .unwrap();
425
426        assert!((log_wmc - p.ln()).abs() < 1e-9, "log_wmc={}", log_wmc);
427    }
428
429    #[test]
430    fn test_parse_detects_missing_terminator() {
431        let nnf = "t 1";
432        let err = DecisionDnnf::parse_str(nnf).unwrap_err();
433        let msg = err.to_string();
434        assert!(msg.contains("terminator"), "msg={}", msg);
435    }
436}
xlog_prob/kc/ddnnf.rs

xlog_prob/kc/
ddnnf.rs
