Sfoglia il codice sorgente

start a dpll module, just for... fun?

Lucas Stadler 10 anni fa
parent
commit
35ab48ea8d
2 ha cambiato i file con 31 aggiunte e 0 eliminazioni
  1. 30 0
      rust/solve/src/dpll.rs
  2. 1 0
      rust/solve/src/lib.rs

+ 30 - 0
rust/solve/src/dpll.rs

@ -0,0 +1,30 @@
1
use std::collections::BTreeSet;
2
3
type Var = i32;
4
type BoundVars = BTreeSet<Var>;
5
6
fn empty_vars() -> BoundVars {
7
    BTreeSet::new()
8
}
9
10
fn from_vec(v: Vec<Var>) -> BoundVars {
11
    let mut vars = empty_vars();
12
    vars.extend(v);
13
    vars
14
}
15
16
fn is_clause_satisfied(vars: BoundVars, clause: Vec<Var>) -> bool {
17
    for v in clause {
18
        if vars.contains(&v) {
19
            return true
20
        }
21
    }
22
    
23
    return false
24
}
25
26
#[test]
27
fn test_is_clause_satisfied() {
28
    assert!(is_clause_satisfied(from_vec(vec!(1)), vec!(1)));
29
    assert!(!is_clause_satisfied(empty_vars(), vec!(1)));
30
}

+ 1 - 0
rust/solve/src/lib.rs

@ -1,3 +1,4 @@
1 1
//! This is a tiny library for building a SAT solver in Rust.
2 2
3 3
pub mod cnf;
4
pub mod dpll;