Add reverse game of life

src/bin/gen_reverse_game_of_life.rs

@@ -0,0 +1,134 @@
+use simple_sat_solver::{
+    cdcl::cdcl,
+    expr::Expr,
+    solver::{normal_form_solver, normal_form_solver_from_cnf, SolutionIterator},
+};
+use std::ops::{Index, IndexMut};
+
+fn neightbors(gol: &Gameoflife, x: usize, y: usize) -> Vec<(usize, usize)> {
+    let mut v = Vec::new();
+    v.push((x, y));
+    if y > 0 {
+        if x > 0 {
+            v.push((x - 1, y - 1));
+        }
+        v.push((x, y - 1));
+        if x < gol.width() - 1 {
+            v.push((x + 1, y - 1));
+        }
+    }
+    if x > 0 {
+        v.push((x - 1, y));
+    }
+    if x < gol.width() - 1 {
+        v.push((x + 1, y));
+    }
+    if y < gol.height() - 1 {
+        if x > 0 {
+            v.push((x - 1, y + 1));
+        }
+        v.push((x, y + 1));
+        if x < gol.width() - 1 {
+            v.push((x + 1, y + 1));
+        }
+    }
+    v
+}
+
+fn gen_reverse_game_of_life(gol: &Gameoflife) -> Expr<(usize, usize)> {
+    let mut and = Vec::new();
+
+    for x in 0..gol.width() {
+        for y in 0..gol.height() {
+            let n = neightbors(gol, x, y);
+
+            if gol[(x, y)] {
+                and.push(Expr::cnf_from_truth_function(
+                    |s| {
+                        s[1..].iter().filter(|&&b| b).count() == 3
+                            || (s[0] && s[1..].iter().filter(|&&b| b).count() == 2)
+                    },
+                    &n,
+                ));
+            } else {
+                and.push(Expr::cnf_from_truth_function(
+                    |s| {
+                        !(s[1..].iter().filter(|&&b| b).count() == 3
+                            || (s[0] && s[1..].iter().filter(|&&b| b).count() == 2))
+                    },
+                    &n,
+                ));
+            }
+        }
+    }
+
+    Expr::And(and)
+}
+
+struct Gameoflife {
+    width: usize,
+    height: usize,
+    data: Vec<bool>,
+}
+
+impl Gameoflife {
+    fn new(width: usize, height: usize) -> Self {
+        Self {
+            width,
+            height,
+            data: vec![false; width * height],
+        }
+    }
+
+    fn width(&self) -> usize {
+        self.width
+    }
+
+    fn height(&self) -> usize {
+        self.height
+    }
+}
+
+impl Index<(usize, usize)> for Gameoflife {
+    type Output = bool;
+
+    fn index(&self, index: (usize, usize)) -> &Self::Output {
+        &self.data[index.1 * self.width + index.0]
+    }
+}
+
+impl IndexMut<(usize, usize)> for Gameoflife {
+    fn index_mut(&mut self, index: (usize, usize)) -> &mut Self::Output {
+        &mut self.data[index.1 * self.width + index.0]
+    }
+}
+
+fn main() {
+    let mut gol = Gameoflife::new(5, 5);
+
+    // gol[(1, 3)] = true;
+    // gol[(2, 3)] = true;
+    // gol[(3, 3)] = true;
+    // gol[(3, 2)] = true;
+    // gol[(2, 1)] = true;
+
+    let e = gen_reverse_game_of_life(&gol);
+
+    // let s = normal_form_solver(cdcl, e).unwrap();
+
+    let solver = SolutionIterator::new(cdcl, e);
+
+    for s in solver {
+        println!("Solution:");
+        for y in 0..gol.height() {
+            for x in 0..gol.width() {
+                if s.get(&(x, y)).copied().unwrap_or(false) {
+                    print!("#");
+                } else {
+                    print!(" ");
+                }
+            }
+            println!()
+        }
+    }
+}

src/cdcl.rs

@@ -225,9 +225,10 @@ fn cdcl_internal(
     }
 }
 
-pub fn cdcl(cnf: &mut NormalForm) -> Option<Vec<Index>> {
+pub fn cdcl(cnf: &NormalForm) -> Option<Vec<Index>> {
+    let mut cnf = cnf.clone();
     let num_literals = cnf.get_num_literals();
-    match cdcl_internal(cnf, State::new(num_literals), 0) {
+    match cdcl_internal(&mut cnf, State::new(num_literals), 0) {
         Ok(state) => {
             if state.is_complete() {
                 Some(state.get_solution())

src/expr/helper.rs

@@ -115,4 +115,38 @@ where
             Expr::not(Expr::less_than_three_of(s)),
         ])
     }
+
+    pub fn cnf_from_truth_function<F: Fn(&[bool]) -> bool>(f: F, s: &[L]) -> Expr<L> {
+        let mut bits = vec![false; s.len()];
+        let mut and = Vec::new();
+        'outer: loop {
+            let mut i = 0;
+
+            if !f(&bits) {
+                and.push(Expr::Or(
+                    s.iter()
+                        .enumerate()
+                        .map(|(i, l)| {
+                            if !bits[i] {
+                                Expr::not(Expr::Literal(l.clone()))
+                            } else {
+                                Expr::Literal(l.clone())
+                            }
+                        })
+                        .collect(),
+                ))
+            }
+
+            while bits[i] == true {
+                bits[i] = false;
+                i += 1;
+                if i >= bits.len() {
+                    break 'outer;
+                }
+            }
+            bits[i] = true;
+        }
+
+        Expr::And(and)
+    }
 }

src/lib.rs

@@ -1,5 +1,7 @@
+pub mod cdcl;
 pub mod dpll;
 pub mod dpll_normal_form;
 pub mod expr;
 pub mod mapping;
 pub mod normal_form;
+pub mod solver;

src/main.rs

@@ -8,6 +8,7 @@ mod dpll_normal_form;
 mod expr;
 mod mapping;
 mod normal_form;
+mod solver;
 
 #[derive(ValueEnum, Clone)]
 enum Method {

src/mapping.rs

@@ -31,6 +31,6 @@ where
     }
 
     pub fn backward(&self, i: Index) -> &L {
-        &self.backward[(i - 1) as usize]
+        &self.backward[(i.abs() - 1) as usize]
     }
 }

src/normal_form.rs

@@ -66,6 +66,24 @@ impl NormalForm {
     pub fn add_clause(&mut self, s: &[Index]) {
         let len = s.len();
 
+        {
+            let mut i = 0;
+            let mut j = s.len() - 1;
+            while s[i] < 0 && s[j] > 0 {
+                match (-s[i]).cmp(&s[j]) {
+                    std::cmp::Ordering::Less => {
+                        j -= 1;
+                    }
+                    std::cmp::Ordering::Equal => {
+                        return;
+                    }
+                    std::cmp::Ordering::Greater => {
+                        i += 1;
+                    }
+                }
+            }
+        }
+
         if self.data.len() <= len {
             self.data.resize(len + 1, Vec::new());
         }

src/solver.rs

@@ -0,0 +1,76 @@
+use std::{collections::HashMap, marker::PhantomData, ops::Neg};
+
+use crate::{dpll::Index, expr::Expr, mapping::Mapping, normal_form::NormalForm};
+
+pub fn normal_form_solver<
+    L: Clone + Eq + std::hash::Hash,
+    F: Fn(&NormalForm) -> Option<Vec<Index>>,
+>(
+    f: F,
+    expr: Expr<L>,
+) -> Option<HashMap<L, bool>> {
+    let (cnf, map) = expr.cnf_normal_form();
+
+    normal_form_solver_from_cnf(f, &cnf, &map)
+}
+
+pub fn normal_form_solver_from_cnf<
+    L: Clone + Eq + std::hash::Hash,
+    F: Fn(&NormalForm) -> Option<Vec<Index>>,
+>(
+    f: F,
+    cnf: &NormalForm,
+    mapping: &Mapping<L>,
+) -> Option<HashMap<L, bool>> {
+    let s = f(cnf)?;
+
+    let mut solution = HashMap::new();
+
+    for l in s {
+        if l < 0 {
+            solution.insert(mapping.backward(l).clone(), true);
+        } else {
+            solution.insert(mapping.backward(l).clone(), false);
+        }
+    }
+
+    Some(solution)
+}
+
+pub struct SolutionIterator<F, L> {
+    f: F,
+    cnf: NormalForm,
+    mapping: Mapping<L>,
+}
+
+impl<F, L: Clone + Eq + std::hash::Hash> SolutionIterator<F, L> {
+    pub fn new(f: F, expr: Expr<L>) -> Self {
+        let (cnf, mapping) = expr.cnf_normal_form();
+        Self { f, cnf, mapping }
+    }
+}
+
+impl<F: Fn(&NormalForm) -> Option<Vec<Index>>, L: Clone + Eq + std::hash::Hash> Iterator
+    for SolutionIterator<F, L>
+{
+    type Item = HashMap<L, bool>;
+
+    fn next(&mut self) -> Option<Self::Item> {
+        let s = (self.f)(&self.cnf)?;
+
+        let inverted: Vec<_> = s.iter().copied().map(Index::neg).collect();
+        self.cnf.add_clause(&inverted);
+
+        let mut solution = HashMap::new();
+
+        for l in s {
+            if l < 0 {
+                solution.insert(self.mapping.backward(l).clone(), true);
+            } else {
+                solution.insert(self.mapping.backward(l).clone(), false);
+            }
+        }
+
+        Some(solution)
+    }
+}