mirror of
https://github.com/tig-foundation/tig-monorepo.git
synced 2026-02-21 10:27:49 +08:00
Submitted satisfiability/inbound
This commit is contained in:
FiveMovesAhead
parent
bdc6ed6794
commit
17b51df05a
23
tig-algorithms/src/satisfiability/inbound/README.md
Normal file
23
tig-algorithms/src/satisfiability/inbound/README.md
Normal file
@ -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
|
||||
241
tig-algorithms/src/satisfiability/inbound/mod.rs
Normal file
241
tig-algorithms/src/satisfiability/inbound/mod.rs
Normal file
@ -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<Map<String, Value>>,
|
||||
) -> 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<i32>> = Vec::with_capacity(clauses_.len());
|
||||
|
||||
let mut dead = false;
|
||||
|
||||
while !(dead) {
|
||||
let mut done = true;
|
||||
for c in &clauses_ {
|
||||
let mut c_: Vec<i32> = 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<usize>> = vec![vec![]; num_variables];
|
||||
let mut n_clauses: Vec<Vec<usize>> = 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<usize> = 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.");
|
||||
}
|
||||
@ -32,7 +32,8 @@
|
||||
|
||||
// c001_a017
|
||||
|
||||
// c001_a018
|
||||
pub mod inbound;
|
||||
pub use inbound as c001_a018;
|
||||
|
||||
// c001_a019
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user