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.
 
 

57 lines
1.4 KiB

// vim: ts=4 sw=4 et
use crate::clause::*;
fn bfs_step(cs: &ClauseList, vs: &Vec<Variable>, n: usize) -> usize {
if n == vs.len() {
let r = cs
.iter()
.filter_map(|c| c.eval())
.map(|b| if b { 1 } else { 0 })
.sum();
#[cfg(debug_bfs)]
println!("{}\t= {}", cs, r);
r
} 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)
}
}
fn bfs_step_bounded(cs: &ClauseList, vs: &Vec<Variable>, n: usize, bound: usize) -> bool {
if n == vs.len() {
let r: usize = cs
.iter()
.filter_map(|c| c.eval())
.map(|b| if b { 1 } else { 0 })
.sum();
#[cfg(debug_bfs)]
println!("{}\t= {}", cs, r);
r == bound
} else {
let a = {
vs[n].assign(false);
bfs_step_bounded(cs, vs, n + 1, bound)
};
if a {
true
} else {
{
vs[n].assign(true);
bfs_step_bounded(cs, vs, n + 1, bound)
}
}
}
}
pub fn solve_by_bfs(cs: &ClauseList) -> usize {
let vars: Vec<Variable> = cs.get_vars().into_iter().collect();
let bound = bfs_step(cs, &vars, 0);
bfs_step_bounded(cs, &vars, 0, bound);
bound
}