diff --git a/Cargo.lock b/Cargo.lock
index edb94c3..897ae02 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -5,3 +5,57 @@ version = 4
 [[package]]
 name = "bg-sat"
 version = "0.1.0"
+dependencies = [
+ "rayon",
+]
+
+[[package]]
+name = "crossbeam-deque"
+version = "0.8.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9dd111b7b7f7d55b72c0a6ae361660ee5853c9af73f70c3c2ef6858b950e2e51"
+dependencies = [
+ "crossbeam-epoch",
+ "crossbeam-utils",
+]
+
+[[package]]
+name = "crossbeam-epoch"
+version = "0.9.18"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5b82ac4a3c2ca9c3460964f020e1402edd5753411d7737aa39c3714ad1b5420e"
+dependencies = [
+ "crossbeam-utils",
+]
+
+[[package]]
+name = "crossbeam-utils"
+version = "0.8.21"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d0a5c400df2834b80a4c3327b3aad3a4c4cd4de0629063962b03235697506a28"
+
+[[package]]
+name = "either"
+version = "1.15.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "48c757948c5ede0e46177b7add2e67155f70e33c07fea8284df6576da70b3719"
+
+[[package]]
+name = "rayon"
+version = "1.10.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b418a60154510ca1a002a752ca9714984e21e4241e804d32555251faf8b78ffa"
+dependencies = [
+ "either",
+ "rayon-core",
+]
+
+[[package]]
+name = "rayon-core"
+version = "1.12.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1465873a3dfdaa8ae7cb14b4383657caab0b3e8a0aa9ae8e04b044854c8dfce2"
+dependencies = [
+ "crossbeam-deque",
+ "crossbeam-utils",
+]
diff --git a/Cargo.toml b/Cargo.toml
index c0b9860..fe08a47 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -4,3 +4,4 @@ version = "0.1.0"
 edition = "2024"
 
 [dependencies]
+rayon = "1.10.0"
diff --git a/src/dimacs.rs b/src/dimacs.rs
index e2f3954..a0ab51d 100644
--- a/src/dimacs.rs
+++ b/src/dimacs.rs
@@ -1,4 +1,6 @@
+use rayon::prelude::*;
 use std::collections::HashMap;
+use std::sync::Mutex;
 
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub struct Variable {
@@ -7,10 +9,12 @@ pub struct Variable {
 }
 
 impl Variable {
+    #[inline]
     pub fn positive(&self) -> i32 {
         self.id
     }
 
+    #[inline]
     pub fn negative(&self) -> i32 {
         -self.id
     }
@@ -18,7 +22,7 @@ impl Variable {
 
 pub struct CnfBuilder {
     variables: HashMap<String, Variable>,
-    clauses: Vec<Vec<i32>>,
+    clauses: Mutex<Vec<Vec<i32>>>,
     variable_counter: i32,
 }
 
@@ -26,17 +30,17 @@ impl CnfBuilder {
     pub fn new() -> Self {
         Self {
             variables: HashMap::new(),
-            clauses: Vec::new(),
+            clauses: Mutex::new(Vec::new()),
             variable_counter: 1,
         }
     }
 
     pub fn clause_count(&self) -> usize {
-        self.clauses.len()
+        self.clauses.lock().unwrap().len()
     }
 
-    pub fn get_clauses(&self) -> &Vec<Vec<i32>> {
-        &self.clauses
+    pub fn get_clauses(&self) -> Vec<Vec<i32>> {
+        self.clauses.lock().unwrap().clone()
     }
 
     pub fn variable(&mut self, name: String) -> Variable {
@@ -60,7 +64,7 @@ impl CnfBuilder {
     }
 
     pub fn clause(&mut self, literals: &[i32]) -> &mut Self {
-        self.clauses.push(literals.to_vec());
+        self.clauses.lock().unwrap().push(literals.to_vec());
         self
     }
 
@@ -76,10 +80,14 @@ impl CnfBuilder {
 
     pub fn at_most_k_true(&mut self, k: usize, vars: &[Variable]) -> &mut Self {
         if k + 1 <= vars.len() {
-            for combo in combinations(vars, k + 1) {
-                let clause: Vec<i32> = combo.iter().map(|v| v.negative()).collect();
-                self.clause(&clause);
-            }
+            let combinations = generate_combinations_optimized(vars, k + 1);
+
+            let new_clauses: Vec<Vec<i32>> = combinations
+                .into_par_iter()
+                .map(|combo| combo.iter().map(|v| v.negative()).collect())
+                .collect();
+
+            self.clauses.lock().unwrap().extend(new_clauses);
         }
 
         self
@@ -91,20 +99,30 @@ impl CnfBuilder {
         }
 
         if k <= vars.len() {
+            let mut all_new_clauses = Vec::new();
+
             for i in 0..k {
-                for combo in combinations(vars, i) {
-                    let clause: Vec<i32> = combo.iter().map(|v| v.negative()).collect();
+                let all_combinations = generate_combinations_optimized(vars, i);
 
-                    let rest: Vec<i32> = vars
-                        .iter()
-                        .filter(|v| !combo.contains(v))
-                        .map(|v| v.positive())
-                        .collect();
+                let new_clauses: Vec<Vec<i32>> = all_combinations
+                    .into_par_iter()
+                    .map(|combo| {
+                        let negated_combo: Vec<i32> = combo.iter().map(|v| v.negative()).collect();
 
-                    let clause: Vec<i32> = [clause, rest].concat();
-                    self.clause(&clause);
-                }
+                        let rest: Vec<i32> = vars
+                            .iter()
+                            .filter(|v| !combo.contains(v))
+                            .map(|v| v.positive())
+                            .collect();
+
+                        [negated_combo, rest].concat()
+                    })
+                    .collect();
+
+                all_new_clauses.extend(new_clauses);
             }
+
+            self.clauses.lock().unwrap().extend(all_new_clauses);
         } else {
             self.clause(&[]);
         }
@@ -114,10 +132,11 @@ impl CnfBuilder {
     pub fn to_dimacs(&self) -> String {
         let mut result = String::new();
 
+        let clauses = self.clauses.lock().unwrap();
         result.push_str(&format!(
             "p cnf {} {}\n",
             self.variable_counter - 1,
-            self.clauses.len()
+            clauses.len()
         ));
 
         let mut sorted_vars = self.variables.values().cloned().collect::<Vec<_>>();
@@ -127,7 +146,7 @@ impl CnfBuilder {
             result.push_str(&format!("c {}: {}\n", var.name, var.id));
         }
 
-        for clause in &self.clauses {
+        for clause in &*clauses {
             for &literal in clause {
                 result.push_str(&format!("{} ", literal));
             }
@@ -136,9 +155,54 @@ impl CnfBuilder {
 
         result
     }
+
+    pub fn add_clauses_batch(&mut self, clauses: Vec<Vec<i32>>) {
+        self.clauses.lock().unwrap().extend(clauses);
+    }
+
+    pub fn with_capacity(capacity: usize) -> Self {
+        Self {
+            variables: HashMap::new(),
+            clauses: Mutex::new(Vec::with_capacity(capacity)),
+            variable_counter: 1,
+        }
+    }
 }
 
-fn combinations<T: Clone>(items: &[T], k: usize) -> Vec<Vec<T>> {
+fn generate_combinations_optimized<T: Clone + Send + Sync>(items: &[T], k: usize) -> Vec<Vec<T>> {
+    if k == 0 {
+        return vec![vec![]];
+    }
+    if items.is_empty() {
+        return vec![];
+    }
+    if k == 1 {
+        return items.iter().map(|item| vec![item.clone()]).collect();
+    }
+
+    if items.len() < 10 {
+        return combinations_sequential(items, k);
+    }
+
+    let first_element = items[0].clone();
+    let remaining = &items[1..];
+
+    let (mut with_first, without_first) = rayon::join(
+        || {
+            let mut combos = generate_combinations_optimized(remaining, k - 1);
+            for combo in &mut combos {
+                combo.insert(0, first_element.clone());
+            }
+            combos
+        },
+        || generate_combinations_optimized(remaining, k),
+    );
+
+    with_first.extend(without_first);
+    with_first
+}
+
+fn combinations_sequential<T: Clone>(items: &[T], k: usize) -> Vec<Vec<T>> {
     if k == 0 {
         return vec![vec![]];
     }
@@ -146,11 +210,15 @@ fn combinations<T: Clone>(items: &[T], k: usize) -> Vec<Vec<T>> {
         return vec![];
     }
 
-    let mut result = combinations(&items[1..], k - 1);
-    for combo in &mut result {
-        combo.insert(0, items[0].clone());
+    let first_element = items[0].clone();
+    let remaining = &items[1..];
+
+    let mut with_first = combinations_sequential(remaining, k - 1);
+    for combo in &mut with_first {
+        combo.insert(0, first_element.clone());
     }
 
-    result.extend(combinations(&items[1..], k));
-    result
+    let without_first = combinations_sequential(remaining, k);
+
+    [with_first, without_first].concat()
 }
diff --git a/src/main.rs b/src/main.rs
index 73382cf..9a2796e 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -3,7 +3,7 @@ pub mod dimacs;
 fn main() {
     let mut cnf = dimacs::CnfBuilder::new();
 
-    let vars = cnf.variables("x", 0..40);
+    let vars = cnf.variables("x", 0..7);
 
     cnf.at_least_k_true(5, &vars);
     cnf.at_most_k_true(5, &vars);