[DPLL] Initialize Watch length with # of literals

src/report.rs

@@ -12,7 +12,7 @@ impl std::fmt::Debug for Report {
 
         if let Some(source) = self.0.source() {
             writeln!(f, "\n\nCaused by:")?;
-            for (i, e) in std::iter::successors(Some(source), |e| e.source()).enumerate() {
+            for (i, e) in std::iter::successors(Some(source), |e| e.clone().source()).enumerate() {
                 writeln!(f, "  {}: {}", i, e)?;
             }
         }

src/solver/dpll.rs

@@ -17,10 +17,10 @@ mod inner {
     }
 
     impl Watch {
-        pub fn new(clauses: &[Clause]) -> Self {
+        pub fn new(clauses: &[Clause], num_variabels: usize) -> Self {
             let mut watch = Self {
-                positive: vec![Vec::new(); clauses.len()],
-                negative: vec![Vec::new(); clauses.len()],
+                positive: vec![Vec::new(); num_variabels],
+                negative: vec![Vec::new(); num_variabels],
             };
 
             for (idx, clause) in clauses.iter().enumerate() {
@@ -171,7 +171,7 @@ impl Solver for DpllSolver {
         let num_variables = formula.num_variables();
         let num_clauses = formula.clauses().len();
 
-        let watch = Watch::new(formula.clauses());
+        let watch = Watch::new(formula.clauses(), num_variables);
         let assignment = vec![None; num_variables];
         let clause_stats = vec![Default::default(); num_clauses];
 

src/tests.rs

@@ -63,6 +63,8 @@ sat_testcase!(satch_cnfs, unit7);
 unsat_testcase!(satch_cnfs, unit8);
 unsat_testcase!(satch_cnfs, unit9);
 
+sat_testcase!(satch_cnfs, var4clause3);
+
 unsat_testcase!(satch_cnfs, full2);
 unsat_testcase!(satch_cnfs, full3);
 unsat_testcase!(satch_cnfs, full4);

testcases/satch_cnfs/var4clause3.cnf

@@ -0,0 +1,4 @@
+p cnf 4 3
+-1 2 0
+-2 -3 0
+3 -4 0