"Player 0x40ba72637962bbeb3da5c36780ff8adea7e9cdfb submitted 'schnoin…

…g' for challenge satisfiability"

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

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 }))
+}