From 0faf1284df8ffadf030dcca72503c05ca3b6315c Mon Sep 17 00:00:00 2001
From: hal8174 <henning.lindemann@pm.me>
Date: Sun, 3 Nov 2024 14:09:06 +0100
Subject: [PATCH] Working cdcl implentation?

---
 sat/wikipedia.sat |  1 -
 src/cdcl.rs       | 31 ++++++++++++++++++++++---------
 src/main.rs       |  1 -
 3 files changed, 22 insertions(+), 11 deletions(-)

diff --git a/sat/wikipedia.sat b/sat/wikipedia.sat
index b3b218a..e71b07c 100644
--- a/sat/wikipedia.sat
+++ b/sat/wikipedia.sat
@@ -6,4 +6,3 @@ x2 | x11
 !x7 | x8 | !x9
 x7 | x8 | !x10
 x7 | x10 | !x12
-x1
diff --git a/src/cdcl.rs b/src/cdcl.rs
index 677d771..c497251 100644
--- a/src/cdcl.rs
+++ b/src/cdcl.rs
@@ -69,6 +69,8 @@ impl State {
                 }
             },
         ) {
+            // println!("Source: {source_slice:?}");
+            // println!("Slice: {slice:?}");
             let mut conflict: Vec<_> = source_slice
                 .iter()
                 .copied()
@@ -112,7 +114,9 @@ impl State {
 
         match unknown_literal {
             Some(l) => ClauseState::UnitPropagate(l),
-            None => panic!("Fully false clause."),
+            None => {
+                panic!("Fully false clause. {s:?}")
+            }
         }
     }
 
@@ -176,6 +180,7 @@ fn unit_propagate(cnf: &NormalForm, state: &mut State) -> Result<(), Vec<Index>>
 
         let l = slice[i];
 
+        // println!("Propagating literal: {l:?}");
         state.add_literal_propagate(l, slice, cnf)?;
 
         unit_propagate(cnf, state)
@@ -184,7 +189,11 @@ fn unit_propagate(cnf: &NormalForm, state: &mut State) -> Result<(), Vec<Index>>
     }
 }
 
-fn cdcl_internal(cnf: &mut NormalForm, mut state: State) -> Result<State, Vec<Index>> {
+fn cdcl_internal(
+    cnf: &mut NormalForm,
+    mut state: State,
+    depth: usize,
+) -> Result<State, Vec<Index>> {
     unit_propagate(cnf, &mut state)?;
 
     let l = match state.get_arbitrary_literal() {
@@ -194,17 +203,21 @@ fn cdcl_internal(cnf: &mut NormalForm, mut state: State) -> Result<State, Vec<In
 
     let mut state_clone = state.clone();
     state_clone.add_literal_arbitrary(l);
+    // println!("Choosing arbitrary literal: {l:?}");
 
-    match cdcl_internal(cnf, state_clone) {
+    match cdcl_internal(cnf, state_clone, depth + 1) {
         Ok(s) => Ok(s),
         Err(c) => {
-            let count_unknown_literals =
-                c.iter().filter(|&&i| !state.is_unknown_literal(i)).count();
-
-            if count_unknown_literals >= 2 || (count_unknown_literals == c.len()) {
+            let count_unknown_literals = c.iter().filter(|&&i| state.is_unknown_literal(i)).count();
+            // println!("Count unknown: {count_unknown_literals}; {c:?}");
+            if count_unknown_literals >= 2
+                || (count_unknown_literals == c.len())
+                || (depth == 0 && count_unknown_literals == 1)
+            {
+                // println!("Adding cclause: {c:?}");
                 cnf.add_clause(&c);
 
-                cdcl_internal(cnf, state)
+                cdcl_internal(cnf, state, depth)
             } else {
                 Err(c)
             }
@@ -214,7 +227,7 @@ fn cdcl_internal(cnf: &mut NormalForm, mut state: State) -> Result<State, Vec<In
 
 pub fn cdcl(cnf: &mut NormalForm) -> Option<Vec<Index>> {
     let num_literals = cnf.get_num_literals();
-    match cdcl_internal(cnf, State::new(num_literals)) {
+    match cdcl_internal(cnf, State::new(num_literals), 0) {
         Ok(state) => {
             if state.is_complete() {
                 Some(state.get_solution())
diff --git a/src/main.rs b/src/main.rs
index 0c04586..fd16603 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -46,7 +46,6 @@ fn main() -> Result<()> {
         }
         Method::Cdcl => {
             let (mut cnf, map) = e.cnf_normal_form();
-            dbg!(&map);
             match crate::cdcl::cdcl(&mut cnf) {
                 Some(s) => {
                     solution.extend_from_slice(&s);