From e5f408aed26bbd9984b1be463298092b72fb2c10 Mon Sep 17 00:00:00 2001 From: hal8174 Date: Wed, 6 Nov 2024 20:00:54 +0100 Subject: [PATCH] Add reverse game of life --- src/bin/gen_reverse_game_of_life.rs | 134 ++++++++++++++++++++++++++++ src/cdcl.rs | 5 +- src/expr/helper.rs | 34 +++++++ src/lib.rs | 2 + src/main.rs | 1 + src/mapping.rs | 2 +- src/normal_form.rs | 18 ++++ src/solver.rs | 76 ++++++++++++++++ 8 files changed, 269 insertions(+), 3 deletions(-) create mode 100644 src/bin/gen_reverse_game_of_life.rs create mode 100644 src/solver.rs diff --git a/src/bin/gen_reverse_game_of_life.rs b/src/bin/gen_reverse_game_of_life.rs new file mode 100644 index 0000000..8c81515 --- /dev/null +++ b/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, +} + +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!() + } + } +} diff --git a/src/cdcl.rs b/src/cdcl.rs index c497251..46066ca 100644 --- a/src/cdcl.rs +++ b/src/cdcl.rs @@ -225,9 +225,10 @@ fn cdcl_internal( } } -pub fn cdcl(cnf: &mut NormalForm) -> Option> { +pub fn cdcl(cnf: &NormalForm) -> Option> { + 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()) diff --git a/src/expr/helper.rs b/src/expr/helper.rs index fd5006c..1b9cc77 100644 --- a/src/expr/helper.rs +++ b/src/expr/helper.rs @@ -115,4 +115,38 @@ where Expr::not(Expr::less_than_three_of(s)), ]) } + + pub fn cnf_from_truth_function bool>(f: F, s: &[L]) -> Expr { + 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) + } } diff --git a/src/lib.rs b/src/lib.rs index 79f6fdb..fd9c162 100644 --- a/src/lib.rs +++ b/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; diff --git a/src/main.rs b/src/main.rs index fd16603..6bc2149 100644 --- a/src/main.rs +++ b/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 { diff --git a/src/mapping.rs b/src/mapping.rs index 8b7546c..7759809 100644 --- a/src/mapping.rs +++ b/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] } } diff --git a/src/normal_form.rs b/src/normal_form.rs index 09668a4..b1707ad 100644 --- a/src/normal_form.rs +++ b/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()); } diff --git a/src/solver.rs b/src/solver.rs new file mode 100644 index 0000000..b4730a3 --- /dev/null +++ b/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>, +>( + f: F, + expr: Expr, +) -> Option> { + 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>, +>( + f: F, + cnf: &NormalForm, + mapping: &Mapping, +) -> Option> { + 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: F, + cnf: NormalForm, + mapping: Mapping, +} + +impl SolutionIterator { + pub fn new(f: F, expr: Expr) -> Self { + let (cnf, mapping) = expr.cnf_normal_form(); + Self { f, cnf, mapping } + } +} + +impl Option>, L: Clone + Eq + std::hash::Hash> Iterator + for SolutionIterator +{ + type Item = HashMap; + + fn next(&mut self) -> Option { + 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) + } +}