diff --git a/conjure_oxide/src/ast.rs b/conjure_oxide/src/ast.rs
index 90f583f13..8bfd3bf0f 100644
--- a/conjure_oxide/src/ast.rs
+++ b/conjure_oxide/src/ast.rs
@@ -45,4 +45,6 @@ pub enum Expression {
     Sum(Vec<Expression>),
     Eq(Box<Expression>, Box<Expression>),
     Geq(Box<Expression>, Box<Expression>),
+    Not(Box<Expression>),
+    Or(Vec<Expression>),
 }
diff --git a/conjure_oxide/src/lib.rs b/conjure_oxide/src/lib.rs
index 851c0bc27..1ddc3a670 100644
--- a/conjure_oxide/src/lib.rs
+++ b/conjure_oxide/src/lib.rs
@@ -1 +1,2 @@
 pub mod ast;
+mod solvers;
\ No newline at end of file
diff --git a/conjure_oxide/src/solvers/kissat.rs b/conjure_oxide/src/solvers/kissat.rs
new file mode 100644
index 000000000..c3002d661
--- /dev/null
+++ b/conjure_oxide/src/solvers/kissat.rs
@@ -0,0 +1,113 @@
+use crate::ast::{DecisionVariable, Domain, Expression, Model, Name};
+use std::collections::HashMap;
+use String;
+
+type CNF = Vec<Vec<i32>>;
+type Error = String;
+
+/// Loop over variable names and assign indices to them for the CNF format. If a variable is not boolean, raise error.
+fn make_indices(vars: &HashMap<Name, DecisionVariable>) -> Result<HashMap<&Name, i32>, Error> {
+    let mut ans: HashMap<&Name, i32> = HashMap::new();
+    let mut next_index = 1;
+
+    for name in vars.keys() {
+        let variable: &DecisionVariable = vars.get(name).unwrap();
+        match variable.domain {
+            Domain::BoolDomain => {
+                ans.insert(name, next_index);
+                next_index += 1;
+            }
+            _ => {
+                return Err(String::from(
+                    "Could not convert (Model -> CNF):\
+                 all variables must belong to domain BoolDomain!",
+                ))
+            }
+        }
+    }
+
+    return Ok(ans);
+}
+
+/// Convert a single expression into a row of the CNF format
+fn convert_expression(
+    expression: &Expression,
+    symbol_table: &HashMap<&Name, i32>,
+) -> Result<Vec<i32>, Error> {
+    let mut ans: Vec<i32> = vec![];
+
+    match expression {
+        Expression::Reference(name) => match symbol_table.get(&name) {
+            // If it's a variable, just get its index
+            None => {
+                let str_name = match name {
+                    Name::UserName(s_name) => s_name.clone(),
+                    Name::MachineName(i_name) => i_name.to_string(),
+                };
+                return Err(format!("Variable with name {str_name} not found!"));
+            }
+            Some(ind) => {
+                ans.push(*ind);
+            }
+        },
+        Expression::Not(var_box) => {
+            let expr = var_box.as_ref();
+            match expr {
+                // Expression inside the Not()
+                Expression::Reference(_) => {
+                    // If it's a variable, get its index by calling
+                    // convert_expression again, and add a -
+                    let ret = convert_expression(expr, symbol_table)?;
+                    let ind = *ret.first().unwrap();
+                    ans.push(-ind);
+                }
+                _ => {
+                    return Err(String::from(
+                        "Expected Model to be in CNF form,\
+                 expression inside Not must always be a Reference!",
+                    ))
+                }
+            }
+        }
+        Expression::Or(expressions) => {
+            // If it's an Or, we just need to convert expressions inside it and flatten the result
+            for expr in expressions {
+                let ret = convert_expression(expr, symbol_table)?;
+                for ind in ret {
+                    ans.push(ind);
+                }
+            }
+        }
+        _ => {
+            return Err(String::from(
+                "Expected Model to be in CNF form,\
+        only Reference, Not(Reference) and Or(...) allowed!",
+            ))
+        }
+    }
+
+    return Ok(ans);
+}
+
+/// Expects Model to be in the Conjunctive Normal Form:
+/// - All variables must be boolean
+/// - Expressions must be Reference, Not(Reference), or Or(Reference1, Not(Reference2), ...)
+impl TryFrom<Model> for CNF {
+    type Error = Error;
+    fn try_from(conjure_model: Model) -> Result<Self, Self::Error> {
+        let mut ans: Vec<Vec<i32>> = vec![];
+        let constraints = conjure_model.constraints;
+        let variables = conjure_model.variables;
+
+        let names_to_indices: HashMap<&Name, i32> = make_indices(&variables)?;
+
+        for expression in constraints.iter() {
+            match convert_expression(expression, &names_to_indices) {
+                Ok(row) => ans.push(row),
+                Err(msg) => return Err(format!("Could not convert (Model -> CNF): {msg}")),
+            }
+        }
+
+        return Ok(ans);
+    }
+}
diff --git a/conjure_oxide/src/solvers/mod.rs b/conjure_oxide/src/solvers/mod.rs
new file mode 100644
index 000000000..7b58d4848
--- /dev/null
+++ b/conjure_oxide/src/solvers/mod.rs
@@ -0,0 +1 @@
+pub mod kissat;
\ No newline at end of file
diff --git a/solvers/chuffed/libwrapper.a b/solvers/chuffed/libwrapper.a
index 2b9638b4f..ece196ecc 100644
Binary files a/solvers/chuffed/libwrapper.a and b/solvers/chuffed/libwrapper.a differ
diff --git a/solvers/chuffed/wrapper.o b/solvers/chuffed/wrapper.o
index 5a7014984..6af35caa0 100644
Binary files a/solvers/chuffed/wrapper.o and b/solvers/chuffed/wrapper.o differ