|
|
@ -74,36 +74,36 @@ fn test_is_unknown() {
|
|
74
|
74
|
}
|
|
75
|
75
|
|
|
76
|
76
|
/// A satisfied clause is a clause where at least one atom is true.
|
|
77
|
|
fn is_clause_satisfied(vars: &BoundVars, clause: Clause) -> bool {
|
|
|
77
|
fn is_clause_satisfied(vars: &BoundVars, clause: &Clause) -> bool {
|
|
78
|
78
|
clause.iter().any(|v| is_true(vars, *v))
|
|
79
|
79
|
}
|
|
80
|
80
|
|
|
81
|
81
|
#[test]
|
|
82
|
82
|
fn test_is_clause_satisfied() {
|
|
83
|
|
assert!(is_clause_satisfied(&from_vec(vec!(1)), vec!(1)));
|
|
84
|
|
assert!(!is_clause_satisfied(&empty_vars(), vec!(1)));
|
|
|
83
|
assert!(is_clause_satisfied(&from_vec(vec!(1)), &vec!(1)));
|
|
|
84
|
assert!(!is_clause_satisfied(&empty_vars(), &vec!(1)));
|
|
85
|
85
|
}
|
|
86
|
86
|
|
|
87
|
87
|
/// A conflict clause is a clause whose atoms each are false.
|
|
88
|
|
fn is_clause_conflict(vars: &BoundVars, clause: Clause) -> bool {
|
|
|
88
|
fn is_clause_conflict(vars: &BoundVars, clause: &Clause) -> bool {
|
|
89
|
89
|
clause.iter().all(|v| is_false(vars, *v))
|
|
90
|
90
|
}
|
|
91
|
91
|
|
|
92
|
92
|
#[test]
|
|
93
|
93
|
fn test_is_clause_conflict() {
|
|
94
|
|
assert!(is_clause_conflict(&from_vec(vec!(-1)), vec!(1)));
|
|
95
|
|
assert!(is_clause_conflict(&from_vec(vec!(-1, -2, -3)), vec!(1, 2, 3)));
|
|
96
|
|
assert!(is_clause_conflict(&from_vec(vec!(-1, -2, -3, 4)), vec!(1, 2, 3)));
|
|
97
|
|
assert!(!is_clause_conflict(&from_vec(vec!(1)), vec!(1)));
|
|
98
|
|
assert!(!is_clause_conflict(&from_vec(vec!(2)), vec!(1, 2)));
|
|
|
94
|
assert!(is_clause_conflict(&from_vec(vec!(-1)), &vec!(1)));
|
|
|
95
|
assert!(is_clause_conflict(&from_vec(vec!(-1, -2, -3)), &vec!(1, 2, 3)));
|
|
|
96
|
assert!(is_clause_conflict(&from_vec(vec!(-1, -2, -3, 4)), &vec!(1, 2, 3)));
|
|
|
97
|
assert!(!is_clause_conflict(&from_vec(vec!(1)), &vec!(1)));
|
|
|
98
|
assert!(!is_clause_conflict(&from_vec(vec!(2)), &vec!(1, 2)));
|
|
99
|
99
|
}
|
|
100
|
100
|
|
|
101
|
101
|
/// A unit clause is a clause where one atom is unknown and all
|
|
102
|
102
|
/// others are false.
|
|
103
|
|
fn is_clause_unit(vars: &BoundVars, clause: Clause) -> bool {
|
|
|
103
|
fn is_clause_unit(vars: &BoundVars, clause: &Clause) -> bool {
|
|
104
|
104
|
let mut unknowns = 0;
|
|
105
|
105
|
|
|
106
|
|
for v in clause {
|
|
|
106
|
for &v in clause {
|
|
107
|
107
|
if is_unknown(vars, v) {
|
|
108
|
108
|
unknowns += 1
|
|
109
|
109
|
}
|
|
|
@ -119,12 +119,12 @@ fn is_clause_unit(vars: &BoundVars, clause: Clause) -> bool {
|
|
119
|
119
|
#[test]
|
|
120
|
120
|
fn test_is_clause_unit() {
|
|
121
|
121
|
let vars = &from_vec(vec!(1, 2));
|
|
122
|
|
assert!(is_clause_unit(vars, vec!(3)));
|
|
123
|
|
assert!(is_clause_unit(vars, vec!(-1, 3)));
|
|
124
|
|
assert!(is_clause_unit(vars, vec!(-1, -2, 3)));
|
|
125
|
|
assert!(!is_clause_unit(vars, vec!(1, 3)));
|
|
126
|
|
assert!(!is_clause_unit(vars, vec!(1, 2, 3)));
|
|
127
|
|
assert!(!is_clause_unit(vars, vec!(1, 2)));
|
|
|
122
|
assert!(is_clause_unit(vars, &vec!(3)));
|
|
|
123
|
assert!(is_clause_unit(vars, &vec!(-1, 3)));
|
|
|
124
|
assert!(is_clause_unit(vars, &vec!(-1, -2, 3)));
|
|
|
125
|
assert!(!is_clause_unit(vars, &vec!(1, 3)));
|
|
|
126
|
assert!(!is_clause_unit(vars, &vec!(1, 2, 3)));
|
|
|
127
|
assert!(!is_clause_unit(vars, &vec!(1, 2)));
|
|
128
|
128
|
}
|
|
129
|
129
|
|
|
130
|
130
|
pub fn dpll(clauses: Vec<Clause>) -> Option<BoundVars> {
|
|
|
@ -132,10 +132,10 @@ pub fn dpll(clauses: Vec<Clause>) -> Option<BoundVars> {
|
|
132
|
132
|
let mut vars = &mut empty_vars();
|
|
133
|
133
|
|
|
134
|
134
|
loop {
|
|
135
|
|
if clauses.iter().all(|c| is_clause_satisfied(&vars, c.clone())) { // all clauses satisfied, success
|
|
|
135
|
if clauses.iter().all(|c| is_clause_satisfied(&vars, c)) { // all clauses satisfied, success
|
|
136
|
136
|
//println!("satisfied");
|
|
137
|
137
|
return Some(vars.clone())
|
|
138
|
|
} else if clauses.iter().any(|c| is_clause_conflict(&vars, c.clone())) { // a conflict exists, backtrack
|
|
|
138
|
} else if clauses.iter().any(|c| is_clause_conflict(&vars, c)) { // a conflict exists, backtrack
|
|
139
|
139
|
match stack.pop() {
|
|
140
|
140
|
None => return None, // nothing to backtrack, no solution found
|
|
141
|
141
|
Some((v, b)) => {
|
|
|
@ -144,9 +144,9 @@ pub fn dpll(clauses: Vec<Clause>) -> Option<BoundVars> {
|
|
144
|
144
|
vars.insert(v);
|
|
145
|
145
|
}
|
|
146
|
146
|
}
|
|
147
|
|
} else if clauses.iter().any(|c| is_clause_unit(&vars, c.clone())) { // a unit clause exists, propagate
|
|
|
147
|
} else if clauses.iter().any(|c| is_clause_unit(&vars, c)) { // a unit clause exists, propagate
|
|
148
|
148
|
let cs = clauses.clone();
|
|
149
|
|
let clause = cs.iter().find(|&c| is_clause_unit(&vars, c.clone())).unwrap();
|
|
|
149
|
let clause = cs.iter().find(|&c| is_clause_unit(&vars, c)).unwrap();
|
|
150
|
150
|
let unknown = *clause.iter().find(|&v| is_unknown(&vars, *v)).unwrap();
|
|
151
|
151
|
//println!("propagate {} from {:?}", unknown, clause);
|
|
152
|
152
|
vars.insert(unknown);
|