From dc6fb09d280b663fdf91cbff035a5821b0233dda Mon Sep 17 00:00:00 2001 From: FiveMovesAhead Date: Mon, 1 Dec 2025 15:21:09 +0000 Subject: [PATCH] Submitted satisfiability/sat_sigma --- tig-algorithms/src/satisfiability/mod.rs | 3 +- .../src/satisfiability/sat_sigma/README.md | 23 + .../src/satisfiability/sat_sigma/mod.rs | 585 ++++++++++++++++++ 3 files changed, 610 insertions(+), 1 deletion(-) create mode 100644 tig-algorithms/src/satisfiability/sat_sigma/README.md create mode 100644 tig-algorithms/src/satisfiability/sat_sigma/mod.rs diff --git a/tig-algorithms/src/satisfiability/mod.rs b/tig-algorithms/src/satisfiability/mod.rs index 22d6805c..a0d7efc5 100644 --- a/tig-algorithms/src/satisfiability/mod.rs +++ b/tig-algorithms/src/satisfiability/mod.rs @@ -134,7 +134,8 @@ // c001_a068 -// c001_a069 +pub mod sat_sigma; +pub use sat_sigma as c001_a069; // c001_a070 diff --git a/tig-algorithms/src/satisfiability/sat_sigma/README.md b/tig-algorithms/src/satisfiability/sat_sigma/README.md new file mode 100644 index 00000000..e799be0f --- /dev/null +++ b/tig-algorithms/src/satisfiability/sat_sigma/README.md @@ -0,0 +1,23 @@ +# TIG Code Submission + +## Submission Details + +* **Challenge Name:** satisfiability +* **Algorithm Name:** sat_sigma +* **Copyright:** 2025 Rootz +* **Identity of Submitter:** Rootz +* **Identity of Creator of Algorithmic Method:** Rootz +* **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/sat_sigma/mod.rs b/tig-algorithms/src/satisfiability/sat_sigma/mod.rs new file mode 100644 index 00000000..a9b7d244 --- /dev/null +++ b/tig-algorithms/src/satisfiability/sat_sigma/mod.rs @@ -0,0 +1,585 @@ +use rand::{rngs::SmallRng, Rng, SeedableRng}; +use std::convert::TryInto; +use serde_json::{Map, Value}; +use tig_challenges::satisfiability::*; +use crate::{seeded_hasher, HashSet}; + +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 = SmallRng::seed_from_u64(u64::from_le_bytes( + challenge.seed[..8].try_into().unwrap(), + )); + let hasher = seeded_hasher(&challenge.seed); + + let mut clauses = challenge.clauses.clone(); + let mut i = clauses.len(); + while i > 0 { + i -= 1; + let clause = &mut clauses[i]; + + if clause.len() > 1 { + let mut seen = HashSet::with_hasher(hasher.clone()); + let mut j = 0; + let mut tautology = false; + while j < clause.len() { + let lit = clause[j]; + if seen.contains(&-lit) { + tautology = true; + break; + } + if !seen.insert(lit) { + clause.swap_remove(j); + } else { + j += 1; + } + } + if tautology { + clauses.swap_remove(i); + i += 1; + continue; + } + } + } + + let mut p_single = vec![false; challenge.num_variables]; + let mut n_single = vec![false; challenge.num_variables]; + let mut clauses_ = clauses; + clauses = 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 &l in c.iter() { + let idx = (l.abs() - 1) as usize; + if (p_single[idx] && l > 0) || (n_single[idx] && l < 0) { + skip = true; + break; + } + if p_single[idx] || n_single[idx] { + done = false; + continue; + } + 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(); + + if num_clauses == 0 { + 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; + } + } + let _ = save_solution(&Solution { variables }); + return Ok(()); + } + + let mut p_clauses: Vec> = vec![Vec::new(); num_variables]; + let mut n_clauses: Vec> = vec![Vec::new(); num_variables]; + + for (i, c) in clauses.iter().enumerate() { + for &l in c { + let var = (l.abs() - 1) as usize; + if l > 0 { + p_clauses[var].push(i); + } else { + n_clauses[var].push(i); + } + } + } + + let density = if num_variables > 0 { + num_clauses as f64 / num_variables as f64 + } else { + 0.0 + }; + let avg_clause_size = + clauses.iter().map(|c| c.len()).sum::() as f64 / num_clauses as f64; + + let nv = num_variables as f64; + let nad = 1.0; + let random_threshold = 0.003 + 0.007 / (1.0 + (-(nv - 30000.0) / 8000.0).exp()); + + let mut variables = vec![false; num_variables]; + for v in 0..num_variables { + let num_p = p_clauses[v].len(); + let num_n = n_clauses[v].len(); + + if num_n == 0 && num_p > 0 { + variables[v] = true; + continue; + } else if num_p == 0 && num_n > 0 { + variables[v] = false; + continue; + } + + let vad = if num_n > 0 { + num_p as f64 / num_n as f64 + } else { + nad + 1.0 + }; + let bias_prob = (num_p as f64 + 0.25) / ((num_p + num_n) as f64 + 1.2); + let steep = if density >= 4.19 && density <= 4.21 { + 0.27 + } else { + 0.35 / (1.0 + (density - 4.18).max(0.0) * 12.0) + }; + let s = 1.0 / (1.0 + (-(vad - nad) / steep).exp()); + let prob = (random_threshold * (1.0 - s) + bias_prob * s).max(0.0).min(1.0); + variables[v] = rng.gen_bool(prob); + } + + let mut num_good_so_far: Vec = vec![0; num_clauses]; + for (i, c) in clauses.iter().enumerate() { + for &l in c { + let var = (l.abs() - 1) as usize; + if (l > 0 && variables[var]) || (l < 0 && !variables[var]) { + num_good_so_far[i] = num_good_so_far[i].saturating_add(1); + } + } + } + + let mut residual_ = Vec::with_capacity(num_clauses); + let mut in_queue = vec![false; num_clauses]; + + for (i, &num_good) in num_good_so_far.iter().enumerate() { + if num_good == 0 { + in_queue[i] = true; + residual_.push(i); + } + } + + if residual_.is_empty() { + for v in 0..num_variables { + if p_single[v] { + variables[v] = true; + } else if n_single[v] { + variables[v] = false; + } + } + let _ = save_solution(&Solution { variables }); + return Ok(()); + } + + let base_prob = 0.45 + 0.1 * (density / 5.0).min(1.0); + let mut current_prob = base_prob; + + let large_problem_scale = + ((num_variables as f64 - 25000.0) / 35000.0).max(0.0).min(1.0); + let base_interval = 60.0 - 30.0 * large_problem_scale; + let min_interval = 25.0 - 10.0 * large_problem_scale; + let density_s = 1.0 / (1.0 + (-(density - 4.0) / 0.5).exp()); + let density_factor = 1.0 + 0.2 * density_s; + let check_interval = + (base_interval * density_factor * (1.0 + (density / 3.0).ln().max(0.0))).max(min_interval) + as usize; + let max_random_prob = 0.9; + let prob_adjustment_factor = if density >= 4.18 && density <= 4.22 { + 0.04 + } else { + 0.03 + }; + let smoothing_factor = if density >= 4.18 && density <= 4.22 { + 0.75 + } else { + 0.8 + }; + + let mut last_check_residual = residual_.len(); + let initial_residual_size = residual_.len(); + let size_scale = 1.0 / (1.0 + (-(nv - 30000.0) / 7000.0).exp()); + let perturbation_flips = if density >= 4.195 { + 4 + } else { + 1 + (2.0 * size_scale) as usize + }; + + let stagnation_limit = if density >= 4.19 && density <= 4.21 { + 2 + } else { + 2 + (2.0 * (1.0 - (density / 5.0).min(1.0))) as usize + }; + let mut stagnation = 0usize; + + let unsat_check_threshold = check_interval * 5; + let mut min_residual_seen = residual_.len(); + + let max_fuel = hyperparameters + .as_ref() + .and_then(|h| h.get("max_fuel")) + .and_then(|v| v.as_f64()) + .unwrap_or(10_000_000_000.0); + let difficulty_factor = density * avg_clause_size.sqrt(); + let scale_factor = + 1.0 + 0.5 * (1.0 / (1.0 + (-(nv - 25000.0) / 8000.0).exp())); + let base_fuel = + (2000.0 + 100.0 * difficulty_factor) * (num_variables as f64).sqrt() * scale_factor; + let flip_fuel = (200.0 + difficulty_factor) / scale_factor; + let remaining = (max_fuel - base_fuel).max(0.0); + let max_num_rounds = if flip_fuel > 0.0 { + (remaining / flip_fuel) as usize + } else { + 0 + }; + let mut rounds = 0; + + unsafe { + loop { + if rounds >= max_num_rounds { + return Ok(()); + } + + if residual_.len() < min_residual_seen { + min_residual_seen = residual_.len(); + } + + if rounds > unsat_check_threshold && rounds % check_interval == 0 { + let total_progress = initial_residual_size.saturating_sub(min_residual_seen); + let progress_pct = total_progress as f64 / initial_residual_size.max(1) as f64; + let residual_pct = min_residual_seen as f64 / initial_residual_size.max(1) as f64; + + let fuel_used_pct = rounds as f64 / max_num_rounds.max(1) as f64; + + let should_give_up = if fuel_used_pct > 0.7 { + progress_pct < 0.05 && residual_pct > 0.5 + } else if fuel_used_pct > 0.5 { + progress_pct < 0.10 && residual_pct > 0.7 + } else { + false + }; + + if should_give_up { + return Ok(()); + } + } + + if rounds % check_interval == 0 && rounds > 0 { + let progress = + last_check_residual as i64 - residual_.len() as i64; + let progress_ratio = + progress as f64 / last_check_residual.max(1) as f64; + + + let progress_threshold = if density >= 4.19 && density <= 4.21 { + 0.16 + 0.06 * (density / 3.0).min(1.0) + } else { + 0.15 + 0.05 * (density / 3.0).min(1.0) + }; + + if progress <= 0 { + stagnation = stagnation.saturating_add(1); + let density_adj = + 1.0 + (density - 4.18).max(0.0) * 10.0; + let prob_adjustment = prob_adjustment_factor + * density_adj + * (-progress as f64 + / last_check_residual.max(1) as f64) + .min(1.0); + current_prob = + (current_prob + prob_adjustment).min(max_random_prob); + + if stagnation >= stagnation_limit { + let extra = (stagnation > 2) as usize + (stagnation / 4); + let kicks = (perturbation_flips + extra).min(6); + for _ in 0..kicks { + if residual_.is_empty() { + break; + } + let id = rng.gen::() % residual_.len(); + let cid = residual_[id]; + let c = clauses.get_unchecked_mut(cid); + if c.is_empty() { + continue; + } + let lit = c[rng.gen::() % c.len()]; + let v = (lit.abs() as usize) - 1; + + let was_true = *variables.get_unchecked(v); + let inc = if was_true { + n_clauses.get_unchecked(v) + } else { + p_clauses.get_unchecked(v) + }; + let dec = if was_true { + p_clauses.get_unchecked(v) + } else { + n_clauses.get_unchecked(v) + }; + + for &cid2 in inc { + let num_good = + num_good_so_far.get_unchecked_mut(cid2); + *num_good = num_good.saturating_add(1); + } + for &cid2 in dec { + let num_good = + num_good_so_far.get_unchecked_mut(cid2); + let new_val = num_good.saturating_sub(1); + *num_good = new_val; + if new_val == 0 + && !*in_queue.get_unchecked(cid2) + { + *in_queue.get_unchecked_mut(cid2) = true; + residual_.push(cid2); + } + } + *variables.get_unchecked_mut(v) = !was_true; + } + stagnation = 0; + } + } else if progress_ratio > progress_threshold { + stagnation = 0; + current_prob = base_prob; + } else { + stagnation = 0; + current_prob = current_prob * smoothing_factor + + base_prob * (1.0 - smoothing_factor); + } + + last_check_residual = residual_.len(); + } + + if !residual_.is_empty() { + let rand_val = rng.gen::(); + + let mut i = residual_.len() - 1; + while !residual_.is_empty() { + let id1 = rng.gen::() % residual_.len(); + let id2 = rng.gen::() % residual_.len(); + let cid1 = residual_[id1]; + let cid2 = residual_[id2]; + let mut best_id = if clauses.get_unchecked(cid2).len() + < clauses.get_unchecked(cid1).len() + { + id2 + } else { + id1 + }; + if density >= 4.195 { + let id3 = rng.gen::() % residual_.len(); + let cid3 = residual_[id3]; + let best_cid = residual_[best_id]; + if clauses.get_unchecked(cid3).len() + < clauses.get_unchecked(best_cid).len() + { + best_id = id3; + } + } + i = residual_[best_id]; + if num_good_so_far[i] > 0 { + in_queue[i] = false; + residual_.swap_remove(best_id); + } else { + break; + } + } + if residual_.is_empty() { + for v in 0..num_variables { + if p_single[v] { + variables[v] = true; + } else if n_single[v] { + variables[v] = false; + } + } + save_solution(&Solution { variables })?; + return Ok(()); + } + + let c = clauses.get_unchecked_mut(i); + + if c.len() > 1 { + let random_index = rand_val % c.len(); + c.swap(0, random_index); + } + + let mut zero_found = None; + 'outer: for &l in c.iter() { + let abs_l = l.abs() as usize - 1; + let clauses_to_check = if *variables.get_unchecked(abs_l) { + p_clauses.get_unchecked(abs_l) + } else { + n_clauses.get_unchecked(abs_l) + }; + + for &c in clauses_to_check { + if *num_good_so_far.get_unchecked(c) == 1 { + continue 'outer; + } + } + zero_found = Some(abs_l); + break; + } + + let v = if let Some(abs_l) = zero_found { + abs_l + } else if rng.gen::() < current_prob { + c[0].abs() as usize - 1 + } else { + let mut min_sad = usize::MAX; + let mut v_min_sad = c[0].abs() as usize - 1; + let mut min_weight = usize::MAX; + + for &l in c.iter() { + let abs_l = l.abs() as usize - 1; + let clauses_to_check = if *variables.get_unchecked(abs_l) + { + p_clauses.get_unchecked(abs_l) + } else { + n_clauses.get_unchecked(abs_l) + }; + + let mut sad = 0; + + for &c_idx in clauses_to_check { + if *num_good_so_far.get_unchecked(c_idx) == 1 { + sad += 1; + } + if sad >= min_sad { + break; + } + } + + if sad == 0 { + + let curr_appearances = p_clauses.get_unchecked(abs_l).len() + + n_clauses.get_unchecked(abs_l).len(); + if min_sad > 0 || curr_appearances < min_weight { + min_sad = 0; + min_weight = curr_appearances; + v_min_sad = abs_l; + } + + } else { + + if min_sad > 0 { + let appearances = p_clauses.get_unchecked(abs_l).len() + + n_clauses.get_unchecked(abs_l).len(); + + let sad_weight = if density >= 4.19 && density <= 4.21 { + 1024 + } else if density >= 4.195 { + 512 + } else { + 256 + }; + let combined_weight = + sad * sad * sad_weight + appearances; + + if combined_weight < min_weight { + min_sad = sad; + min_weight = combined_weight; + v_min_sad = abs_l; + } + + if min_sad <= 1 { + break; + } + } + } + } + v_min_sad + }; + + let was_true = *variables.get_unchecked(v); + let clauses_to_decrement = if was_true { + p_clauses.get_unchecked(v) + } else { + n_clauses.get_unchecked(v) + }; + let clauses_to_increment = if was_true { + n_clauses.get_unchecked(v) + } else { + p_clauses.get_unchecked(v) + }; + + for &cid in clauses_to_increment { + let num_good = num_good_so_far.get_unchecked_mut(cid); + *num_good = num_good.saturating_add(1); + } + + for &cid in clauses_to_decrement { + let num_good = num_good_so_far.get_unchecked_mut(cid); + let new_val = num_good.saturating_sub(1); + *num_good = new_val; + if new_val == 0 && !*in_queue.get_unchecked(cid) { + *in_queue.get_unchecked_mut(cid) = true; + residual_.push(cid); + } + } + + *variables.get_unchecked_mut(v) = !was_true; + } else { + break; + } + rounds += 1; + } + } + for v in 0..num_variables { + if p_single[v] { + variables[v] = true; + } else if n_single[v] { + variables[v] = false; + } + } + save_solution(&Solution { variables })?; + return Ok(()); +} + +pub fn help() { + println!("No help information available."); +}