Add ng option with heu to binary

Fix various bugs with the nogood learner
2025-12-19 09:29:36 +01:00 · 2022-06-22 17:15:51 +02:00 · 2022-06-22 17:15:51 +02:00 · 86084d7221
commit 86084d7221
parent 5da2c2cf62
8 changed files with 169 additions and 50 deletions
--- a/Cargo.lock
+++ b/Cargo.lock
@ -2,26 +2,11 @@
 # It is not intended for manual editing.
 version = 3

-[[package]]
-name = "adf_bdd"
-version = "0.2.4"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e781519ea5434514f014476c02ccee777b28e600ad58fadca195715acb194c69"
-dependencies = [
- "biodivine-lib-bdd 0.3.0",
- "derivative",
- "lexical-sort",
- "log",
- "nom",
- "serde",
- "serde_json",
-]
-
 [[package]]
 name = "adf_bdd"
 version = "0.2.5"
 dependencies = [
- "biodivine-lib-bdd 0.4.0",
+ "biodivine-lib-bdd",
 "derivative",
 "env_logger 0.9.0",
 "lexical-sort",
@ -32,14 +17,15 @@ dependencies = [
 "roaring",
 "serde",
 "serde_json",
+ "strum",
 "test-log",
 ]

 [[package]]
 name = "adf_bdd-solver"
-version = "0.2.4"
+version = "0.2.5"
 dependencies = [
- "adf_bdd 0.2.4",
+ "adf_bdd",
 "assert_cmd",
 "assert_fs",
 "clap",
@ -48,6 +34,7 @@ dependencies = [
 "predicates",
 "serde",
 "serde_json",
+ "strum",
 ]

 [[package]]
@ -110,16 +97,6 @@ version = "1.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "d468802bab17cbc0cc575e9b053f41e72aa36bfa6b7f55e3529ffa43161b97fa"

-[[package]]
-name = "biodivine-lib-bdd"
-version = "0.3.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "bddcfb460c1131729ec8d797ce0be49ec102506e764ce62f20a40056516851c5"
-dependencies = [
- "fxhash",
- "rand 0.7.3",
-]
-
 [[package]]
 name = "biodivine-lib-bdd"
 version = "0.4.0"
@ -168,16 +145,16 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"

 [[package]]
 name = "clap"
-version = "3.1.18"
+version = "3.2.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d2dbdf4bdacb33466e854ce889eee8dfd5729abf7ccd7664d0a2d60cd384440b"
+checksum = "9f1fe12880bae935d142c8702d500c63a4e8634b6c3c57ad72bf978fc7b6249a"
 dependencies = [
 "atty",
 "bitflags",
 "clap_derive",
 "clap_lex",
 "indexmap",
- "lazy_static",
+ "once_cell",
 "strsim",
 "termcolor",
 "textwrap",
@ -185,9 +162,9 @@ dependencies = [

 [[package]]
 name = "clap_derive"
-version = "3.1.18"
+version = "3.2.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "25320346e922cffe59c0bbc5410c8d8784509efb321488971081313cb1e1a33c"
+checksum = "ed6db9e867166a43a53f7199b5e4d1f522a1e5bd626654be263c999ce59df39a"
 dependencies = [
 "heck",
 "proc-macro-error",
@ -198,9 +175,9 @@ dependencies = [

 [[package]]
 name = "clap_lex"
-version = "0.2.0"
+version = "0.2.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a37c35f1112dad5e6e0b1adaff798507497a18fceeb30cceb3bae7d1427b9213"
+checksum = "87eba3c8c7f42ef17f6c659fc7416d0f4758cd3e58861ee63c5fa4a4dde649e4"
 dependencies = [
 "os_str_bytes",
 ]
@ -515,9 +492,9 @@ dependencies = [

 [[package]]
 name = "once_cell"
-version = "1.9.0"
+version = "1.12.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "da32515d9f6e6e489d7bc9d84c71b060db7247dc035bbe44eac88cf87486d8d5"
+checksum = "7709cef83f0c1f58f666e746a08b21e0085f7440fa6a29cc194d68aac97a4225"

 [[package]]
 name = "os_str_bytes"
@ -742,6 +719,12 @@ dependencies = [
 "retain_mut",
 ]

+[[package]]
+name = "rustversion"
+version = "1.0.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a0a5f7c728f5d284929a1cccb5bc19884422bfe6ef4d6c409da2c41838983fcf"
+
 [[package]]
 name = "ryu"
 version = "1.0.9"
@ -794,6 +777,28 @@ version = "0.10.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "73473c0e59e6d5812c5dfe2a064a6444949f089e20eec9a2e5506596494e4623"

+[[package]]
+name = "strum"
+version = "0.24.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "063e6045c0e62079840579a7e47a355ae92f60eb74daaf156fb1e84ba164e63f"
+dependencies = [
+ "strum_macros",
+]
+
+[[package]]
+name = "strum_macros"
+version = "0.24.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6878079b17446e4d3eba6192bb0a2950d5b14f0ed8424b852310e5a94345d0ef"
+dependencies = [
+ "heck",
+ "proc-macro2",
+ "quote",
+ "rustversion",
+ "syn",
+]
+
 [[package]]
 name = "syn"
 version = "1.0.92"
--- a/bin/Cargo.toml
+++ b/bin/Cargo.toml
@ -1,6 +1,6 @@
 [package]
 name = "adf_bdd-solver"
-version = "0.2.4"
+version = "0.2.5"
 authors = ["Stefan Ellmauthaler <stefan.ellmauthaler@tu-dresden.de>"]
 edition = "2021"
 license = "MIT"
@ -14,12 +14,13 @@ name = "adf-bdd"
 path = "src/main.rs"

 [dependencies]
-adf_bdd = { version="0.2.4", default-features = false }
-clap = {version = "3.1.18", features = [ "derive", "cargo", "env" ]}
+adf_bdd = { version="0.2.5", path="../lib", default-features = false }
+clap = {version = "3.2.6", features = [ "derive", "cargo", "env" ]}
 log = { version = "0.4", features = [ "max_level_trace", "release_max_level_info" ] }
 serde = { version = "1.0", features = ["derive","rc"] }
 serde_json = "1.0"
 env_logger = "0.9"
+strum = { version = "0.24" }

 [dev-dependencies]
 assert_cmd = "2.0"
--- a/bin/src/main.rs
+++ b/bin/src/main.rs
@ -74,6 +74,7 @@ use adf_bdd::adfbiodivine::Adf as BdAdf;

 use adf_bdd::parser::AdfParser;
 use clap::Parser;
+use strum::VariantNames;

 #[derive(Parser, Debug)]
 #[clap(author, version, about)]
@ -84,7 +85,7 @@ struct App {
    /// Sets the verbosity to 'warn', 'info', 'debug' or 'trace' if -v and -q are not use
    #[clap(long = "rust_log", env)]
    rust_log: Option<String>,
-    /// choose the bdd implementation of either 'biodivine', 'naive', or hybrid
+    /// Choose the bdd implementation of either 'biodivine', 'naive', or hybrid
    #[clap(long = "lib", default_value = "hybrid")]
    implementation: String,
    /// Sets log verbosity (multiple times means more verbose)
@ -120,6 +121,12 @@ struct App {
    /// Compute the stable models with a single-formula rewriting on internal representation(only hybrid lib-mode)
    #[clap(long = "stmrew2")]
    stable_rew2: bool,
+    /// Compute the stable models with the nogood-learning based approach
+    #[clap(long = "stmng")]
+    stable_ng: bool,
+    /// Choose which heuristics shall be used by the nogood-learning approach
+    #[clap(long, possible_values = adf_bdd::adf::heuristics::Heuristic::VARIANTS.iter().filter(|&v| v != &"Custom"))]
+    heu: Option<adf_bdd::adf::heuristics::Heuristic<'static>>,
    /// Compute the complete models
    #[clap(long = "com")]
    complete: bool,
@ -244,6 +251,12 @@ impl App {
                        print!("{}", printer.print_interpretation(&model));
                    }
                }
+
+                if self.stable_ng {
+                    for model in naive_adf.stable_nogood(self.heu.unwrap_or_default()) {
+                        print!("{}", printer.print_interpretation(&model));
+                    }
+                }
            }
            "biodivine" => {
                if self.counter.is_some() {
--- a/lib/Cargo.toml
+++ b/lib/Cargo.toml
@ -31,6 +31,7 @@ serde_json = "1.0"
 biodivine-lib-bdd = "0.4.0"
 derivative = "2.2.0"
 roaring = "0.9.0"
+strum = { version = "0.24", features = ["derive"] }

 [dev-dependencies]
 test-log = "0.2"
--- a/lib/src/adf.rs
+++ b/lib/src/adf.rs
@ -815,7 +815,7 @@ impl Adf {
            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()));
+                //stack.push((false, cur_interpr.as_slice().into()));
            } else if !update_ng {
                // No updates done this loop
                if !self.is_two_valued(&cur_interpr) {
@ -832,6 +832,7 @@ impl Adf {
                }
            }
        }
+        log::info!("{ng_store}");
        result
    }
 }
--- a/lib/src/adf/heuristics.rs
+++ b/lib/src/adf/heuristics.rs
@ -5,6 +5,13 @@ In addition there is the public enum [Heuristic], which allows to set a heuristi
 use super::Adf;
 use crate::datatypes::{Term, Var};

+use strum::{EnumString, EnumVariantNames};
+
+/// Return value for heuristics.
+pub type RetVal = Option<(Var, Term)>;
+/// Signature for heuristics functions.
+pub type HeuristicFn = dyn Fn(&Adf, &[Term]) -> RetVal;
+
 pub(crate) fn heu_simple(_adf: &Adf, interpr: &[Term]) -> Option<(Var, Term)> {
    for (idx, term) in interpr.iter().enumerate() {
        if !term.is_truth_value() {
@ -14,25 +21,59 @@ pub(crate) fn heu_simple(_adf: &Adf, interpr: &[Term]) -> Option<(Var, Term)> {
    None
 }

-/// Return value for heuristics.
-pub type RetVal = Option<(Var, Term)>;
-/// Signature for heuristics functions.
-pub type HeuristicFn = dyn Fn(&Adf, &[Term]) -> RetVal;
+pub(crate) fn heu_mc_minpaths_maxvarimp(adf: &Adf, interpr: &[Term]) -> Option<(Var, Term)> {
+    interpr
+        .iter()
+        .enumerate()
+        .filter(|(_var, term)| !term.is_truth_value())
+        .min_by(|(vara, &terma), (varb, &termb)| {
+            match adf
+                .bdd
+                .paths(terma, true)
+                .minimum()
+                .cmp(&adf.bdd.paths(termb, true).minimum())
+            {
+                std::cmp::Ordering::Equal => adf
+                    .bdd
+                    .passive_var_impact(Var::from(*vara), interpr)
+                    .cmp(&adf.bdd.passive_var_impact(Var::from(*varb), interpr)),
+                value => value,
+            }
+        })
+        .map(|(var, term)| {
+            (
+                Var::from(var),
+                (!adf.bdd.paths(*term, true).more_models()).into(),
+            )
+        })
+}

 /// Enumeration of all currently implemented heuristics.
 /// It represents a public view on the crate-view implementations of heuristics.
+#[derive(EnumString, EnumVariantNames, Copy, Clone)]
 pub enum Heuristic<'a> {
    /// Implementation of a simple heuristic.
    /// This will just take the first not decided variable and maps it value to (`true`)[Term::TOP].   
    Simple,
+    /// Implementation of a heuristic, which which uses minimal number of [paths][crate::obdd::Bdd::paths] and maximal [variable-impact][crate::obdd::Bdd::passive_var_impact to identify the variable to be set.
+    /// As the value of the variable value with the minimal model-path is chosen.
+    MinModMinPathsMaxVarImp,
    /// Allow passing in an externally-defined custom heuristic.
+    #[strum(disabled)]
    Custom(&'a HeuristicFn),
 }

+impl Default for Heuristic<'_> {
+    fn default() -> Self {
+        Self::Simple
+    }
+}
+
 impl std::fmt::Debug for Heuristic<'_> {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Simple => write!(f, "Simple"),
+	    Self::MinModMinPathsMaxVarImp => write!(f, "Minimal model count as value and minimum paths with maximal variable impact as variable choice"),
            Self::Custom(_) => f.debug_tuple("Custom function").finish(),
        }
    }
@ -42,7 +83,23 @@ impl Heuristic<'_> {
    pub(crate) fn get_heuristic(&self) -> &(dyn Fn(&Adf, &[Term]) -> RetVal + '_) {
        match self {
            Heuristic::Simple => &heu_simple,
+            Heuristic::MinModMinPathsMaxVarImp => &heu_mc_minpaths_maxvarimp,
            Self::Custom(f) => f,
        }
    }
 }
+
+// impl FromStr for Heuristic<'_> {
+//     type Err = ();
+
+//     fn from_str(s: &str) -> Result<Self, Self::Err> {
+//         match s {
+//             "simple" => Ok(Self::Simple),
+//             "MinmcMinpathsMaxvarimp" => Ok(Self::MinModMinPathsMaxVarImp),
+//             _ => {
+//                 log::info!("Unknown heuristic {s}");
+//                 Err(())
+//             }
+//         }
+//     }
+// }
--- a/lib/src/datatypes/bdd.rs
+++ b/lib/src/datatypes/bdd.rs
@ -25,6 +25,16 @@ impl From<usize> for Term {
    }
 }

+impl From<bool> for Term {
+    fn from(val: bool) -> Self {
+        if val {
+            Self::TOP
+        } else {
+            Self::BOT
+        }
+    }
+}
+
 impl From<&biodivine_lib_bdd::Bdd> for Term {
    fn from(val: &biodivine_lib_bdd::Bdd) -> Self {
        if val.is_true() {
--- a/lib/src/nogoods.rs
+++ b/lib/src/nogoods.rs
@ -2,7 +2,8 @@

 use std::{
    borrow::Borrow,
-    ops::{BitAnd, BitOr, BitXor},
+    fmt::Display,
+    ops::{BitAnd, BitOr, BitXor, BitXorAssign},
 };

 use crate::datatypes::Term;
@ -117,12 +118,22 @@ impl NoGood {
            .borrow()
            .bitxor(other.active.borrow())
            .bitand(self.active.borrow());
-        if implication.len() == 1 {
+
+        let bothactive = self.active.borrow().bitand(other.active.borrow());
+        let mut no_matches = bothactive.borrow().bitand(other.value.borrow());
+        no_matches.bitxor_assign(bothactive.bitand(self.value.borrow()));
+
+        if implication.len() == 1 && no_matches.is_empty() {
            let pos = implication
                .min()
                .expect("just checked that there is one element to be found");
+            log::trace!(
+                "Conclude {:?}",
+                Some((pos as usize, !self.value.contains(pos)))
+            );
            Some((pos as usize, !self.value.contains(pos)))
        } else {
+            log::trace!("Nothing to Conclude");
            None
        }
    }
@ -175,6 +186,16 @@ pub struct NoGoodStore {
    duplicates: DuplicateElemination,
 }

+impl Display for NoGoodStore {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        writeln!(f, "NoGoodStats: [")?;
+        for (arity, vec) in self.store.iter().enumerate() {
+            writeln!(f, "{arity}: {}", vec.len())?;
+        }
+        write!(f, "]")
+    }
+}
+
 impl NoGoodStore {
    /// Creates a new [NoGoodStore] and assumes a size compatible with the underlying [NoGood] implementation.
    pub fn new(size: u32) -> NoGoodStore {
@ -227,6 +248,7 @@ impl NoGoodStore {
    /// *Returns* [None] if there is a conflict
    pub fn conclusions(&self, nogood: &NoGood) -> Option<NoGood> {
        let mut result = nogood.clone();
+        log::trace!("ng-store: {:?}", self.store);
        self.store
            .iter()
            .enumerate()
@ -236,6 +258,7 @@ impl NoGoodStore {
            })
            .try_fold(&mut result, |acc, ng| {
                if ng.is_violating(acc) {
+                    log::trace!("ng conclusion violating");
                    None
                } else {
                    acc.disjunction(&ng);
@ -261,7 +284,15 @@ impl NoGoodStore {
    pub(crate) fn conclusion_closure(&self, interpretation: &[Term]) -> ClosureResult {
        let mut update = true;
        let mut result = match self.conclusions(&interpretation.into()) {
-            Some(val) => val.update_term_vec(interpretation, &mut update),
+            Some(val) => {
+                log::trace!(
+                    "conclusion-closure step 1: val:{:?} -> {:?}",
+                    val,
+                    val.update_term_vec(interpretation, &mut update)
+                );
+                val.update_term_vec(interpretation, &mut update)
+            }
+
            None => return ClosureResult::Inconsistent,
        };
        if !update {
@ -786,7 +817,7 @@ mod test {

        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)])
+            ClosureResult::Update(vec![Term(1), Term(0), Term(3), Term(9), Term(0), Term(1)])
        );
    }
 }