1
0
mirror of https://github.com/ellmau/adf-obdd.git synced 2025-12-19 09:29:36 +01:00

Add new heuristics approach

Selecting the minimal number of paths in the bdds, then choosing
variable with the highest impact.
This commit is contained in:
Stefan Ellmauthaler 2022-04-04 12:56:12 +02:00
parent b6fbb23626
commit 8d9e7f09e1
Failed to extract signature

View File

@ -404,20 +404,7 @@ impl Adf {
will_be: &[Term], will_be: &[Term],
depth: usize, depth: usize,
) -> Vec<Vec<Term>> { ) -> Vec<Vec<Term>> {
let cacheitem = interpr
.iter()
.enumerate()
.map(|(idx, val)| *val.min(&will_be[idx]))
.collect::<Vec<Term>>();
if !self.callcache.insert(cacheitem) {
panic!("trying to check the same model candidate twice");
return Vec::new();
}
log::trace!("two_val_model_counts({:?}) called", interpr);
log::debug!("two_val_model_recursion_depth: {}/{}", depth, interpr.len()); log::debug!("two_val_model_recursion_depth: {}/{}", depth, interpr.len());
//for (idx, &ac) in interpr.iter().enumerate() {
// log::trace!("idx{}, ac: Term({}), modelc-/+: {:?}, depth:{}, impact: {}, num_interpr+: {}, num interpr-: {}", idx, ac, self.bdd.models(ac, true), self.bdd.max_depth(ac), self.bdd.var_impact(Var(idx),interpr), self.bdd.interpretations(ac, true, Var(idx), &[], &[]).len(),self.bdd.interpretations(ac, false, Var(idx), &[], &[]).len());
//}
if let Some((idx, ac)) = interpr if let Some((idx, ac)) = interpr
.iter() .iter()
.enumerate() .enumerate()
@ -425,20 +412,21 @@ impl Adf {
.min_by(|(idx_a, val_a), (idx_b, val_b)| { .min_by(|(idx_a, val_a), (idx_b, val_b)| {
match self match self
.bdd .bdd
.var_impact(Var(*idx_b), interpr) .paths(**val_a, true)
.cmp(&self.bdd.var_impact(Var(*idx_a), interpr)) .minimum()
.cmp(&self.bdd.paths(**val_b, true).minimum())
{ {
// if the minimal counts are equal, choose the maximal var_impact // if the minimal counts are equal, choose the maximal var_impact
std::cmp::Ordering::Equal => self std::cmp::Ordering::Equal => self
.bdd .bdd
.max_depth(**val_a) .var_impact(Var(*idx_b), interpr)
.cmp(&self.bdd.max_depth(**val_b)), .cmp(&self.bdd.var_impact(Var(*idx_a), interpr)),
value => value, value => value,
} }
}) })
{ {
let mut result = Vec::new(); let mut result = Vec::new();
let check_models = !self.bdd.models(*ac, true).more_models(); let check_models = !self.bdd.paths(*ac, true).more_models();
log::trace!( log::trace!(
"Identified Var({}) with ac {:?} to be {}", "Identified Var({}) with ac {:?} to be {}",
idx, idx,