diff --git a/tig-algorithms/src/satisfiability/inbound/README.md b/tig-algorithms/src/satisfiability/inbound/README.md new file mode 100644 index 00000000..32a5f65e --- /dev/null +++ b/tig-algorithms/src/satisfiability/inbound/README.md @@ -0,0 +1,23 @@ +# TIG Code Submission + +## Submission Details + +* **Challenge Name:** satisfiability +* **Algorithm Name:** inbound +* **Copyright:** 2024 Clifford Algueraz +* **Identity of Submitter:** Clifford Algueraz +* **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/inbound/mod.rs b/tig-algorithms/src/satisfiability/inbound/mod.rs new file mode 100644 index 00000000..7fcb8723 --- /dev/null +++ b/tig-algorithms/src/satisfiability/inbound/mod.rs @@ -0,0 +1,241 @@ +use rand::{rngs::StdRng, Rng, SeedableRng}; +use std::collections::HashMap; +use serde_json::{Map, Value}; +use tig_challenges::satisfiability::*; + +pub fn solve_challenge( + challenge: &Challenge, + save_solution: &dyn Fn(&Solution) -> anyhow::Result<()>, + hyperparameters: &Option>, +) -> anyhow::Result<()> { + let _ = save_solution(&Solution { variables: vec![false; challenge.num_variables] }); + let mut rng = StdRng::seed_from_u64(u64::from_le_bytes(challenge.seed[..8].try_into().unwrap()) as u64); + + let mut p_single = vec![false; challenge.num_variables]; + let mut n_single = vec![false; challenge.num_variables]; + + let mut clauses_ = challenge.clauses.clone(); + let mut clauses: Vec> = Vec::with_capacity(clauses_.len()); + + let mut dead = false; + + while !(dead) { + let mut done = true; + for c in &clauses_ { + let mut c_: Vec = Vec::with_capacity(c.len()); + let mut skip = false; + for (i, l) in c.iter().enumerate() { + if (p_single[(l.abs() - 1) as usize] && *l > 0) + || (n_single[(l.abs() - 1) as usize] && *l < 0) + || c[(i + 1)..].contains(&-l) + { + skip = true; + break; + } else if p_single[(l.abs() - 1) as usize] + || n_single[(l.abs() - 1) as usize] + || c[(i + 1)..].contains(&l) + { + done = false; + continue; + } else { + c_.push(*l); + } + } + if skip { + done = false; + continue; + }; + match c_[..] { + [l] => { + done = false; + if l > 0 { + if n_single[(l.abs() - 1) as usize] { + dead = true; + break; + } else { + p_single[(l.abs() - 1) as usize] = true; + } + } else { + if p_single[(l.abs() - 1) as usize] { + dead = true; + break; + } else { + n_single[(l.abs() - 1) as usize] = true; + } + } + } + [] => { + dead = true; + break; + } + _ => { + clauses.push(c_); + } + } + } + if done { + break; + } else { + clauses_ = clauses; + clauses = Vec::with_capacity(clauses_.len()); + } + } + + if dead { + return Ok(()); + } + + let num_variables = challenge.num_variables; + let num_clauses = clauses.len(); + + let mut p_clauses: Vec> = vec![vec![]; num_variables]; + let mut n_clauses: Vec> = vec![vec![]; num_variables]; + + let mut variables = vec![false; num_variables]; + for v in 0..num_variables { + if p_single[v] { + variables[v] = true + } else if n_single[v] { + variables[v] = false + } else { + variables[v] = rng.gen_bool(0.5) + } + } + let mut num_good_so_far: Vec = vec![0; num_clauses]; + + for (i, &ref c) in clauses.iter().enumerate() { + for &l in c { + let var = (l.abs() - 1) as usize; + if l > 0 { + p_clauses[var].push(i); + if variables[var] { + num_good_so_far[i] += 1 + } + } else { + n_clauses[var].push(i); + if !variables[var] { + num_good_so_far[i] += 1 + } + } + } + } + + let mut residual_ = Vec::with_capacity(num_clauses); + let mut residual_indices = HashMap::with_capacity(num_clauses); + + for (i, &num_good) in num_good_so_far.iter().enumerate() { + if num_good == 0 { + residual_.push(i); + residual_indices.insert(i, residual_.len() - 1); + } + } + + let mut attempts = 0; + loop { + if attempts >= num_variables * 25 { + return Ok(()); + } + if !residual_.is_empty() { + let i = residual_[0]; + let mut min_sad = clauses.len(); + let mut v_min_sad = vec![]; + let c = &clauses[i]; + for &l in c { + let mut sad = 0 as usize; + if variables[(l.abs() - 1) as usize] { + for &c in &p_clauses[(l.abs() - 1) as usize] { + if num_good_so_far[c] == 1 { + sad += 1; + if sad > min_sad { + break; + } + } + } + } else { + for &c in &n_clauses[(l.abs() - 1) as usize] { + if num_good_so_far[c] == 1 { + sad += 1; + if sad > min_sad { + break; + } + } + } + } + + if sad < min_sad { + min_sad = sad; + v_min_sad = vec![(l.abs() - 1) as usize]; + } else if sad == min_sad { + v_min_sad.push((l.abs() - 1) as usize); + } + } + let v = if min_sad == 0 { + if v_min_sad.len() == 1 { + v_min_sad[0] + } else { + v_min_sad[rng.gen_range(0..(v_min_sad.len() as u32)) as usize] + } + } else { + if rng.gen_bool(0.5) { + let l = c[rng.gen_range(0..(c.len() as u32)) as usize]; + (l.abs() - 1) as usize + } else { + v_min_sad[rng.gen_range(0..(v_min_sad.len() as u32)) as usize] + } + }; + + if variables[v] { + for &c in &n_clauses[v] { + num_good_so_far[c] += 1; + if num_good_so_far[c] == 1 { + let i = residual_indices.remove(&c).unwrap(); + let last = residual_.pop().unwrap(); + if i < residual_.len() { + residual_[i] = last; + residual_indices.insert(last, i); + } + } + } + for &c in &p_clauses[v] { + if num_good_so_far[c] == 1 { + residual_.push(c); + residual_indices.insert(c, residual_.len() - 1); + } + num_good_so_far[c] -= 1; + } + } else { + for &c in &n_clauses[v] { + if num_good_so_far[c] == 1 { + residual_.push(c); + residual_indices.insert(c, residual_.len() - 1); + } + num_good_so_far[c] -= 1; + } + + for &c in &p_clauses[v] { + num_good_so_far[c] += 1; + if num_good_so_far[c] == 1 { + let i = residual_indices.remove(&c).unwrap(); + let last = residual_.pop().unwrap(); + if i < residual_.len() { + residual_[i] = last; + residual_indices.insert(last, i); + } + } + } + } + + variables[v] = !variables[v]; + } else { + break; + } + attempts += 1; + } + + let _ = save_solution(&Solution { variables }); + return Ok(()); +} + +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..86b7334e 100644 --- a/tig-algorithms/src/satisfiability/mod.rs +++ b/tig-algorithms/src/satisfiability/mod.rs @@ -32,7 +32,8 @@ // c001_a017 -// c001_a018 +pub mod inbound; +pub use inbound as c001_a018; // c001_a019