From 959ac83124153c4e8bb2f66179ebbf9a3440a131 Mon Sep 17 00:00:00 2001
From: hal8174 <henning.lindemann@pm.me>
Date: Tue, 8 Oct 2024 21:21:17 +0200
Subject: [PATCH] Initial commit

---
 .gitignore  |  1 +
 Cargo.lock  |  7 ++++
 Cargo.toml  |  6 ++++
 src/dpll.rs | 97 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 src/main.rs | 22 ++++++++++++
 5 files changed, 133 insertions(+)
 create mode 100644 .gitignore
 create mode 100644 Cargo.lock
 create mode 100644 Cargo.toml
 create mode 100644 src/dpll.rs
 create mode 100644 src/main.rs

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..ea8c4bf
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+/target
diff --git a/Cargo.lock b/Cargo.lock
new file mode 100644
index 0000000..362bf7f
--- /dev/null
+++ b/Cargo.lock
@@ -0,0 +1,7 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 3
+
+[[package]]
+name = "simple-sat-solver"
+version = "0.1.0"
diff --git a/Cargo.toml b/Cargo.toml
new file mode 100644
index 0000000..4608f86
--- /dev/null
+++ b/Cargo.toml
@@ -0,0 +1,6 @@
+[package]
+name = "simple-sat-solver"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
diff --git a/src/dpll.rs b/src/dpll.rs
new file mode 100644
index 0000000..2b408f5
--- /dev/null
+++ b/src/dpll.rs
@@ -0,0 +1,97 @@
+use std::collections::HashSet;
+
+type Index = i16;
+
+fn remvove_literal(cnf: &mut Vec<Vec<Index>>, l: Index) {
+    cnf.retain(|c| c.binary_search(&l).is_err());
+
+    for c in cnf {
+        if let Ok(i) = c.binary_search(&(-l)) {
+            c.remove(i);
+        }
+    }
+}
+
+fn unit_propagate(cnf: &mut Vec<Vec<Index>>, solution: &mut Vec<Index>) {
+    if let Some(i) = cnf
+        .iter()
+        .rev()
+        .position(|c| c.len() == 1)
+        .map(|i| cnf.len() - i - 1)
+    {
+        let l = cnf[i][0];
+        solution.push(l);
+        cnf.swap_remove(i);
+        remvove_literal(cnf, l);
+        unit_propagate(cnf, solution);
+    }
+}
+
+fn pure_literal_assign(cnf: &mut Vec<Vec<Index>>, solution: &mut Vec<Index>) {
+    let mut literals: HashSet<Index> = HashSet::new();
+    for c in cnf.iter() {
+        literals.extend(c.iter());
+    }
+
+    for &l in &literals {
+        if !literals.contains(&(-l)) {
+            solution.push(l);
+            remvove_literal(cnf, l);
+        }
+    }
+}
+
+pub fn dpll(cnf: &[Vec<Index>], solution: &mut Vec<Index>) -> bool {
+    let prev_solution = solution.len();
+    let mut own_cnf = cnf.to_owned();
+
+    unit_propagate(&mut own_cnf, solution);
+    pure_literal_assign(&mut own_cnf, solution);
+
+    if own_cnf.is_empty() {
+        return true;
+    }
+
+    if own_cnf.iter().any(|c| c.is_empty()) {
+        solution.resize(prev_solution, 0);
+        return false;
+    }
+
+    let literal = own_cnf[0][0];
+
+    own_cnf.push(vec![literal]);
+    if dpll(&own_cnf, solution) {
+        return true;
+    }
+
+    own_cnf.last_mut().unwrap()[0] = -literal;
+    if dpll(&own_cnf, solution) {
+        return true;
+    }
+
+    solution.resize(prev_solution, 0);
+    false
+}
+
+#[cfg(test)]
+mod test {
+    use super::dpll;
+
+    #[test]
+    fn wikipedia() {
+        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],
+        ];
+
+        let mut solution = Vec::new();
+
+        assert!(dpll(&cnf, &mut solution));
+    }
+}
diff --git a/src/main.rs b/src/main.rs
new file mode 100644
index 0000000..2f797da
--- /dev/null
+++ b/src/main.rs
@@ -0,0 +1,22 @@
+use dpll::dpll;
+
+mod dpll;
+
+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);
+}