Browse Source

Implemented BFS-based solver as benchmark

clause_generator
Cameron Weinfurt 3 years ago
parent
commit
19f14f8bc3
  1. 1
      src/main.rs
  2. 23
      src/maxsat.rs

1
src/main.rs

@ -6,5 +6,6 @@ pub mod clause;
/// I made this before I knew I didn't need it. :/
pub mod hash_wrapper;
mod messy_minsat;
mod maxsat;
fn main() {}

23
src/maxsat.rs

@ -0,0 +1,23 @@
use crate::clause::*;
fn bfs_step(cs: &ClauseList, vs: &Vec<Variable>, n: usize) -> usize {
if n == vs.len() {
cs.iter().filter_map(|c| c.eval())
.map(|b| if b { 1 } else { 0 }).sum()
} else {
vs[n].assign(false);
let rf = bfs_step(cs, vs, n+1);
vs[n].assign(true);
let rt = bfs_step(cs, vs, n+1);
usize::max(rt, rf)
}
}
pub fn solve_by_bfs(cs: &ClauseList) -> usize {
let vars: Vec<Variable> = cs.get_vars().into_iter().collect();
bfs_step(cs, &vars, 0)
}
Loading…
Cancel
Save