From 86084d722173bb2fe59ace77cf8b87ca86c2e1d6 Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Wed, 22 Jun 2022 17:15:51 +0200 Subject: [PATCH] Add ng option with heu to binary Fix various bugs with the nogood learner --- Cargo.lock | 79 +++++++++++++++++++++------------------ bin/Cargo.toml | 7 ++-- bin/src/main.rs | 15 +++++++- lib/Cargo.toml | 1 + lib/src/adf.rs | 3 +- lib/src/adf/heuristics.rs | 65 ++++++++++++++++++++++++++++++-- lib/src/datatypes/bdd.rs | 10 +++++ lib/src/nogoods.rs | 39 +++++++++++++++++-- 8 files changed, 169 insertions(+), 50 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index c7931f7..43e85e4 100644 --- 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" diff --git a/bin/Cargo.toml b/bin/Cargo.toml index 79cef0e..33a8cb0 100644 --- 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 "] 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" diff --git a/bin/src/main.rs b/bin/src/main.rs index 13fb052..5bac810 100644 --- 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, - /// 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>, /// 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() { diff --git a/lib/Cargo.toml b/lib/Cargo.toml index c5a39e2..98a8007 100644 --- 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" diff --git a/lib/src/adf.rs b/lib/src/adf.rs index e51c274..9106951 100644 --- 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 } } diff --git a/lib/src/adf/heuristics.rs b/lib/src/adf/heuristics.rs index ccfc642..7e7eb23 100644 --- 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 { +// match s { +// "simple" => Ok(Self::Simple), +// "MinmcMinpathsMaxvarimp" => Ok(Self::MinModMinPathsMaxVarImp), +// _ => { +// log::info!("Unknown heuristic {s}"); +// Err(()) +// } +// } +// } +// } diff --git a/lib/src/datatypes/bdd.rs b/lib/src/datatypes/bdd.rs index b1c2975..5324b03 100644 --- a/lib/src/datatypes/bdd.rs +++ b/lib/src/datatypes/bdd.rs @@ -25,6 +25,16 @@ impl From for Term { } } +impl From 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() { diff --git a/lib/src/nogoods.rs b/lib/src/nogoods.rs index 155e4cf..07e15c1 100644 --- 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 { 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)]) ); } }