mirror of
https://github.com/ellmau/adf-obdd.git
synced 2025-12-19 09:29:36 +01:00
Add a random heuristic, based on rand-crate (#96)
* Add a random heuristic, based on rand-crate * Add cryptographically strong seed option
This commit is contained in:
parent
ebbf8de684
commit
495f9c893f
15
Cargo.lock
generated
15
Cargo.lock
generated
@ -32,6 +32,7 @@ dependencies = [
|
|||||||
"nom",
|
"nom",
|
||||||
"quickcheck",
|
"quickcheck",
|
||||||
"quickcheck_macros",
|
"quickcheck_macros",
|
||||||
|
"rand 0.8.5",
|
||||||
"roaring",
|
"roaring",
|
||||||
"serde",
|
"serde",
|
||||||
"serde_json",
|
"serde_json",
|
||||||
@ -622,7 +623,7 @@ checksum = "6a6b1679d49b24bbfe0c803429aa1874472f50d9b363131f0e89fc356b544d03"
|
|||||||
dependencies = [
|
dependencies = [
|
||||||
"getrandom 0.1.16",
|
"getrandom 0.1.16",
|
||||||
"libc",
|
"libc",
|
||||||
"rand_chacha",
|
"rand_chacha 0.2.2",
|
||||||
"rand_core 0.5.1",
|
"rand_core 0.5.1",
|
||||||
"rand_hc",
|
"rand_hc",
|
||||||
]
|
]
|
||||||
@ -633,6 +634,8 @@ version = "0.8.5"
|
|||||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
checksum = "34af8d1a0e25924bc5b7c43c079c942339d8f0a8b57c39049bef581b46327404"
|
checksum = "34af8d1a0e25924bc5b7c43c079c942339d8f0a8b57c39049bef581b46327404"
|
||||||
dependencies = [
|
dependencies = [
|
||||||
|
"libc",
|
||||||
|
"rand_chacha 0.3.1",
|
||||||
"rand_core 0.6.3",
|
"rand_core 0.6.3",
|
||||||
]
|
]
|
||||||
|
|
||||||
@ -646,6 +649,16 @@ dependencies = [
|
|||||||
"rand_core 0.5.1",
|
"rand_core 0.5.1",
|
||||||
]
|
]
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "rand_chacha"
|
||||||
|
version = "0.3.1"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "e6c10a63a0fa32252be49d21e7709d4d4baf8d231c2dbce1eaa8141b9b127d88"
|
||||||
|
dependencies = [
|
||||||
|
"ppv-lite86",
|
||||||
|
"rand_core 0.6.3",
|
||||||
|
]
|
||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
name = "rand_core"
|
name = "rand_core"
|
||||||
version = "0.5.1"
|
version = "0.5.1"
|
||||||
|
|||||||
@ -33,6 +33,7 @@ derivative = "2.2.0"
|
|||||||
roaring = "0.9.0"
|
roaring = "0.9.0"
|
||||||
strum = { version = "0.24", features = ["derive"] }
|
strum = { version = "0.24", features = ["derive"] }
|
||||||
crossbeam-channel = "0.5"
|
crossbeam-channel = "0.5"
|
||||||
|
rand = {version = "0.8.5", features = ["std_rng"]}
|
||||||
|
|
||||||
[dev-dependencies]
|
[dev-dependencies]
|
||||||
test-log = "0.2"
|
test-log = "0.2"
|
||||||
|
|||||||
@ -6,6 +6,8 @@ This module describes the abstract dialectical framework.
|
|||||||
*/
|
*/
|
||||||
|
|
||||||
pub mod heuristics;
|
pub mod heuristics;
|
||||||
|
use std::cell::RefCell;
|
||||||
|
|
||||||
use crate::{
|
use crate::{
|
||||||
datatypes::{
|
datatypes::{
|
||||||
adf::{
|
adf::{
|
||||||
@ -18,6 +20,7 @@ use crate::{
|
|||||||
obdd::Bdd,
|
obdd::Bdd,
|
||||||
parser::{AdfParser, Formula},
|
parser::{AdfParser, Formula},
|
||||||
};
|
};
|
||||||
|
use rand::{rngs::StdRng, SeedableRng};
|
||||||
use serde::{Deserialize, Serialize};
|
use serde::{Deserialize, Serialize};
|
||||||
|
|
||||||
use self::heuristics::Heuristic;
|
use self::heuristics::Heuristic;
|
||||||
@ -30,6 +33,8 @@ pub struct Adf {
|
|||||||
ordering: VarContainer,
|
ordering: VarContainer,
|
||||||
bdd: Bdd,
|
bdd: Bdd,
|
||||||
ac: Vec<Term>,
|
ac: Vec<Term>,
|
||||||
|
#[serde(skip, default = "Adf::default_rng")]
|
||||||
|
rng: RefCell<StdRng>,
|
||||||
}
|
}
|
||||||
|
|
||||||
impl Default for Adf {
|
impl Default for Adf {
|
||||||
@ -38,6 +43,7 @@ impl Default for Adf {
|
|||||||
ordering: VarContainer::default(),
|
ordering: VarContainer::default(),
|
||||||
bdd: Bdd::new(),
|
bdd: Bdd::new(),
|
||||||
ac: Vec::new(),
|
ac: Vec::new(),
|
||||||
|
rng: Adf::default_rng(),
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
@ -50,6 +56,7 @@ impl Adf {
|
|||||||
ordering: parser.var_container(),
|
ordering: parser.var_container(),
|
||||||
bdd: Bdd::new(),
|
bdd: Bdd::new(),
|
||||||
ac: vec![Term(0); parser.dict_size()],
|
ac: vec![Term(0); parser.dict_size()],
|
||||||
|
rng: Adf::default_rng(),
|
||||||
};
|
};
|
||||||
(0..parser.dict_size()).into_iter().for_each(|value| {
|
(0..parser.dict_size()).into_iter().for_each(|value| {
|
||||||
log::trace!("adding variable {}", Var(value));
|
log::trace!("adding variable {}", Var(value));
|
||||||
@ -85,6 +92,7 @@ impl Adf {
|
|||||||
ordering: ordering.clone(),
|
ordering: ordering.clone(),
|
||||||
bdd: Bdd::new(),
|
bdd: Bdd::new(),
|
||||||
ac: vec![Term(0); bio_ac.len()],
|
ac: vec![Term(0); bio_ac.len()],
|
||||||
|
rng: Adf::default_rng(),
|
||||||
};
|
};
|
||||||
result
|
result
|
||||||
.ac
|
.ac
|
||||||
@ -134,6 +142,15 @@ impl Adf {
|
|||||||
result
|
result
|
||||||
}
|
}
|
||||||
|
|
||||||
|
fn default_rng() -> RefCell<StdRng> {
|
||||||
|
RefCell::new(StdRng::from_entropy())
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Sets a cryptographiclly strong seed
|
||||||
|
pub fn seed(&mut self, seed: [u8; 32]) {
|
||||||
|
self.rng = RefCell::new(StdRng::from_seed(seed))
|
||||||
|
}
|
||||||
|
|
||||||
/// Instantiates a new ADF, based on a [biodivine adf][crate::adfbiodivine::Adf].
|
/// Instantiates a new ADF, based on a [biodivine adf][crate::adfbiodivine::Adf].
|
||||||
pub fn from_biodivine(bio_adf: &super::adfbiodivine::Adf) -> Self {
|
pub fn from_biodivine(bio_adf: &super::adfbiodivine::Adf) -> Self {
|
||||||
Self::from_biodivine_vector(bio_adf.var_container(), bio_adf.ac())
|
Self::from_biodivine_vector(bio_adf.var_container(), bio_adf.ac())
|
||||||
@ -1232,6 +1249,25 @@ mod test {
|
|||||||
solving.join().unwrap();
|
solving.join().unwrap();
|
||||||
}
|
}
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn rand_stable_heu() {
|
||||||
|
let parser = AdfParser::default();
|
||||||
|
parser.parse()("s(a).s(b).ac(a,neg(b)).ac(b,neg(a)).").unwrap();
|
||||||
|
let mut adf = Adf::from_parser(&parser);
|
||||||
|
let result = adf.stable_nogood(Heuristic::Rand).collect::<Vec<_>>();
|
||||||
|
assert!(result.contains(&vec![Term(0), Term(1)]));
|
||||||
|
assert!(result.contains(&vec![Term(1), Term(0)]));
|
||||||
|
assert_eq!(result.len(), 2);
|
||||||
|
|
||||||
|
let mut adf = Adf::from_parser(&parser);
|
||||||
|
adf.seed([
|
||||||
|
122, 186, 240, 42, 235, 102, 89, 81, 187, 203, 127, 188, 167, 198, 126, 156, 25, 205,
|
||||||
|
204, 132, 112, 93, 23, 193, 21, 108, 166, 231, 158, 250, 128, 135,
|
||||||
|
]);
|
||||||
|
let result = adf.stable_nogood(Heuristic::Rand).collect::<Vec<_>>();
|
||||||
|
assert_eq!(result, vec![vec![Term(1), Term(0)], vec![Term(0), Term(1)]]);
|
||||||
|
}
|
||||||
|
|
||||||
#[test]
|
#[test]
|
||||||
fn complete() {
|
fn complete() {
|
||||||
let parser = AdfParser::default();
|
let parser = AdfParser::default();
|
||||||
|
|||||||
@ -5,6 +5,7 @@ In addition there is the public enum [Heuristic], which allows to set a heuristi
|
|||||||
use super::Adf;
|
use super::Adf;
|
||||||
use crate::datatypes::{Term, Var};
|
use crate::datatypes::{Term, Var};
|
||||||
|
|
||||||
|
use rand::{Rng, RngCore};
|
||||||
use strum::{EnumString, EnumVariantNames};
|
use strum::{EnumString, EnumVariantNames};
|
||||||
|
|
||||||
/// Return value for heuristics.
|
/// Return value for heuristics.
|
||||||
@ -76,6 +77,23 @@ pub(crate) fn heu_mc_maxvarimp_minpaths(adf: &Adf, interpr: &[Term]) -> Option<(
|
|||||||
})
|
})
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pub(crate) fn heu_rand(adf: &Adf, interpr: &[Term]) -> Option<(Var, Term)> {
|
||||||
|
let possible = interpr
|
||||||
|
.iter()
|
||||||
|
.enumerate()
|
||||||
|
.filter(|(_var, term)| !term.is_truth_value())
|
||||||
|
.collect::<Vec<_>>();
|
||||||
|
if possible.is_empty() {
|
||||||
|
return None;
|
||||||
|
}
|
||||||
|
let mut rng = adf.rng.borrow_mut();
|
||||||
|
if let Ok(position) = usize::try_from(rng.next_u64() % (possible.len() as u64)) {
|
||||||
|
Some((Var::from(position), rng.gen_bool(0.5).into()))
|
||||||
|
} else {
|
||||||
|
None
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
/// Enumeration of all currently implemented heuristics.
|
/// Enumeration of all currently implemented heuristics.
|
||||||
/// It represents a public view on the crate-view implementations of heuristics.
|
/// It represents a public view on the crate-view implementations of heuristics.
|
||||||
#[derive(EnumString, EnumVariantNames, Copy, Clone)]
|
#[derive(EnumString, EnumVariantNames, Copy, Clone)]
|
||||||
@ -89,6 +107,8 @@ pub enum Heuristic<'a> {
|
|||||||
/// Implementation of a heuristic, which which uses maximal [variable-impact][crate::obdd::Bdd::passive_var_impact] and minimal number of [paths][crate::obdd::Bdd::paths] to identify the variable to be set.
|
/// Implementation of a heuristic, which which uses maximal [variable-impact][crate::obdd::Bdd::passive_var_impact] and minimal number of [paths][crate::obdd::Bdd::paths] to identify the variable to be set.
|
||||||
/// As the value of the variable value with the maximal model-path is chosen.
|
/// As the value of the variable value with the maximal model-path is chosen.
|
||||||
MinModMaxVarImpMinPaths,
|
MinModMaxVarImpMinPaths,
|
||||||
|
/// Implementation of a heuristic, which chooses random values.
|
||||||
|
Rand,
|
||||||
/// Allow passing in an externally-defined custom heuristic.
|
/// Allow passing in an externally-defined custom heuristic.
|
||||||
#[strum(disabled)]
|
#[strum(disabled)]
|
||||||
Custom(&'a HeuristicFn),
|
Custom(&'a HeuristicFn),
|
||||||
@ -106,6 +126,7 @@ impl std::fmt::Debug for Heuristic<'_> {
|
|||||||
Self::Simple => write!(f, "Simple"),
|
Self::Simple => write!(f, "Simple"),
|
||||||
Self::MinModMinPathsMaxVarImp => write!(f, "Maximal model-path count as value and minimum paths with maximal variable impact as variable choice"),
|
Self::MinModMinPathsMaxVarImp => write!(f, "Maximal model-path count as value and minimum paths with maximal variable impact as variable choice"),
|
||||||
Self::MinModMaxVarImpMinPaths => write!(f, "Maximal model-path count as value and maximal variable impact with minimum paths as variable choice"),
|
Self::MinModMaxVarImpMinPaths => write!(f, "Maximal model-path count as value and maximal variable impact with minimum paths as variable choice"),
|
||||||
|
Self::Rand => write!(f, "Random heuristics"),
|
||||||
Self::Custom(_) => f.debug_tuple("Custom function").finish(),
|
Self::Custom(_) => f.debug_tuple("Custom function").finish(),
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
@ -117,6 +138,7 @@ impl Heuristic<'_> {
|
|||||||
Heuristic::Simple => &heu_simple,
|
Heuristic::Simple => &heu_simple,
|
||||||
Heuristic::MinModMinPathsMaxVarImp => &heu_mc_minpaths_maxvarimp,
|
Heuristic::MinModMinPathsMaxVarImp => &heu_mc_minpaths_maxvarimp,
|
||||||
Heuristic::MinModMaxVarImpMinPaths => &heu_mc_maxvarimp_minpaths,
|
Heuristic::MinModMaxVarImpMinPaths => &heu_mc_maxvarimp_minpaths,
|
||||||
|
Heuristic::Rand => &heu_rand,
|
||||||
Self::Custom(f) => f,
|
Self::Custom(f) => f,
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
@ -132,6 +154,7 @@ mod test {
|
|||||||
dbg!(Heuristic::Simple);
|
dbg!(Heuristic::Simple);
|
||||||
dbg!(Heuristic::MinModMaxVarImpMinPaths);
|
dbg!(Heuristic::MinModMaxVarImpMinPaths);
|
||||||
dbg!(Heuristic::MinModMinPathsMaxVarImp);
|
dbg!(Heuristic::MinModMinPathsMaxVarImp);
|
||||||
|
dbg!(Heuristic::Rand);
|
||||||
dbg!(Heuristic::Custom(&|_adf: &Adf,
|
dbg!(Heuristic::Custom(&|_adf: &Adf,
|
||||||
_int: &[Term]|
|
_int: &[Term]|
|
||||||
-> Option<(Var, Term)> { None }));
|
-> Option<(Var, Term)> { None }));
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user