Generalize literals in epression and add helper function for expressions

sat/wikipedia.sat

@@ -6,4 +6,3 @@ x2 | x11
 !x7 | x8 | !x9
 x7 | x8 | !x10
 x7 | x10 | !x12
-x1

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 =
+            let count_unknown_literals = c.iter().filter(|&&i| state.is_unknown_literal(i)).count();
-                c.iter().filter(|&&i| !state.is_unknown_literal(i)).count();
+            // println!("Count unknown: {count_unknown_literals}; {c:?}");
-
+            if count_unknown_literals >= 2
-            if count_unknown_literals >= 2 || (count_unknown_literals == c.len()) {
+                || (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())

src/expr.rs

@@ -1,3 +1,5 @@
+use std::hash::Hash;
+
 use crate::{
     dpll::Index,
     mapping::Mapping,
@@ -5,12 +7,26 @@ use crate::{
 };
 use miette::{miette, Context, Result};
 
+pub mod helper;
+
 #[derive(Debug, Clone)]
-pub enum Expr<'s> {
+pub enum Expr<L>
-    Literal(&'s str),
+where
-    Not(Box<Expr<'s>>),
+    L: Clone,
-    And(Vec<Expr<'s>>),
+{
-    Or(Vec<Expr<'s>>),
+    Literal(L),
+    Not(Box<Expr<L>>),
+    And(Vec<Expr<L>>),
+    Or(Vec<Expr<L>>),
+}
+
+impl<L> Expr<L>
+where
+    L: Clone,
+{
+    pub fn not(e: Expr<L>) -> Expr<L> {
+        Expr::Not(Box::new(e))
+    }
 }
 
 #[derive(Debug)]
@@ -91,8 +107,8 @@ impl<'s> Iterator for Tokanizer<'s> {
     }
 }
 
-impl<'s> Expr<'s> {
+impl<'s> Expr<&'s str> {
-    fn parse_expr(tokanizer: &mut Tokanizer<'s>) -> Result<Expr<'s>> {
+    fn parse_expr(tokanizer: &mut Tokanizer<'s>) -> Result<Expr<&'s str>> {
         if let Some(token) = tokanizer.next().transpose()? {
             match token {
                 Token::Literal(l) => Ok(Expr::Literal(l)),
@@ -173,7 +189,12 @@ impl<'s> Expr<'s> {
             Ok(Expr::And(v))
         }
     }
+}
 
+impl<L> Expr<L>
+where
+    L: Clone,
+{
     pub fn disjunctive_normal_form(self) -> Self {
         // dbg!(&self);
         match self {
@@ -245,8 +266,13 @@ impl<'s> Expr<'s> {
             ),
         }
     }
+}
 
-    pub fn disjunctive_normal_form2(self, mapping: &mut Mapping<'s>) -> NormalForm {
+impl<L> Expr<L>
+where
+    L: Clone + Eq + Hash,
+{
+    pub fn disjunctive_normal_form2(self, mapping: &mut Mapping<L>) -> NormalForm {
         match self {
             Expr::Literal(l) => {
                 let mut n = NormalForm::new();
@@ -371,7 +397,7 @@ impl<'s> Expr<'s> {
         }
     }
 
-    pub fn cnf_normal_form(self) -> (NormalForm, Mapping<'s>) {
+    pub fn cnf_normal_form(self) -> (NormalForm, Mapping<L>) {
         let mut mapping = Mapping::new();
 
         let mut cnf = Expr::Not(Box::new(self)).disjunctive_normal_form2(&mut mapping);
@@ -381,7 +407,7 @@ impl<'s> Expr<'s> {
         (cnf, mapping)
     }
 
-    pub fn cnf(self) -> (Vec<Vec<Index>>, Mapping<'s>) {
+    pub fn cnf(self) -> (Vec<Vec<Index>>, Mapping<L>) {
         let mut map = Mapping::new();
 
         let mut cnf = Vec::new();

src/expr/helper.rs

@@ -0,0 +1,118 @@
+use super::Expr;
+
+impl<L> Expr<L>
+where
+    L: Clone,
+{
+    pub fn to_expressions(s: &[L]) -> Vec<Expr<L>> {
+        s.iter().map(|l| Expr::Literal(l.clone())).collect()
+    }
+
+    pub fn less_than_two_of(s: &[Expr<L>]) -> Expr<L> {
+        assert!(s.len() > 1);
+        let mut and = Vec::new();
+
+        for i in 0..s.len() {
+            for j in 0..i {
+                and.push(Expr::not(Expr::And(vec![s[i].clone(), s[j].clone()])));
+            }
+        }
+
+        Expr::And(and)
+    }
+
+    pub fn less_than_three_of(s: &[Expr<L>]) -> Expr<L> {
+        assert!(s.len() > 2);
+        let mut and = Vec::new();
+
+        for i in 0..s.len() {
+            for j in 0..i {
+                for k in 0..j {
+                    and.push(Expr::not(Expr::And(vec![
+                        s[i].clone(),
+                        s[j].clone(),
+                        s[k].clone(),
+                    ])));
+                }
+            }
+        }
+
+        Expr::And(and)
+    }
+
+    pub fn more_than_zero_of(s: &[Expr<L>]) -> Expr<L> {
+        Expr::Or(s.to_vec())
+    }
+
+    pub fn more_than_one_of(s: &[Expr<L>]) -> Expr<L> {
+        assert!(s.len() > 1);
+        let mut or = Vec::new();
+
+        for i in 0..s.len() {
+            for j in 0..i {
+                or.push(Expr::And(vec![s[i].clone(), s[j].clone()]));
+            }
+        }
+
+        Expr::Or(or)
+    }
+
+    pub fn more_than_two_of(s: &[Expr<L>]) -> Expr<L> {
+        assert!(s.len() > 2);
+        let mut or = Vec::new();
+
+        for i in 0..s.len() {
+            for j in 0..i {
+                for k in 0..j {
+                    or.push(Expr::And(vec![s[i].clone(), s[j].clone(), s[k].clone()]));
+                }
+            }
+        }
+
+        Expr::Or(or)
+    }
+
+    pub fn more_than_three_of(s: &[Expr<L>]) -> Expr<L> {
+        assert!(!s.is_empty());
+        if s.len() < 4 {
+            Expr::And(vec![s[0].clone(), Expr::not(s[0].clone())])
+        } else {
+            let mut or = Vec::new();
+
+            for i in 0..s.len() {
+                for j in 0..i {
+                    for k in 0..j {
+                        for l in 0..k {
+                            or.push(Expr::And(vec![
+                                s[i].clone(),
+                                s[j].clone(),
+                                s[k].clone(),
+                                s[l].clone(),
+                            ]));
+                        }
+                    }
+                }
+            }
+
+            Expr::Or(or)
+        }
+    }
+
+    pub fn exactly_one_of(s: &[Expr<L>]) -> Expr<L> {
+        Expr::And(vec![Expr::less_than_two_of(s), Expr::more_than_zero_of(s)])
+    }
+
+    pub fn exactly_two_of(s: &[Expr<L>]) -> Expr<L> {
+        Expr::not(Expr::Or(vec![
+            Expr::less_than_two_of(s),
+            Expr::more_than_two_of(s),
+        ]))
+    }
+
+    pub fn exactly_three_of(s: &[Expr<L>]) -> Expr<L> {
+        Expr::And(vec![
+            Expr::not(Expr::more_than_three_of(s)),
+            Expr::not(Expr::less_than_three_of(s)),
+        ])
+    }
+}

src/lib.rs

@@ -0,0 +1,5 @@
+pub mod dpll;
+pub mod dpll_normal_form;
+pub mod expr;
+pub mod mapping;
+pub mod normal_form;

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);

src/mapping.rs

@@ -1,14 +1,17 @@
-use std::collections::HashMap;
+use std::{collections::HashMap, hash::Hash};
 
 use crate::dpll::Index;
 
 #[derive(Debug, Clone)]
-pub struct Mapping<'s> {
+pub struct Mapping<L> {
-    forward: HashMap<&'s str, Index>,
+    forward: HashMap<L, Index>,
-    backward: Vec<&'s str>,
+    backward: Vec<L>,
 }
 
-impl<'s> Mapping<'s> {
+impl<L> Mapping<L>
+where
+    L: Eq + Hash + Clone,
+{
     pub fn new() -> Self {
         Self {
             forward: HashMap::new(),
@@ -16,18 +19,18 @@ impl<'s> Mapping<'s> {
         }
     }
 
-    pub fn forward(&mut self, str: &'s str) -> Index {
+    pub fn forward(&mut self, l: L) -> Index {
-        if let Some(&i) = self.forward.get(str) {
+        if let Some(&i) = self.forward.get(&l) {
             i
         } else {
             let i = self.backward.len() as Index + 1;
-            self.forward.insert(str, i);
+            self.forward.insert(l.clone(), i);
-            self.backward.push(str);
+            self.backward.push(l);
             i
         }
     }
 
-    pub fn backward(&self, i: Index) -> &'s str {
+    pub fn backward(&self, i: Index) -> &L {
-        self.backward[(i - 1) as usize]
+        &self.backward[(i - 1) as usize]
     }
 }