diff --git a/sat/wikipedia.sat b/sat/wikipedia.sat new file mode 100644 index 0000000..b3b218a --- /dev/null +++ b/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 diff --git a/src/cdcl.rs b/src/cdcl.rs index 9afaa68..072e079 100644 --- a/src/cdcl.rs +++ b/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), +#[derive(Debug, Clone, Copy)] +enum StateItem { + True, + False, + Unknown, } -fn cdcl_internal( - cnf: &NormalForm, - solution: &mut Vec, +#[derive(Debug, Clone)] +struct State { + map: Vec, graph: Vec<(Index, Index)>, -) -> Result { - todo!() } -pub fn cdcl(cnf: &NormalForm, solution: &mut Vec) -> 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 { + 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> { + 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 { + 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> { + 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> { + 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> { + 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, } } diff --git a/src/dpll_normal_form.rs b/src/dpll_normal_form.rs index 1c31f76..9458147 100644 --- a/src/dpll_normal_form.rs +++ b/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) { if let Some((s, _)) = cnf.iter_len(1).next() { @@ -19,8 +22,13 @@ fn pure_literal_assign(cnf: &mut NormalForm, solution: &mut Vec) { 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) -> 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) { diff --git a/src/expr.rs b/src/expr.rs index ab916cb..2a10559 100644 --- a/src/expr.rs +++ b/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); } } diff --git a/src/main.rs b/src/main.rs index b6e2d6d..0c04586 100644 --- a/src/main.rs +++ b/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(); diff --git a/src/mapping.rs b/src/mapping.rs index e76707c..f42337d 100644 --- a/src/mapping.rs +++ b/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>, diff --git a/src/normal_form.rs b/src/normal_form.rs index 0d72dd1..09668a4 100644 --- a/src/normal_form.rs +++ b/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 { 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 }