microsat/
solver.rs

1use crate::cnf::{to_variable, Assignment};
2use crate::dpll::solve_dpll;
3use crate::expression::{self, Expression};
4use std::sync::mpsc;
5
6fn verify_assignment(expression: &Expression, assignment: &Assignment) -> bool {
7    for clause in expression.get_clauses() {
8        let mut satisfied = false;
9        for literal in clause.literals() {
10            let term = to_variable(*literal);
11            let sign = *literal > 0;
12
13            // The clause is satisfied as long as a literal's assignment matches its sign
14            // Aka, if the literal is positive, the assignment must be true
15            // If the literal is negative, the assignment must be false (making the literal true when it is negated)
16            if assignment[&term] == sign {
17                satisfied = true;
18                break;
19            }
20        }
21
22        if !satisfied {
23            return false;
24        }
25    }
26
27    return true;
28}
29
30pub fn solve(expression: Expression, use_multiple_threads: bool, verify: bool) -> Option<Assignment> {
31    let mut expression_max_literals = expression.clone();
32    let mut expression_min_clause_len = expression.clone();
33
34    let (send_channel, recv_channel) = mpsc::channel();
35    let send_channel_copy = send_channel.clone();
36
37    std::thread::spawn(move || {
38        expression_max_literals.optimize();
39        expression_max_literals
40            .set_heuristic(expression::SolverHeuristic::MostLiteralOccurances);
41
42        let result = solve_dpll(&mut expression_max_literals);
43        let _ = send_channel.send(result);
44    });
45
46    if use_multiple_threads {
47        std::thread::spawn(move || {
48            expression_min_clause_len.optimize();
49            expression_min_clause_len
50                .set_heuristic(expression::SolverHeuristic::MinimizeClauseLength);
51    
52            let result = solve_dpll(&mut expression_min_clause_len);
53            let _ = send_channel_copy.send(result);
54        });
55    }
56
57    let solution = recv_channel.recv().expect("Could not receive result from solver.");
58    if solution.is_some() && verify {
59        let assignment = solution.clone().unwrap();
60        if !verify_assignment(&expression, &assignment) {
61            panic!("Solution is invalid!");
62        }
63    }
64
65    return solution;
66}
67
68// Tests
69
70#[cfg(test)]
71mod tests {
72    use super::*;
73    use crate::cnf::{Clause, CNF};
74    use crate::expression::Expression;
75
76    #[test]
77    fn test_verify_assignment() {
78        let mut expression = Expression::new();
79        let mut clause = Clause::new();
80        clause.insert_checked(1);
81        clause.insert_checked(-2);
82        expression.add_clause(clause);
83
84        let mut assignment = Assignment::new();
85        assignment.insert(1, true);
86        assignment.insert(2, false);
87
88        assert!(verify_assignment(&expression, &assignment));
89    }
90
91    #[test]
92    fn test_verify_assignment_unsatisfied() {
93        let mut expression = Expression::new();
94        let mut clause = Clause::new();
95        clause.insert_checked(1);
96        clause.insert_checked(2);
97        expression.add_clause(clause);
98
99        let mut assignment = Assignment::new();
100        assignment.insert(1, false);
101        assignment.insert(2, false);
102
103        assert!(!verify_assignment(&expression, &assignment));
104    }
105
106    #[test]
107    fn test_verify_assignment_unsatisfied_multiple_clauses() {
108        let mut expression = Expression::new();
109        let mut clause = Clause::new();
110        clause.insert_checked(1);
111        clause.insert_checked(2);
112        expression.add_clause(clause);
113
114        let mut clause = Clause::new();
115        clause.insert_checked(-3);
116        clause.insert_checked(-4);
117        expression.add_clause(clause);
118
119        let mut assignment = Assignment::new();
120        assignment.insert(1, false);
121        assignment.insert(2, false);
122        assignment.insert(3, true);
123        assignment.insert(4, true);
124
125        assert!(!verify_assignment(&expression, &assignment));
126    }
127
128    #[test]
129    fn test_verify_assignment_satisfied_multiple_clauses() {
130        let mut expression = Expression::new();
131        let mut clause = Clause::new();
132        clause.insert_checked(1);
133        clause.insert_checked(-2);
134        expression.add_clause(clause);
135
136        let mut clause = Clause::new();
137        clause.insert_checked(3);
138        clause.insert_checked(-4);
139        expression.add_clause(clause);
140
141        let mut assignment = Assignment::new();
142        assignment.insert(1, true);
143        assignment.insert(2, false);
144        assignment.insert(3, true);
145        assignment.insert(4, false);
146
147        assert!(verify_assignment(&expression, &assignment));
148    }
149
150}
microsat/solver.rs

microsat/
solver.rs
