diff --git a/src/cdcl.rs b/src/cdcl.rs new file mode 100644 index 0000000..9afaa68 --- /dev/null +++ b/src/cdcl.rs @@ -0,0 +1,21 @@ +use crate::{dpll::Index, normal_form::NormalForm}; + +enum Result { + Complete, + Conflict(Vec), +} + +fn cdcl_internal( + cnf: &NormalForm, + solution: &mut 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, + } +} diff --git a/src/dpll.rs b/src/dpll.rs index 23bf229..2ec4417 100644 --- a/src/dpll.rs +++ b/src/dpll.rs @@ -21,7 +21,6 @@ fn unit_propagate(cnf: &mut Vec>, solution: &mut Vec) { { let l = cnf[i][0]; solution.push(l); - cnf.swap_remove(i); remvove_literal(cnf, l); unit_propagate(cnf, solution); } diff --git a/src/dpll_normal_form.rs b/src/dpll_normal_form.rs index d7594b2..1c31f76 100644 --- a/src/dpll_normal_form.rs +++ b/src/dpll_normal_form.rs @@ -1,6 +1,4 @@ -use std::{ - borrow::BorrowMut, cell::RefCell, collections::HashSet, ops::DerefMut, sync::RwLockWriteGuard, -}; +use std::{cell::RefCell, collections::HashSet}; use crate::{dpll::Index, normal_form::NormalForm}; diff --git a/src/expr.rs b/src/expr.rs index dbdecb4..ab916cb 100644 --- a/src/expr.rs +++ b/src/expr.rs @@ -1,6 +1,5 @@ use crate::{dpll::Index, mapping::Mapping, normal_form::NormalForm}; use miette::{miette, Context, Result}; -use std::collections::HashMap; #[derive(Debug, Clone)] pub enum Expr<'s> { @@ -171,25 +170,25 @@ impl<'s> Expr<'s> { } } - pub fn disjunctiveNormalForm(self) -> Self { + pub fn disjunctive_normal_form(self) -> Self { // dbg!(&self); match self { Expr::Literal(_) => self, Expr::Not(n) => match *n { Expr::Literal(_) => Expr::Not(n), - Expr::Not(i) => i.disjunctiveNormalForm(), + Expr::Not(i) => i.disjunctive_normal_form(), Expr::And(v) => Expr::Or( v.into_iter() - .map(|e| Expr::Not(Box::new(e)).disjunctiveNormalForm()) + .map(|e| Expr::Not(Box::new(e)).disjunctive_normal_form()) .collect(), ) - .disjunctiveNormalForm(), + .disjunctive_normal_form(), Expr::Or(v) => Expr::And( v.into_iter() - .map(|e| Expr::Not(Box::new(e)).disjunctiveNormalForm()) + .map(|e| Expr::Not(Box::new(e)).disjunctive_normal_form()) .collect(), ) - .disjunctiveNormalForm(), + .disjunctive_normal_form(), }, Expr::And(v) => { let v = v @@ -213,7 +212,7 @@ impl<'s> Expr<'s> { v.into_iter().next().unwrap() } else { let mut iter = v.into_iter(); - let mut v = match iter.next().unwrap().disjunctiveNormalForm() { + let mut v = match iter.next().unwrap().disjunctive_normal_form() { Expr::Literal(s) => vec![Expr::Literal(s)], Expr::Not(n) => vec![Expr::Not(n)], Expr::And(_) => unreachable!(), @@ -223,16 +222,16 @@ impl<'s> Expr<'s> { for e in iter { v = v .into_iter() - .map(|i| Expr::And(vec![e.clone(), i]).disjunctiveNormalForm()) + .map(|i| Expr::And(vec![e.clone(), i]).disjunctive_normal_form()) .collect() } - Expr::Or(v).disjunctiveNormalForm() + Expr::Or(v).disjunctive_normal_form() } } Expr::Or(v) => Expr::Or( v.into_iter() - .flat_map(|e| match e.disjunctiveNormalForm() { + .flat_map(|e| match e.disjunctive_normal_form() { Expr::Literal(s) => vec![Expr::Literal(s)].into_iter(), Expr::Not(n) => vec![Expr::Not(n)].into_iter(), Expr::And(_) => unreachable!(), @@ -243,7 +242,7 @@ impl<'s> Expr<'s> { } } - pub fn disjunctiveNormalForm2(self, mapping: &mut Mapping<'s>) -> NormalForm { + pub fn disjunctive_normal_form2(self, mapping: &mut Mapping<'s>) -> NormalForm { match self { Expr::Literal(l) => { let mut n = NormalForm::new(); @@ -256,12 +255,12 @@ impl<'s> Expr<'s> { n.add_clause(&[-mapping.forward(l)]); n } - Expr::Not(n) => n.disjunctiveNormalForm2(mapping), + Expr::Not(n) => n.disjunctive_normal_form2(mapping), Expr::And(v) => { let mut n = NormalForm::new(); for e in v .into_iter() - .map(|e| Expr::Not(Box::new(e)).disjunctiveNormalForm2(mapping)) + .map(|e| Expr::Not(Box::new(e)).disjunctive_normal_form2(mapping)) { for (s, _, _) in e.iter() { n.add_clause(s); @@ -271,12 +270,12 @@ impl<'s> Expr<'s> { } Expr::Or(v) => Expr::And(v.into_iter().map(|e| Expr::Not(Box::new(e))).collect()) - .disjunctiveNormalForm2(mapping), + .disjunctive_normal_form2(mapping), }, Expr::And(v) => { let mut v: Vec<_> = v .into_iter() - .map(|e| e.disjunctiveNormalForm2(mapping)) + .map(|e| e.disjunctive_normal_form2(mapping)) .collect(); let mut n = v.pop().unwrap(); @@ -305,7 +304,7 @@ impl<'s> Expr<'s> { Expr::Or(v) => { let mut n = NormalForm::new(); for e in v { - let on = e.disjunctiveNormalForm2(mapping); + let on = e.disjunctive_normal_form2(mapping); for (s, _, _) in on.iter() { n.add_clause(s); } @@ -316,8 +315,8 @@ impl<'s> Expr<'s> { } } - pub fn conjunctiveNormalForm(self) -> Self { - if let Expr::Or(v) = Expr::Not(Box::new(self)).disjunctiveNormalForm() { + pub fn conjunctive_normal_form(self) -> Self { + if let Expr::Or(v) = Expr::Not(Box::new(self)).disjunctive_normal_form() { Expr::And( v.into_iter() .map(|e| match e { @@ -348,51 +347,37 @@ impl<'s> Expr<'s> { } } - pub fn to_dpll_cnf_normal_form(self) -> (NormalForm, Mapping<'s>) { + pub fn cnf_normal_form(self) -> (NormalForm, Mapping<'s>) { let mut mapping = Mapping::new(); - let mut cnf = Expr::Not(Box::new(self)).disjunctiveNormalForm2(&mut mapping); + let mut cnf = Expr::Not(Box::new(self)).disjunctive_normal_form2(&mut mapping); cnf.negate(); (cnf, mapping) } - pub fn to_dpll_cnf(self) -> (Vec>, HashMap<&'s str, Index>) { - let mut map = HashMap::new(); + pub fn cnf(self) -> (Vec>, Mapping<'s>) { + let mut map = Mapping::new(); let mut cnf = Vec::new(); - let v = if let Expr::And(v) = self.conjunctiveNormalForm() { + let v = if let Expr::And(v) = self.conjunctive_normal_form() { v } else { unreachable!() }; - let mut nextfree = 1; - for e in v { let s = match e { Expr::Or(v) => { let mut s = Vec::new(); for l in v { if let Expr::Literal(l) = l { - if let Some(&i) = map.get(&l) { - s.push(i); - } else { - map.insert(l, nextfree); - s.push(nextfree); - nextfree += 1; - } + s.push(map.forward(l)); } else if let Expr::Not(n) = l { if let Expr::Literal(l) = *n { - if let Some(&i) = map.get(&l) { - s.push(-i); - } else { - map.insert(l, nextfree); - s.push(-nextfree); - nextfree += 1; - } + s.push(-map.forward(l)); } else { unreachable!() } @@ -401,28 +386,15 @@ impl<'s> Expr<'s> { } } s.sort(); + s.dedup(); s } Expr::Literal(l) => { - if let Some(&i) = map.get(&l) { - vec![-i] - } else { - map.insert(l, nextfree); - let i = nextfree; - nextfree += 1; - vec![-i] - } + vec![-map.forward(l)] } Expr::Not(n) => { if let Expr::Literal(l) = *n { - if let Some(&i) = map.get(&l) { - vec![i] - } else { - map.insert(l, nextfree); - let i = nextfree; - nextfree += 1; - vec![i] - } + vec![map.forward(l)] } else { unreachable!() } diff --git a/src/main.rs b/src/main.rs index a22314b..b6e2d6d 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1,88 +1,71 @@ -use std::collections::HashMap; - -use clap::Parser; -use dpll::dpll; -use expr::{Expr, Tokanizer}; -use mapping::Mapping; +use clap::{Parser, ValueEnum}; +use expr::Expr; use miette::{IntoDiagnostic, Result}; -use normal_form::NormalForm; + +mod cdcl; mod dpll; mod dpll_normal_form; +mod expr; mod mapping; mod normal_form; -mod expr; +#[derive(ValueEnum, Clone)] +enum Method { + DpllExpr, + Dpll, + Cdcl, +} #[derive(Parser)] struct Args { + method: Method, inputfile: std::path::PathBuf, } fn main() -> Result<()> { let args = Args::parse(); + let start = std::time::Instant::now(); let s = std::fs::read_to_string(args.inputfile).into_diagnostic()?; let e = Expr::parse(&s)?; - println!("Expression parsed succesfully."); - - // dbg!(&e); - // dbg!(Expr::Not(Box::new(e.clone())).disjunctiveNormalForm()); - - let (cnf, map) = e.to_dpll_cnf_normal_form(); - - println!("Normal form created."); - cnf.stats(); + let elapsed = start.elapsed(); + println!("Expression parsed succesfully in {elapsed:?}"); let mut solution = Vec::new(); let start = std::time::Instant::now(); - dbg!(crate::dpll_normal_form::dpll(&cnf, &mut solution)); + let (result, map) = match args.method { + Method::DpllExpr => { + let (cnf, map) = e.cnf(); + (crate::dpll::dpll(&cnf, &mut solution), map) + } + Method::Dpll => { + let (cnf, map) = e.cnf_normal_form(); + (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 elapsed = start.elapsed(); - println!("Time dpll: {elapsed:?}"); + println!("Time: {elapsed:?}"); - // dbg!(&solution); - // dbg!(e.clone().conjunctiveNormalForm()); - - // let (cnf, map) = e.to_dpll_cnf(); - - // dbg!(&cnf, &map); - // println!("cnf clauses: {}", cnf.len()); - - // let mut solution = Vec::new(); - - // dpll(&cnf, &mut solution); - - // dbg!(solution); - - // let inv_map: HashMap<_, _> = map.into_iter().map(|(k, v)| (v, k)).collect(); - - // dbg!(&solution); - - let mut s = Vec::new(); - for i in solution { - if i > 0 { - s.push((map.backward(i), true)); - } else { - s.push((map.backward(i.abs()), false)); + if result { + println!("Solution found:"); + let mut s = Vec::new(); + for i in solution { + if i > 0 { + s.push((map.backward(i), true)); + } else { + s.push((map.backward(i.abs()), false)); + } + } + s.sort(); + for (s, b) in s { + println!("{s}: {b}"); } } - s.sort(); - for (s, b) in s { - println!("{s}: {b}"); - } - - // let mut nf = NormalForm::from_slices(&cnf); - // dbg!(&nf); - - // nf.remove_literal(-1); - // dbg!(&nf); - - // let mut s2 = Vec::new(); - - // dbg!(dpll_normal_form::dpll(&nf, &mut s2)); - - // dbg!(s2 == solution); - Ok(()) } diff --git a/src/normal_form.rs b/src/normal_form.rs index a3ce0f6..0d72dd1 100644 --- a/src/normal_form.rs +++ b/src/normal_form.rs @@ -1,5 +1,3 @@ -use std::ops::Neg; - use crate::dpll::Index; #[derive(Debug, Clone)]