Part of cdcl

sat/wikipedia.sat

@@ -0,0 +1,9 @@
+x1 | !x4
+x1 | !x3 | !x4
+x1 | x8 | x12
+x2 | x11
+!x7 | !x3 | x9
+!x7 | x8 | !x9
+x7 | x8 | !x10
+x7 | x10 | !x12
+x1

src/cdcl.rs

@@ -1,21 +1,158 @@
-use crate::{dpll::Index, normal_form::NormalForm};
+use crate::{
+    dpll::Index,
+    normal_form::{NormalForm, NormalFormIteratorItem},
+};
 
-enum Result {
-    Complete,
-    Conflict(Vec<Index>),
+#[derive(Debug, Clone, Copy)]
+enum StateItem {
+    True,
+    False,
+    Unknown,
 }
 
-fn cdcl_internal(
-    cnf: &NormalForm,
-    solution: &mut Vec<Index>,
+#[derive(Debug, Clone)]
+struct State {
+    map: Vec<StateItem>,
     graph: Vec<(Index, Index)>,
-) -> Result {
-    todo!()
 }
 
-pub fn cdcl(cnf: &NormalForm, solution: &mut Vec<Index>) -> bool {
-    match cdcl_internal(cnf, solution, vec![]) {
-        Result::Complete => true,
-        Result::Conflict(_) => false,
+impl State {
+    fn new(num_literals: Index) -> Self {
+        Self {
+            map: vec![StateItem::Unknown; num_literals as usize],
+            graph: Vec::new(),
+        }
+    }
+
+    fn get_arbitrary_literal(&self) -> Option<Index> {
+        self.map
+            .iter()
+            .position(|i| matches!(i, StateItem::Unknown))
+            .map(|i| i as Index + 1)
+    }
+
+    fn add_literal_arbitrary(&mut self, l: Index) {
+        assert!(self.is_unknown_literal(l));
+        self.set_literal(l);
+    }
+
+    fn add_literal_propagate(&mut self, l: Index, cnf: &NormalForm) -> Result<(), Vec<Index>> {
+        self.set_literal(l);
+
+        Ok(())
+    }
+
+    fn get_literal(&self, l: Index) -> StateItem {
+        self.map[l.unsigned_abs() as usize - 1]
+    }
+
+    fn set_literal_item(&mut self, l: Index, item: StateItem) {
+        self.map[l.unsigned_abs() as usize - 1] = item;
+    }
+
+    fn is_unknown_literal(&self, l: Index) -> bool {
+        matches!(self.get_literal(l), StateItem::Unknown)
+    }
+
+    fn set_literal(&mut self, l: Index) {
+        self.set_literal_item(
+            l,
+            if l > 0 {
+                StateItem::True
+            } else {
+                StateItem::False
+            },
+        );
+    }
+
+    fn get_solution(&self) -> Vec<Index> {
+        let mut res = Vec::new();
+        for (i, item) in self.map.iter().enumerate() {
+            let i = (i + 1) as Index;
+            match item {
+                StateItem::True => res.push(i),
+                StateItem::False => res.push(-i),
+                StateItem::Unknown => panic!(),
+            }
+        }
+        res
+    }
+
+    fn is_complete(&self) -> bool {
+        !self.map.iter().any(|l| matches!(l, StateItem::Unknown))
+    }
+}
+
+fn unit_propagate(cnf: &NormalForm, state: &mut State) -> Result<(), Vec<Index>> {
+    if let Some(nfii) = cnf.iter().find(
+        |NormalFormIteratorItem {
+             slice,
+             len: _,
+             index: _,
+         }| {
+            slice
+                .iter()
+                .filter(|&&l| state.is_unknown_literal(l))
+                .count()
+                == 1
+        },
+    ) {
+        let i = nfii
+            .slice
+            .iter()
+            .position(|&i| state.is_unknown_literal(i))
+            .unwrap();
+
+        let l = nfii.slice[i];
+
+        state.add_literal_propagate(l, cnf)?;
+
+        unit_propagate(cnf, state)
+    } else {
+        Ok(())
+    }
+}
+
+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 mut state_clone = state.clone();
+    state_clone.add_literal_arbitrary(l);
+
+    match cdcl_internal(cnf, state_clone) {
+        Ok(_) => todo!(),
+        Err(_) => todo!(),
+    };
+
+    let mut state_clone = state.clone();
+    state_clone.add_literal_arbitrary(-l);
+
+    match cdcl_internal(cnf, state_clone) {
+        Ok(_) => todo!(),
+        Err(_) => todo!(),
+    };
+
+    Ok(state)
+}
+
+pub fn cdcl(mut cnf: &mut NormalForm) -> Option<Vec<Index>> {
+    let num_literals = cnf.get_num_literals();
+    match cdcl_internal(&mut cnf, State::new(num_literals)) {
+        Ok(state) => {
+            if state.is_complete() {
+                Some(state.get_solution())
+            } else {
+                None
+            }
+        }
+        Err(_) => None,
     }
 }

src/dpll_normal_form.rs

@@ -1,6 +1,9 @@
 use std::{cell::RefCell, collections::HashSet};
 
-use crate::{dpll::Index, normal_form::NormalForm};
+use crate::{
+    dpll::Index,
+    normal_form::{NormalForm, NormalFormIteratorItem},
+};
 
 fn unit_propagate(cnf: &mut NormalForm, solution: &mut Vec<Index>) {
     if let Some((s, _)) = cnf.iter_len(1).next() {
@@ -19,8 +22,13 @@ fn pure_literal_assign(cnf: &mut NormalForm, solution: &mut Vec<Index>) {
     let mut literals = LITERALS.take();
     literals.clear();
 
-    for (s, _, _) in cnf.iter() {
-        literals.extend(s.iter());
+    for NormalFormIteratorItem {
+        slice,
+        len: _,
+        index: _,
+    } in cnf.iter()
+    {
+        literals.extend(slice.iter());
     }
 
     for &l in &literals {
@@ -59,7 +67,7 @@ pub fn dpll(cnf: &NormalForm, solution: &mut Vec<Index>) -> bool {
         return false;
     }
 
-    let literal = own_cnf.iter().next().unwrap().0[0];
+    let literal = own_cnf.iter().next().unwrap().slice[0];
 
     own_cnf.push_litearl_clause(literal);
     if dpll(&own_cnf, solution) {

src/expr.rs

@@ -1,4 +1,8 @@
-use crate::{dpll::Index, mapping::Mapping, normal_form::NormalForm};
+use crate::{
+    dpll::Index,
+    mapping::Mapping,
+    normal_form::{NormalForm, NormalFormIteratorItem},
+};
 use miette::{miette, Context, Result};
 
 #[derive(Debug, Clone)]
@@ -262,8 +266,13 @@ impl<'s> Expr<'s> {
                         .into_iter()
                         .map(|e| Expr::Not(Box::new(e)).disjunctive_normal_form2(mapping))
                     {
-                        for (s, _, _) in e.iter() {
-                            n.add_clause(s);
+                        for NormalFormIteratorItem {
+                            slice,
+                            len: _,
+                            index: _,
+                        } in e.iter()
+                        {
+                            n.add_clause(slice);
                         }
                     }
                     n
@@ -285,8 +294,18 @@ impl<'s> Expr<'s> {
                 for on in v {
                     let mut new_n = NormalForm::new();
 
-                    for (old_s, _, _) in n.iter() {
-                        for (new_s, _, _) in on.iter() {
+                    for NormalFormIteratorItem {
+                        slice: old_s,
+                        len: _,
+                        index: _,
+                    } in n.iter()
+                    {
+                        for NormalFormIteratorItem {
+                            slice: new_s,
+                            len: _,
+                            index: _,
+                        } in on.iter()
+                        {
                             scratch.clear();
                             scratch.extend_from_slice(old_s);
                             scratch.extend_from_slice(new_s);
@@ -305,8 +324,13 @@ impl<'s> Expr<'s> {
                 let mut n = NormalForm::new();
                 for e in v {
                     let on = e.disjunctive_normal_form2(mapping);
-                    for (s, _, _) in on.iter() {
-                        n.add_clause(s);
+                    for NormalFormIteratorItem {
+                        slice,
+                        len: _,
+                        index: _,
+                    } in on.iter()
+                    {
+                        n.add_clause(slice);
                     }
                 }
 

src/main.rs

@@ -45,8 +45,16 @@ fn main() -> Result<()> {
             (crate::dpll_normal_form::dpll(&cnf, &mut solution), map)
         }
         Method::Cdcl => {
-            let (cnf, map) = e.cnf_normal_form();
-            (crate::cdcl::cdcl(&cnf, &mut solution), map)
+            let (mut cnf, map) = e.cnf_normal_form();
+            dbg!(&map);
+            match crate::cdcl::cdcl(&mut cnf) {
+                Some(s) => {
+                    solution.extend_from_slice(&s);
+
+                    (true, map)
+                }
+                None => (false, map),
+            }
         }
     };
     let elapsed = start.elapsed();

src/mapping.rs

@@ -2,6 +2,7 @@ use std::collections::HashMap;
 
 use crate::dpll::Index;
 
+#[derive(Debug, Clone)]
 pub struct Mapping<'s> {
     forward: HashMap<&'s str, Index>,
     backward: Vec<&'s str>,

src/normal_form.rs

@@ -120,6 +120,13 @@ impl NormalForm {
         }
     }
 
+    pub fn get_num_literals(&self) -> Index {
+        self.iter()
+            .flat_map(|i| i.slice.iter().map(|l| l.abs()))
+            .max()
+            .unwrap()
+    }
+
     pub fn stats(&self) {
         println!("Normal form stats:");
         let mut sum = 0;
@@ -147,8 +154,14 @@ impl<'nf> NormalFormIterator<'nf> {
     }
 }
 
+pub struct NormalFormIteratorItem<'nf> {
+    pub slice: &'nf [Index],
+    pub len: usize,
+    pub index: usize,
+}
+
 impl<'nf> Iterator for NormalFormIterator<'nf> {
-    type Item = (&'nf [Index], usize, usize);
+    type Item = NormalFormIteratorItem<'nf>;
 
     fn next(&mut self) -> Option<Self::Item> {
         while self.len < self.nf.data.len()
@@ -162,7 +175,11 @@ impl<'nf> Iterator for NormalFormIterator<'nf> {
 
             self.index += 1;
 
-            Some((s, self.len, self.index - 1))
+            Some(NormalFormIteratorItem {
+                slice: s,
+                len: self.len,
+                index: self.index - 1,
+            })
         } else {
             None
         }