Submitted satisfiability/dpll_backtracking

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

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.");
+}

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