Progress with cdcl

src/cdcl.rs

@@ -10,6 +10,13 @@ enum StateItem {
     Unknown,
 }
 
+#[derive(Debug, Clone, Copy)]
+enum ClauseState {
+    Satisfied,
+    UnitPropagate(Index),
+    Unknown,
+}
+
 #[derive(Debug, Clone)]
 struct State {
     map: Vec<StateItem>,
@@ -36,12 +43,79 @@ impl State {
         self.set_literal(l);
     }
 
-    fn add_literal_propagate(&mut self, l: Index, cnf: &NormalForm) -> Result<(), Vec<Index>> {
+    fn add_literal_propagate(
+        &mut self,
+        l: Index,
+        source_slice: &[Index],
+        cnf: &NormalForm,
+    ) -> Result<(), Vec<Index>> {
+        for &i in source_slice.iter().filter(|&&i| i != l) {
+            self.graph.push((i, l));
+        }
+
+        if let Some(NormalFormIteratorItem {
+            slice,
+            len: _,
+            index: _,
+        }) = cnf.iter().find(
+            |&NormalFormIteratorItem {
+                 slice,
+                 len: _,
+                 index: _,
+             }| {
+                match self.get_clause_state(slice) {
+                    ClauseState::UnitPropagate(other) => other == -l,
+                    _ => false,
+                }
+            },
+        ) {
+            let mut conflict: Vec<_> = source_slice
+                .iter()
+                .copied()
+                .filter(|&i| i != l)
+                .chain(slice.iter().copied().filter(|&i| i != -l))
+                .collect();
+            conflict.sort();
+            conflict.dedup();
+
+            return Err(conflict);
+        }
+
         self.set_literal(l);
 
         Ok(())
     }
 
+    fn get_clause_state(&self, s: &[Index]) -> ClauseState {
+        let mut unknown_literal = None;
+        for &l in s {
+            match self.get_literal(l) {
+                StateItem::True => {
+                    if l > 0 {
+                        return ClauseState::Satisfied;
+                    }
+                }
+                StateItem::False => {
+                    if l < 0 {
+                        return ClauseState::Satisfied;
+                    }
+                }
+                StateItem::Unknown => {
+                    if unknown_literal.is_some() {
+                        return ClauseState::Unknown;
+                    } else {
+                        unknown_literal = Some(l);
+                    }
+                }
+            }
+        }
+
+        match unknown_literal {
+            Some(l) => ClauseState::UnitPropagate(l),
+            None => panic!("Fully false clause."),
+        }
+    }
+
     fn get_literal(&self, l: Index) -> StateItem {
         self.map[l.unsigned_abs() as usize - 1]
     }
@@ -84,28 +158,25 @@ impl State {
 }
 
 fn unit_propagate(cnf: &NormalForm, state: &mut State) -> Result<(), Vec<Index>> {
-    if let Some(nfii) = cnf.iter().find(
+    if let Some(NormalFormIteratorItem {
+        slice,
+        len: _,
+        index: _,
+    }) = cnf.iter().find(
         |NormalFormIteratorItem {
              slice,
              len: _,
              index: _,
-         }| {
-            slice
-                .iter()
-                .filter(|&&l| state.is_unknown_literal(l))
-                .count()
-                == 1
-        },
+         }| { matches!(state.get_clause_state(slice), ClauseState::UnitPropagate(_)) },
     ) {
-        let i = nfii
-            .slice
+        let i = slice
             .iter()
             .position(|&i| state.is_unknown_literal(i))
             .unwrap();
 
-        let l = nfii.slice[i];
+        let l = slice[i];
 
-        state.add_literal_propagate(l, cnf)?;
+        state.add_literal_propagate(l, slice, cnf)?;
 
         unit_propagate(cnf, state)
     } else {
@@ -116,36 +187,34 @@ fn unit_propagate(cnf: &NormalForm, state: &mut State) -> Result<(), Vec<Index>>
 fn cdcl_internal(cnf: &mut NormalForm, mut state: State) -> Result<State, Vec<Index>> {
     unit_propagate(cnf, &mut state)?;
 
-    dbg!(&state);
-
-    if state.is_complete() {
-        return Ok(state);
-    }
-
-    let l = state.get_arbitrary_literal().unwrap();
+    let l = match state.get_arbitrary_literal() {
+        Some(l) => l,
+        None => return Ok(state),
+    };
 
     let mut state_clone = state.clone();
     state_clone.add_literal_arbitrary(l);
 
     match cdcl_internal(cnf, state_clone) {
-        Ok(_) => todo!(),
-        Err(_) => todo!(),
-    };
+        Ok(s) => Ok(s),
+        Err(c) => {
+            let count_unknown_literals =
+                c.iter().filter(|&&i| !state.is_unknown_literal(i)).count();
 
-    let mut state_clone = state.clone();
-    state_clone.add_literal_arbitrary(-l);
+            if count_unknown_literals >= 2 || (count_unknown_literals == c.len()) {
+                cnf.add_clause(&c);
 
-    match cdcl_internal(cnf, state_clone) {
-        Ok(_) => todo!(),
-        Err(_) => todo!(),
-    };
-
-    Ok(state)
+                cdcl_internal(cnf, state)
+            } else {
+                Err(c)
+            }
+        }
+    }
 }
 
-pub fn cdcl(mut cnf: &mut NormalForm) -> Option<Vec<Index>> {
+pub fn cdcl(cnf: &mut NormalForm) -> Option<Vec<Index>> {
     let num_literals = cnf.get_num_literals();
-    match cdcl_internal(&mut cnf, State::new(num_literals)) {
+    match cdcl_internal(cnf, State::new(num_literals)) {
         Ok(state) => {
             if state.is_complete() {
                 Some(state.get_solution())