dpll/
dpll.rs

1use std::{error::Error, rc::Rc};
2
3use branch_and_bound::{Subproblem, SubproblemResolution};
4
5mod dpll_core;
6use dpll_core::*;
7
8pub struct Node {
9    clauses: Rc<Vec<Clause>>,
10    vars_left: Rc<Vec<u32>>,
11    vars_left_idx: usize,
12    assignments: Vec<i8>,
13}
14
15impl Subproblem for Node {
16    // We never need to compare solutions to each other. We just need to find any.
17    // Thus, `Score` is the unit type.
18    type Score = ();
19
20    fn bound(&self) -> Self::Score {}
21
22    fn branch_or_evaluate(&mut self) -> SubproblemResolution<Self, Self::Score> {
23        let mut unknown_count = 0;
24        // Eager assignments
25        for clause in self.clauses.as_ref() {
26            match clause.eval(&self.assignments) {
27                ClauseState::Known(false) => {
28                    return SubproblemResolution::Branched(Box::new(std::iter::empty()));
29                }
30                ClauseState::Known(true) => {}
31                ClauseState::Unknown => unknown_count += 1,
32                ClauseState::OneLeft(literal) => {
33                    // Assign a variable eagerly. May break other clauses - in the worst case,
34                    // checked when processing children.
35                    assert_ne!(literal, 0);
36                    self.assignments[literal.unsigned_abs() as usize] = literal.signum() as i8;
37                }
38            }
39        }
40
41        if unknown_count == 0 {
42            return SubproblemResolution::Solved(());
43        }
44
45        let vars_left = self.vars_left.as_ref();
46        let mut var_idx = self.vars_left_idx;
47        while var_idx < vars_left.len() {
48            let &var = &vars_left[var_idx];
49
50            if self.assignments[var as usize] != 0 {
51                // Already eagerly assigned. Skip to the next variable
52                var_idx += 1;
53                continue;
54            }
55
56            let mut child_true = Node {
57                clauses: self.clauses.clone(),
58                vars_left: self.vars_left.clone(),
59                vars_left_idx: var_idx + 1,
60                assignments: self.assignments.clone(),
61            };
62            child_true.assignments[var as usize] = 1;
63
64            let mut child_false = Node {
65                clauses: self.clauses.clone(),
66                vars_left: self.vars_left.clone(),
67                vars_left_idx: var_idx + 1,
68                assignments: self.assignments.clone(),
69            };
70            child_false.assignments[var as usize] = -1;
71
72            return SubproblemResolution::Branched(Box::new([child_true, child_false].into_iter()));
73        }
74
75        // The initial validation did not detect that the formula is decided,
76        // but we ran out of variables to check. This only happens if we've
77        // managed to eagerly assign the last variable. So, just perform the
78        // final validation!
79        Node {
80            clauses: self.clauses.clone(),
81            vars_left: self.vars_left.clone(),
82            vars_left_idx: var_idx,
83            assignments: self.assignments.clone(),
84        }
85        .branch_or_evaluate()
86    }
87}
88
89fn solve(parsed: &CnfSat) -> Option<Vec<i8>> {
90    let problem = Node {
91        clauses: Rc::new(parsed.clauses.clone()),
92        vars_left: Rc::new(parsed.vars_by_frequency.clone()),
93        vars_left_idx: 0,
94        assignments: vec![0; 1 + parsed.vars_cnt as usize],
95    };
96
97    branch_and_bound::solve(problem, branch_and_bound::TraverseMethod::DepthFirst)
98        .map(|n| n.assignments)
99}
100
101fn main() -> Result<(), Box<dyn Error>> {
102    examples_main()
103}
dpll/dpll.rs

dpll/
dpll.rs
