From c3f294ed64d0b29d60fb74aabb4e701bd8dc5fbe Mon Sep 17 00:00:00 2001
From: FiveMovesAhead <ying@tig.foundation>
Date: Mon, 1 Dec 2025 15:19:09 +0000
Subject: [PATCH] Submitted satisfiability/dpll_backtracking

---
 .../dpll_backtracking/README.md               | 23 ++++++
 .../satisfiability/dpll_backtracking/mod.rs   | 76 +++++++++++++++++++
 tig-algorithms/src/satisfiability/mod.rs      |  3 +-
 3 files changed, 101 insertions(+), 1 deletion(-)
 create mode 100644 tig-algorithms/src/satisfiability/dpll_backtracking/README.md
 create mode 100644 tig-algorithms/src/satisfiability/dpll_backtracking/mod.rs

diff --git a/tig-algorithms/src/satisfiability/dpll_backtracking/README.md b/tig-algorithms/src/satisfiability/dpll_backtracking/README.md
new file mode 100644
index 00000000..4c1ea2e6
--- /dev/null
+++ b/tig-algorithms/src/satisfiability/dpll_backtracking/README.md
@@ -0,0 +1,23 @@
+# TIG Code Submission
+
+## Submission Details
+
+* **Challenge Name:** satisfiability
+* **Algorithm Name:** dpll_backtracking
+* **Copyright:** 2024 Chad Blanchard
+* **Identity of Submitter:** Chad Blanchard
+* **Identity of Creator of Algorithmic Method:** null
+* **Unique Algorithm Identifier (UAI):** null
+
+## License
+
+The files in this folder are under the following licenses:
+* TIG Benchmarker Outbound License
+* TIG Commercial License
+* TIG Inbound Game License
+* TIG Innovator Outbound Game License
+* TIG Open Data License
+* TIG THV Game License
+
+Copies of the licenses can be obtained at:
+https://github.com/tig-foundation/tig-monorepo/tree/main/docs/licenses
\ No newline at end of file
diff --git a/tig-algorithms/src/satisfiability/dpll_backtracking/mod.rs b/tig-algorithms/src/satisfiability/dpll_backtracking/mod.rs
new file mode 100644
index 00000000..035ffdb1
--- /dev/null
+++ b/tig-algorithms/src/satisfiability/dpll_backtracking/mod.rs
@@ -0,0 +1,76 @@
+// TIG's UI uses the pattern `tig_challenges::<challenge_name>` to automatically detect your algorithm's challenge
+
+use serde_json::{Map, Value};
+use tig_challenges::satisfiability::*;
+use std::collections::HashMap;
+
+pub fn solve_challenge(
+    challenge: &Challenge,
+    save_solution: &dyn Fn(&Solution) -> anyhow::Result<()>,
+    hyperparameters: &Option<Map<String, Value>>,
+) -> anyhow::Result<()> {
+    let _ = save_solution(&Solution { variables: vec![false; challenge.num_variables] });
+    let num_variables = challenge.num_variables;
+    let mut assignment = vec![None; num_variables];
+
+    if dpll(&challenge.clauses, &mut assignment) {
+        let variables = assignment.into_iter().map(|x| x.unwrap_or(false)).collect();
+        let _ = save_solution(&Solution { variables });
+        return Ok(());
+    } else {
+        Ok(())
+    }
+}
+
+fn dpll(clauses: &[Vec<i32>], assignment: &mut [Option<bool>]) -> bool {
+    if clauses.is_empty() {
+        return true;
+    }
+
+    if clauses.iter().any(|clause| clause.is_empty()) {
+        return false;
+    }
+
+    let unit_clauses: Vec<&Vec<i32>> = clauses.iter().filter(|clause| clause.len() == 1).collect();
+    for unit in unit_clauses {
+        let literal = unit[0];
+        let var = literal.abs() as usize - 1;
+        let value = literal > 0;
+        if assignment[var].is_some() && assignment[var] != Some(value) {
+            return false;
+        }
+        assignment[var] = Some(value);
+    }
+
+    let mut pure_literals: HashMap<i32, bool> = HashMap::new();
+    for clause in clauses {
+        for &literal in clause {
+            let var = literal.abs();
+            if !pure_literals.contains_key(&var) {
+                pure_literals.insert(var, literal > 0);
+            }
+        }
+    }
+    for (&var, &value) in pure_literals.iter() {
+        let index = var as usize - 1;
+        if assignment[index].is_none() {
+            assignment[index] = Some(value);
+        }
+    }
+
+    let first_unassigned = assignment.iter().position(|&x| x.is_none()).unwrap();
+    assignment[first_unassigned] = Some(true);
+    if dpll(clauses, assignment) {
+        return true;
+    }
+    assignment[first_unassigned] = Some(false);
+    if dpll(clauses, assignment) {
+        return true;
+    }
+    assignment[first_unassigned] = None;
+    false
+}
+
+pub fn help() {
+    println!("No help information available.");
+}
diff --git a/tig-algorithms/src/satisfiability/mod.rs b/tig-algorithms/src/satisfiability/mod.rs
index 22d6805c..c6bf63d1 100644
--- a/tig-algorithms/src/satisfiability/mod.rs
+++ b/tig-algorithms/src/satisfiability/mod.rs
@@ -1,6 +1,7 @@
 // c001_a001
 
-// c001_a002
+pub mod dpll_backtracking;
+pub use dpll_backtracking as c001_a002;
 
 // c001_a003