Browse Source

Fixed the same-name duplicate variables problem

master
Cameron Weinfurt 3 years ago
parent
commit
f16a957366
  1. 41
      src/clause_gen.rs
  2. 2
      src/main.rs
  3. 6
      src/maxsat.rs

41
src/clause_gen.rs

@ -19,24 +19,25 @@ fn get_var_name(n: usize) -> String {
}
/*
* Generates a clause with [var_count] literals that are randomly negated.
* Returns a list of integers from 0 to (n-1) in a random order.
*/
pub fn gen_clause(var_count: usize) -> Clause {
let mut vars: Vec<Literal> = (0..var_count)
.map(get_var_name)
.map(Variable::from_name)
.map(|v| {
if rand::random() {
v.get_pos_literal()
} else {
v.get_neg_literal()
}
})
.collect();
fn get_rand_list(n : usize) -> Vec<usize> {
let mut int_list : Vec<usize> = (0..n).collect();
let mut r_list : Vec<usize> = Vec::new();
for _ in 0..n {
let idx: usize = rand::random::<usize>() % 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 _ in 0..var_count {
let idx: usize = rand::random::<usize>() % vars.len();
cl.push(vars.remove(idx));
for i in get_rand_list(var_list.len()) {
cl.push(var_list[i].get_literal(rand::random()));
}
cl
}
@ -47,8 +48,14 @@ pub fn gen_clause(var_count: usize) -> Clause {
*/
pub fn gen_clause_list(count: usize, max_vars: usize) -> ClauseList {
let mut cls = ClauseList::new();
let vars : Vec<Variable> = get_rand_list(max_vars)
.into_iter()
.map(get_var_name)
.map(Variable::from_name)
.collect();
for _ in 0..count {
cls.push(gen_clause(rand::random::<usize>() % (max_vars) + 1));
let idx = rand::random::<usize>() % (max_vars - 1) + 1;
cls.push(gen_clause(vars.split_at(idx).0));
}
cls
}

2
src/main.rs

@ -12,7 +12,7 @@ use crate::clause_gen::*;
use crate::maxsat::*;
fn main() {
let rand_clause_list = gen_clause_list(5, 5);
let rand_clause_list = gen_clause_list(7, 4);
println!("{}", rand_clause_list);
println!("MAXSAT (By BFS): {}", solve_by_bfs(&rand_clause_list));
}

6
src/maxsat.rs

@ -4,10 +4,12 @@ use crate::clause::*;
fn bfs_step(cs: &ClauseList, vs: &Vec<Variable>, n: usize) -> usize {
if n == vs.len() {
cs.iter()
let r = cs.iter()
.filter_map(|c| c.eval())
.map(|b| if b { 1 } else { 0 })
.sum()
.sum();
println!("{}\t= {}", cs, r);
r
} else {
vs[n].assign(false);
let rf = bfs_step(cs, vs, n + 1);

Loading…
Cancel
Save