Add nogood-algorithm to the ADF

add additional test cases, fixed a bug in the ng-learner module

lib/src/adf.rs

@@ -5,6 +5,10 @@ This module describes the abstract dialectical framework.
  - computing fixpoints
 */
 
+pub mod heuristics;
+
+use std::cmp::Ordering;
+
 use serde::{Deserialize, Serialize};
 
 use crate::{
@@ -15,6 +19,7 @@ use crate::{
         },
         FacetCounts, ModelCounts, Term, Var,
     },
+    nogoods::{NoGood, NoGoodStore},
     obdd::Bdd,
     parser::{AdfParser, Formula},
 };
@@ -405,6 +410,10 @@ impl Adf {
         true
     }
 
+    fn is_two_valued(&self, interpretation: &[Term]) -> bool {
+        interpretation.iter().all(|t| t.is_truth_value())
+    }
+
     fn two_val_model_counts<H>(&mut self, interpr: &[Term], heuristic: H) -> Vec<Vec<Term>>
     where
         H: Fn(&Self, (Var, Term), (Var, Term), &[Term]) -> std::cmp::Ordering + Copy,
@@ -590,6 +599,26 @@ impl Adf {
         }
     }
 
+    /// Constructs the fixpoint of the given interpretation with respect to the ADF.
+    /// sets _update_ to [`true`] if the value has been updated and to [`false`] otherwise.
+    fn update_interpretation_fixpoint_upd(
+        &mut self,
+        interpretation: &[Term],
+        update: &mut bool,
+    ) -> Vec<Term> {
+        let mut cur_int = interpretation.to_vec();
+        *update = false;
+        loop {
+            let new_int = self.update_interpretation(interpretation);
+            if cur_int == new_int {
+                return cur_int;
+            } else {
+                cur_int = new_int;
+                *update = true;
+            }
+        }
+    }
+
     fn update_interpretation(&mut self, interpretation: &[Term]) -> Vec<Term> {
         self.apply_interpretation(interpretation, interpretation)
     }
@@ -697,6 +726,101 @@ impl Adf {
             })
             .collect::<Vec<_>>()
     }
+
+    fn stable_nogood<H>(&mut self, interpretation: &[Term], heuristic: H) -> Vec<Vec<Term>>
+    where
+        H: Fn(&Self, &[Term]) -> Option<(Var, Term)>,
+    {
+        let mut result = Vec::new();
+        let mut cur_interpr = interpretation.to_vec();
+        let mut ng_store = NoGoodStore::new(
+            self.ac
+                .len()
+                .try_into()
+                .expect("Expecting only u32 many statements"),
+        );
+        let mut stack: Vec<(bool, NoGood)> = Vec::new();
+        let mut interpr_history: Vec<Vec<Term>> = Vec::new();
+        let mut backtrack = false;
+        let mut update_ng = true;
+        let mut update_fp = false;
+        let mut choice = false;
+
+        log::debug!("start learning loop");
+        loop {
+            log::trace!("interpr: {:?}", cur_interpr);
+            log::trace!("choice: {}", choice);
+            if choice {
+                choice = false;
+                if let Some((var, term)) = heuristic(&*self, &cur_interpr) {
+                    log::trace!("choose {}->{}", var, term.is_true());
+                    interpr_history.push(cur_interpr.to_vec());
+                    cur_interpr[var.value()] = term;
+                    stack.push((true, cur_interpr.as_slice().into()));
+                } else {
+                    backtrack = true;
+                }
+            }
+            update_ng = true;
+            log::trace!("backtrack: {}", backtrack);
+            if backtrack {
+                backtrack = false;
+                if stack.is_empty() {
+                    break;
+                }
+                while let Some((choice, ng)) = stack.pop() {
+                    log::trace!("adding ng: {:?}", ng);
+                    ng_store.add_ng(ng);
+
+                    if choice {
+                        cur_interpr = interpr_history.pop().expect("both stacks (interpr_history and `stack`) should always be synchronous");
+                        log::trace!(
+                            "choice found, reverting interpretation to {:?}",
+                            cur_interpr
+                        );
+                        break;
+                    }
+                }
+            }
+            match ng_store.conclusion_closure(&cur_interpr) {
+                crate::nogoods::ClosureResult::Update(new_int) => {
+                    cur_interpr = new_int;
+                    log::trace!("ng update: {:?}", cur_interpr);
+                    stack.push((false, cur_interpr.as_slice().into()));
+                }
+                crate::nogoods::ClosureResult::NoUpdate => {
+                    log::trace!("no update");
+                    update_ng = false;
+                }
+                crate::nogoods::ClosureResult::Inconsistent => {
+                    log::trace!("inconsistency");
+                    backtrack = true;
+                    continue;
+                }
+            }
+
+            cur_interpr = self.update_interpretation_fixpoint_upd(&cur_interpr, &mut update_fp);
+            if update_fp {
+                log::trace!("fixpount updated");
+                stack.push((false, cur_interpr.as_slice().into()));
+            } else if !update_ng {
+                // No updates done this loop
+                if !self.is_two_valued(&cur_interpr) {
+                    choice = true;
+                } else if self.stability_check(&cur_interpr) {
+                    // stable model found
+                    stack.push((false, cur_interpr.as_slice().into()));
+                    result.push(cur_interpr.clone());
+                    backtrack = true;
+                } else {
+                    // not stable
+                    stack.push((false, cur_interpr.as_slice().into()));
+                    backtrack = true;
+                }
+            }
+        }
+        result
+    }
 }
 
 #[cfg(test)]
@@ -882,6 +1006,29 @@ mod test {
         assert_eq!(adf.stable_count_optimisation_heu_b().next(), None);
     }
 
+    #[test]
+    fn stable_nogood() {
+        let parser = AdfParser::default();
+        parser.parse()("s(a).s(b).s(c).s(d).ac(a,c(v)).ac(b,b).ac(c,and(a,b)).ac(d,neg(b)).\ns(e).ac(e,and(b,or(neg(b),c(f)))).s(f).\n\nac(f,xor(a,e)).")
+            .unwrap();
+        let mut adf = Adf::from_parser(&parser);
+
+        let grounded = adf.grounded();
+        let stable = adf.stable_nogood(&grounded, crate::adf::heuristics::heu_simple);
+
+        assert_eq!(
+            stable,
+            vec![vec![
+                Term::TOP,
+                Term::BOT,
+                Term::BOT,
+                Term::TOP,
+                Term::BOT,
+                Term::TOP
+            ]]
+        );
+    }
+
     #[test]
     fn complete() {
         let parser = AdfParser::default();

lib/src/nogoods.rs

@@ -42,6 +42,17 @@ impl NoGood {
         result
     }
 
+    /// Creates a [NoGood] representing an atomic assignment.
+    pub fn new_single_nogood(pos: usize, val: bool) -> NoGood {
+        let mut result = Self::default();
+        let pos:u32 = pos.try_into().expect("nog-good learner implementation is based on the assumption that only u32::MAX-many variables are in place");
+        result.active.insert(pos);
+        if val {
+            result.value.insert(pos);
+        }
+        result
+    }
+
     /// Returns [None] if the pair contains inconsistent pairs.
     /// Otherwise it returns a [NoGood] which represents the set values.
     pub fn try_from_pair_iter(
@@ -231,7 +242,7 @@ impl NoGoodStore {
             .filter(|(len, _vec)| *len <= nogood.len())
             .any(|(_, vec)| {
                 vec.iter()
-                    .any(|elem| result.is_violating(elem) || elem.is_violating(nogood))
+                    .any(|elem| elem.is_violating(&result) || elem.is_violating(nogood))
             })
         {
             return None;
@@ -383,6 +394,8 @@ mod test {
         assert!(!ng1.is_violating(&ng4));
         assert!(ng2.is_violating(&ng3));
         assert!(!ng3.is_violating(&ng2));
+
+        assert_eq!(ng4, NoGood::new_single_nogood(0, true));
     }
 
     #[test]
@@ -639,6 +652,35 @@ mod test {
         ];
 
         assert_eq!(ngs.conclusions(&interpr.as_slice().into()), None);
+
+        ngs = NoGoodStore::new(6);
+        ngs.add_ng(
+            [Term(1), Term(1), Term(1), Term(0), Term(0), Term(1)]
+                .as_slice()
+                .into(),
+        );
+        ngs.add_ng(
+            [Term(1), Term(1), Term(8), Term(0), Term(0), Term(11)]
+                .as_slice()
+                .into(),
+        );
+        ngs.add_ng([Term(22), Term(1)].as_slice().into());
+
+        assert_eq!(
+            ngs.conclusions(
+                &[Term(1), Term(3), Term(3), Term(9), Term(0), Term(1)]
+                    .as_slice()
+                    .into(),
+            ),
+            Some(NoGood::from_term_vec(&[
+                Term(1),
+                Term(0),
+                Term(3),
+                Term(9),
+                Term(0),
+                Term(1)
+            ]))
+        );
     }
 
     #[test]
@@ -717,5 +759,23 @@ mod test {
                 .expect_err("just checked that it is an error"),
             "Inconsistency occurred"
         );
+
+        ngs = NoGoodStore::new(6);
+        ngs.add_ng(
+            [Term(1), Term(1), Term(1), Term(0), Term(0), Term(1)]
+                .as_slice()
+                .into(),
+        );
+        ngs.add_ng(
+            [Term(1), Term(1), Term(8), Term(0), Term(0), Term(11)]
+                .as_slice()
+                .into(),
+        );
+        ngs.add_ng([Term(22), Term(1)].as_slice().into());
+
+        assert_eq!(
+            ngs.conclusion_closure(&[Term(1), Term(3), Term(3), Term(9), Term(0), Term(1)]),
+            ClosureResult::Update(vec![Term(1), Term(0), Term(0), Term(1), Term(0), Term(1)])
+        );
     }
 }