Solving MAXSAT and saying a few words about it.
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

#### 86 lines 2.3 KiB Raw Blame History

 `// vim: ts=4 sw=4 et` `use crate::clause::*;` `/*` ` * Produces a unique variable name from a given usize. The variable name is` ` * always lower case and will extend to a longer name should the number be` ` * larger than 25. For reference, 0 maps to 'a' and 26 maps to 'aa'.` ` */` `fn get_var_name(n: usize) -> String {` ` let ch = std::char::from_u32((n as u32) % 26 + 0x61)` ` .unwrap()` ` .to_string();` ` if n >= 26 {` ` get_var_name(n / 26) + &ch` ` } else {` ` ch` ` }` `}` `/*` ` * Returns a list of integers from 0 to (n-1) in a random order.` ` */` `fn get_rand_list(n: usize) -> Vec {` ` let mut int_list: Vec = (0..n).collect();` ` let mut r_list: Vec = Vec::new();` ` for _ in 0..n {` ` let idx: usize = rand::random::() % int_list.len();` ` r_list.push(int_list.remove(idx));` ` }` ` r_list` `}` `/*` ` * Generates a random clause from a slice of variables.` ` */` `pub fn gen_clause(var_list: &[Variable]) -> Clause {` ` let mut cl = Clause::new();` ` for i in get_rand_list(var_list.len()) {` ` cl.push(var_list[i].get_literal(rand::random()));` ` }` ` cl` `}` `/*` ` * Generates a list of clauses that has [count] clauses that will have up to` ` * [max_vars] literals in them. No empty clauses are generated.` ` */` `pub fn gen_clause_list(count: usize, max_vars: usize) -> ClauseList {` ` let mut cls = ClauseList::new();` ` let vars: Vec = get_rand_list(max_vars)` ` .into_iter()` ` .map(get_var_name)` ` .map(Variable::from_name)` ` .collect();` ` for _ in 0..count {` ` let idx = rand::random::() % (max_vars - 1) + 1;` ` cls.push(gen_clause(vars.split_at(idx).0));` ` }` ` cls` `}` `#[cfg(test)]` `mod test {` ` use super::*;` ` #[test]` ` fn test_clause_gen() {` ` let test_var_short = get_var_name(1);` ` let test_var_long = get_var_name(27);` ` println!("{}, {}", test_var_short, test_var_long);` ` assert!(test_var_short == "b");` ` assert!(test_var_long == "bb");` ` let test_clause = gen_clause(10);` ` println!("{}", test_clause);` ` assert!(test_clause.len() == 10);` ` let test_clause_list = gen_clause_list(5, 4);` ` assert!(test_clause_list.len() == 5);` ` for cl in test_clause_list.iter() {` ` println!("{}", cl);` ` assert!(cl.len() <= 4 && cl.len() > 0);` ` }` ` }` ```} ```