diff --git a/src/dpll.rs b/src/dpll.rs
index 2b408f5..23bf229 100644
--- a/src/dpll.rs
+++ b/src/dpll.rs
@@ -1,6 +1,6 @@
 use std::collections::HashSet;
 
-type Index = i16;
+pub type Index = i16;
 
 fn remvove_literal(cnf: &mut Vec<Vec<Index>>, l: Index) {
     cnf.retain(|c| c.binary_search(&l).is_err());
diff --git a/src/expr.rs b/src/expr.rs
new file mode 100644
index 0000000..36202b4
--- /dev/null
+++ b/src/expr.rs
@@ -0,0 +1,157 @@
+use std::collections::HashMap;
+
+use crate::dpll::Index;
+
+#[derive(Debug, Clone)]
+pub enum Expr {
+    Literal(String),
+    Not(Box<Expr>),
+    And(Vec<Expr>),
+    Or(Vec<Expr>),
+}
+
+impl Expr {
+    pub fn disjunctiveNormalForm(self) -> Self {
+        match self {
+            Expr::Literal(_) => self,
+            Expr::Not(n) => match *n {
+                Expr::Literal(_) => Expr::Not(n),
+                Expr::Not(i) => i.disjunctiveNormalForm(),
+                Expr::And(v) => Expr::Or(v.into_iter().map(|e| Expr::Not(Box::new(e))).collect())
+                    .disjunctiveNormalForm(),
+                Expr::Or(v) => Expr::And(v.into_iter().map(|e| Expr::Not(Box::new(e))).collect())
+                    .disjunctiveNormalForm(),
+            },
+            Expr::And(v) => {
+                let v = v
+                    .into_iter()
+                    .flat_map(|e| {
+                        if let Expr::And(v) = e {
+                            v.into_iter()
+                        } else {
+                            vec![e].into_iter()
+                        }
+                    })
+                    .collect::<Vec<_>>();
+
+                if v.iter()
+                    .all(|e| matches!(e, Expr::Literal(_) | Expr::Not(_)))
+                {
+                    return Expr::Or(vec![Expr::And(v)]);
+                }
+
+                if v.len() == 1 {
+                    v.into_iter().next().unwrap()
+                } else {
+                    let mut iter = v.into_iter();
+                    let mut v = match iter.next().unwrap().disjunctiveNormalForm() {
+                        Expr::Literal(s) => vec![Expr::Literal(s)],
+                        Expr::Not(n) => vec![Expr::Not(n)],
+                        Expr::And(_) => unreachable!(),
+                        Expr::Or(v) => v,
+                    };
+
+                    for e in iter {
+                        v = v
+                            .into_iter()
+                            .map(|i| Expr::And(vec![e.clone(), i]).disjunctiveNormalForm())
+                            .collect()
+                    }
+
+                    Expr::Or(v).disjunctiveNormalForm()
+                }
+            }
+            Expr::Or(v) => Expr::Or(
+                v.into_iter()
+                    .flat_map(|e| match e.disjunctiveNormalForm() {
+                        Expr::Literal(s) => vec![Expr::Literal(s)].into_iter(),
+                        Expr::Not(n) => vec![Expr::Not(n)].into_iter(),
+                        Expr::And(_) => unreachable!(),
+                        Expr::Or(o) => o.into_iter(),
+                    })
+                    .collect(),
+            ),
+        }
+    }
+
+    pub fn conjunctiveNormalForm(self) -> Self {
+        if let Expr::Or(v) = Expr::Not(Box::new(self)).disjunctiveNormalForm() {
+            Expr::And(
+                v.into_iter()
+                    .map(|e| {
+                        if let Expr::And(v) = e {
+                            Expr::Or(
+                                v.into_iter()
+                                    .map(|e| match e {
+                                        Expr::Literal(s) => Expr::Not(Box::new(Expr::Literal(s))),
+                                        Expr::Not(n) => *n,
+                                        Expr::And(_) => unreachable!(),
+                                        Expr::Or(_) => unreachable!(),
+                                    })
+                                    .collect(),
+                            )
+                        } else {
+                            unreachable!()
+                        }
+                    })
+                    .collect(),
+            )
+        } else {
+            unreachable!()
+        }
+    }
+
+    pub fn to_dpll_cnf(self) -> (Vec<Vec<Index>>, HashMap<String, Index>) {
+        let mut map = HashMap::new();
+
+        let mut cnf = Vec::new();
+
+        let v = if let Expr::And(v) = self.conjunctiveNormalForm() {
+            v
+        } else {
+            unreachable!()
+        };
+
+        let mut nextfree = 1;
+
+        for e in v {
+            let mut s = Vec::new();
+
+            let v = if let Expr::Or(v) = e {
+                v
+            } else {
+                unreachable!()
+            };
+
+            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;
+                    }
+                } 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;
+                        }
+                    } else {
+                        unreachable!()
+                    }
+                } else {
+                    unreachable!()
+                }
+            }
+
+            cnf.push(s);
+        }
+
+        (cnf, map)
+    }
+}
diff --git a/src/main.rs b/src/main.rs
index 2f797da..4cf4759 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -1,22 +1,50 @@
 use dpll::dpll;
+use expr::Expr;
 
 mod dpll;
 
+mod expr;
+
 fn main() {
+    let v = Expr::Not(Box::new(Expr::And(vec![
+        Expr::Or(vec![
+            Expr::Literal(String::from("a")),
+            Expr::Literal(String::from("b")),
+        ]),
+        Expr::Or(vec![
+            Expr::Literal(String::from("c")),
+            Expr::Literal(String::from("d")),
+        ]),
+    ])));
+
+    dbg!(&v);
+
+    dbg!(v.clone().disjunctiveNormalForm());
+    dbg!(v.clone().conjunctiveNormalForm());
+
+    let (cnf, _) = dbg!(v.clone().to_dpll_cnf());
+
     let mut solution = Vec::new();
-
-    let cnf = vec![
-        vec![-1, 2, 3],
-        vec![1, 3, 4],
-        vec![-4, 1, 3],
-        vec![-3, 1, 4],
-        vec![-4, -3, 1],
-        vec![-3, -2, 4],
-        vec![-3, -1, 2],
-        vec![-2, -1, 3],
-    ];
-
     dbg!(dpll(&cnf, &mut solution));
 
     dbg!(solution);
 }
+
+// fn main() {
+//     let mut solution = Vec::new();
+
+//     let cnf = vec![
+//         vec![-1, 2, 3],
+//         vec![1, 3, 4],
+//         vec![-4, 1, 3],
+//         vec![-3, 1, 4],
+//         vec![-4, -3, 1],
+//         vec![-3, -2, 4],
+//         vec![-3, -1, 2],
+//         vec![-2, -1, 3],
+//     ];
+
+//     dbg!(dpll(&cnf, &mut solution));
+
+//     dbg!(solution);
+// }