From 713004281855dea656cdf599c9c4b4d9cff02d0b Mon Sep 17 00:00:00 2001
From: 0x40ba72637962bbeb3da5c36780ff8adea7e9cdfb <contact@tig.foundation>
Date: Tue, 23 Apr 2024 15:34:37 +0000
Subject: [PATCH] "Player 0x40ba72637962bbeb3da5c36780ff8adea7e9cdfb submitted
 'schnoing' for challenge satisfiability"

---
 tig-algorithms/src/satisfiability/mod.rs      |  2 +-
 tig-algorithms/src/satisfiability/schnoing.rs | 50 +++++++++++++++++++
 2 files changed, 51 insertions(+), 1 deletion(-)
 create mode 100644 tig-algorithms/src/satisfiability/schnoing.rs

diff --git a/tig-algorithms/src/satisfiability/mod.rs b/tig-algorithms/src/satisfiability/mod.rs
index 71a70334..52b53110 100644
--- a/tig-algorithms/src/satisfiability/mod.rs
+++ b/tig-algorithms/src/satisfiability/mod.rs
@@ -1,4 +1,4 @@
-// c001_a001 placeholder
+pub mod schnoing;
 // c001_a002 placeholder
 // c001_a003 placeholder
 // c001_a004 placeholder
diff --git a/tig-algorithms/src/satisfiability/schnoing.rs b/tig-algorithms/src/satisfiability/schnoing.rs
new file mode 100644
index 00000000..01b22c7c
--- /dev/null
+++ b/tig-algorithms/src/satisfiability/schnoing.rs
@@ -0,0 +1,50 @@
+use rand::{rngs::StdRng, Rng, SeedableRng};
+use tig_challenges::satisfiability::*;
+
+pub fn solve_challenge(challenge: &Challenge) -> anyhow::Result<Option<Solution>> {
+    let mut rng = StdRng::seed_from_u64(challenge.seed as u64);
+    let num_variables = challenge.difficulty.num_variables;
+    let mut variables: Vec<bool> = (0..num_variables).map(|_| rng.gen::<bool>()).collect();
+
+    // Pre-generate a bunch of random integers
+    // IMPORTANT! When generating random numbers, never use usize! usize bytes varies from system to system
+    let rand_ints: Vec<usize> = (0..2 * num_variables)
+        .map(|_| rng.gen_range(0..1_000_000_000u32) as usize)
+        .collect();
+
+    for i in 0..num_variables {
+        // Evaluate clauses and find any that are unsatisfied
+        let substituted: Vec<bool> = challenge
+            .clauses
+            .iter()
+            .map(|clause| {
+                clause.iter().any(|&literal| {
+                    let var_idx = literal.abs() as usize - 1;
+                    let var_value = variables[var_idx];
+                    (literal > 0 && var_value) || (literal < 0 && !var_value)
+                })
+            })
+            .collect();
+
+        let unsatisfied_clauses: Vec<usize> = substituted
+            .iter()
+            .enumerate()
+            .filter_map(|(idx, &satisfied)| if !satisfied { Some(idx) } else { None })
+            .collect();
+
+        let num_unsatisfied_clauses = unsatisfied_clauses.len();
+        if num_unsatisfied_clauses == 0 {
+            break;
+        }
+
+        // Flip the value of a random variable from a random unsatisfied clause
+        let rand_unsatisfied_clause_idx = rand_ints[2 * i] % num_unsatisfied_clauses;
+        let rand_unsatisfied_clause = unsatisfied_clauses[rand_unsatisfied_clause_idx];
+        let rand_variable_idx = rand_ints[2 * i + 1] % 3;
+        let rand_variable =
+            challenge.clauses[rand_unsatisfied_clause][rand_variable_idx].abs() as usize - 1;
+        variables[rand_variable] = !variables[rand_variable];
+    }
+
+    Ok(Some(Solution { variables }))
+}