Skip to content

Commit

Permalink
Merge remote-tracking branch 'public/test/satisfiability/schnoing' in…
Browse files Browse the repository at this point in the history
…to test/temp
  • Loading branch information
FiveMovesAhead committed Apr 25, 2024
2 parents 54de92f + 5686528 commit f5798e1
Show file tree
Hide file tree
Showing 3 changed files with 51 additions and 1 deletion.
2 changes: 1 addition & 1 deletion tig-algorithms/src/satisfiability/mod.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// c001_a001 placeholder
pub mod schnoing;
// c001_a002 placeholder
// c001_a003 placeholder
// c001_a004 placeholder
Expand Down
50 changes: 50 additions & 0 deletions tig-algorithms/src/satisfiability/schnoing.rs
Original file line number Diff line number Diff line change
@@ -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 }))
}
Binary file added tig-algorithms/wasm/satisfiability/schnoing.wasm
Binary file not shown.

0 comments on commit f5798e1

Please sign in to comment.