Browse Source

Merge branch 'master' of gitea:thajohns/cs451-project

master
Cameron Weinfurt 3 years ago
parent
commit
3dab188e17
  1. 23
      src/clause.rs
  2. 30
      src/clause_gen.rs
  3. 2
      src/main.rs
  4. 12
      src/maxsat.rs

23
src/clause.rs

@ -183,7 +183,10 @@ impl Display for Literal {
macro_rules! nd {
($($s:literal)?$(, $coln:ident, $colt:ident)?) => {
if self.neg {
cd!($($s)?, "¬", $($coln, $colt)?)
#[cfg(not(no_unicode))]
{ cd!($($s)?, "¬", $($coln, $colt)?) }
#[cfg(no_unicode)]
{ cd!($($s)?, "~", $($coln, $colt)?) }
} else {
cd!($($s)?, , $($coln, $colt)?)
}
@ -265,11 +268,19 @@ impl Display for Clause {
fn fmt(&self, fmt: &mut Formatter) -> core::fmt::Result {
if self.literals.len() == 0 {
write!(fmt, "NULL")
} else {
let mut iter = self.literals.iter();
write!(fmt, "{}", iter.next().unwrap())?;
for lit in iter {
#[cfg(not(no_unicode))]
{
write!(fmt, "⊥")
}
#[cfg(no_unicode)]
{
write!(fmt, "FALSE")
}
write!(fmt, " V {}", lit)?;
#[cfg(not(no_unicode))]
write!(fmt, " ∨ {}", lit)?;
#[cfg(no_unicode)]
write!(fmt, " v {}", lit)?;
}
Ok(())
}
@ -457,7 +468,7 @@ mod test {
y.get_name(),
z.get_name(),
w.get_name()
);
);
println!("x: {}, y: {}, z: {}, w: {}", x, y, z, w);
assign_vars! {
x = 1;

30
src/clause_gen.rs

@ -1,3 +1,5 @@
// vim: ts=4 sw=4 et
use crate::clause::*;
/*
@ -6,7 +8,9 @@ use crate::clause::*;
* 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();
let ch = std::char::from_u32((n as u32) % 26 + 0x61)
.unwrap()
.to_string();
if n >= 26 {
get_var_name(n / 26) + &ch
} else {
@ -18,20 +22,20 @@ fn get_var_name(n: usize) -> String {
* Generates a clause with [var_count] literals that are randomly negated.
*/
pub fn gen_clause(var_count: usize) -> Clause {
let mut vars : Vec<Literal> = (0..var_count)
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()
}
)
.map(|v| {
if rand::random() {
v.get_pos_literal()
} else {
v.get_neg_literal()
}
})
.collect();
let mut cl = Clause::new();
for _ in 0..var_count {
let idx : usize = rand::random::<usize>() % vars.len();
let idx: usize = rand::random::<usize>() % vars.len();
cl.push(vars.remove(idx));
}
cl
@ -39,7 +43,7 @@ pub fn gen_clause(var_count: usize) -> Clause {
/*
* Generates a list of clauses that has [count] clauses that will have up to
* [max_vars] literals in them. No empty clauses are generated.
* [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();
@ -51,8 +55,8 @@ pub fn gen_clause_list(count: usize, max_vars: usize) -> ClauseList {
#[cfg(test)]
mod test {
use super::*;
use super::*;
#[test]
fn test_clause_gen() {
let test_var_short = get_var_name(1);

2
src/main.rs

@ -3,9 +3,9 @@
#[macro_use]
/// Useful for disjunctive clauses and variables.
pub mod clause;
mod clause_gen;
/// I made this before I knew I didn't need it. :/
pub mod hash_wrapper;
mod messy_minsat;
mod maxsat;
mod clause_gen;

12
src/maxsat.rs

@ -1,16 +1,19 @@
// vim: ts=4 sw=4 et
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()
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);
let rf = bfs_step(cs, vs, n + 1);
vs[n].assign(true);
let rt = bfs_step(cs, vs, n+1);
let rt = bfs_step(cs, vs, n + 1);
usize::max(rt, rf)
}
@ -20,4 +23,3 @@ 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