From 361c4a9d44c9b413dd6f9a1a87a5cb8c3a929344 Mon Sep 17 00:00:00 2001 From: shujinarazaki Date: Sat, 16 Jan 2021 13:29:27 +0900 Subject: [PATCH] src/sudoku.rs: inject preset before making rulse new file: .shell modified: src/bin/sudoku25.rs modified: src/bin/sudoku400.rs modified: src/bin/sudoku64.rs modified: src/sudoku.rs --- .shell | 1 + src/bin/sudoku25.rs | 12 ++++--- src/bin/sudoku400.rs | 19 ++++++----- src/bin/sudoku64.rs | 14 ++++---- src/sudoku.rs | 79 ++++++++++++++++++++++++++++++++++++++------ 5 files changed, 96 insertions(+), 29 deletions(-) create mode 100644 .shell diff --git a/.shell b/.shell new file mode 100644 index 0000000..1f64d01 --- /dev/null +++ b/.shell @@ -0,0 +1 @@ +cargo run --bin sudoku400 --release < hn_singles400x400.txt diff --git a/src/bin/sudoku25.rs b/src/bin/sudoku25.rs index aef009d..44b8db1 100644 --- a/src/bin/sudoku25.rs +++ b/src/bin/sudoku25.rs @@ -8,12 +8,14 @@ pub fn main() { let range = 25; set_range(range); let mut rules: Rules = Vec::new(); - rules.append(&mut sudoku_ident()); + let conf: Vec<(Pos, usize)> = parse_s25(); + rules.append(&mut sudoku_ident(&conf)); rules.append(&mut sudoku_ident2()); - rules.append(&mut sudoku_row()); - rules.append(&mut sudoku_column()); - rules.append(&mut sudoku_block()); - let setting: Vec = parse_s25() + rules.append(&mut sudoku_row(&conf)); + rules.append(&mut sudoku_column(&conf)); + rules.append(&mut sudoku_block(&conf)); + rules.append(&mut sudoku_preset(&conf)); + let setting: Vec = conf .iter() .map(|(p, d)| p.state(*d, true).as_lit()) .collect::>(); diff --git a/src/bin/sudoku400.rs b/src/bin/sudoku400.rs index fdc9407..2eb909d 100644 --- a/src/bin/sudoku400.rs +++ b/src/bin/sudoku400.rs @@ -7,16 +7,18 @@ use { pub fn main() { let range = 400; set_range(range); - let setting: Vec = parse(20) + let constraints: Vec<(Pos, usize)> = parse(20); + let setting: Vec = constraints .iter() .map(|(p, d)| p.state(*d, true).as_lit()) .collect::>(); + dbg!(constraints.len()); let mut rules: Rules = Vec::new(); - rules.append(&mut sudoku_ident()); - rules.append(&mut sudoku_ident2()); - rules.append(&mut sudoku_row()); - rules.append(&mut sudoku_column()); - rules.append(&mut sudoku_block()); + rules.append(&mut sudoku_ident(&constraints)); + // rules.append(&mut sudoku_ident2()); + // rules.append(&mut sudoku_row(&constraints)); + // rules.append(&mut sudoku_column(&constraints)); + // rules.append(&mut sudoku_block(&constraints)); let mut file = File::create("sudoku400.cnf").expect("fail to create 'sudoku400.cnf'"); file.write_all(&miracle_sudoku::cnf::as_cnf_u8(&rules, &setting)) .expect("fail to write 'sudoku400.cnf'"); @@ -47,7 +49,9 @@ pub fn main() { fn parse(tick: usize) -> Vec<(Pos, usize)> { let mut buf = String::new(); - std::io::stdin().read_to_string(&mut buf).expect("fail to read"); + std::io::stdin() + .read_to_string(&mut buf) + .expect("fail to read"); let mut vec: Vec<(Pos, usize)> = Vec::new(); let mut i = 0; for (ii, l) in buf.lines().enumerate() { @@ -69,7 +73,6 @@ fn parse(tick: usize) -> Vec<(Pos, usize)> { } else { dbg!(w); } - } } } diff --git a/src/bin/sudoku64.rs b/src/bin/sudoku64.rs index b932731..64e4be2 100644 --- a/src/bin/sudoku64.rs +++ b/src/bin/sudoku64.rs @@ -9,19 +9,20 @@ pub fn main() { set_range(64); assert_eq!(get_range(), range); let mut rules: Rules = Vec::new(); - rules.append(&mut sudoku_ident()); + let (conf, mut dic) = parse_sudoku(); + rules.append(&mut sudoku_ident(&conf)); rules.append(&mut sudoku_ident2()); - rules.append(&mut sudoku_row()); - rules.append(&mut sudoku_column()); - rules.append(&mut sudoku_block()); + rules.append(&mut sudoku_row(&conf)); + rules.append(&mut sudoku_column(&conf)); + rules.append(&mut sudoku_block(&conf)); + rules.append(&mut sudoku_preset(&conf)); // csv_sudoku(); - let (conf, mut dic) = parse_sudoku(); let setting: Vec = conf .iter() .map(|(p, d)| p.state(*d, true).as_lit()) .collect::>(); let mut file = File::create("sudoku64.cnf").expect("fail to create 'sudoku64.cnf'"); - file.write_all(&miracle_sudoku::cnf::as_cnf_u8(&rules, &setting)) + file.write_all(&miracle_sudoku::cnf::as_cnf_u8(&rules, &vec![])) .expect("fail to write 'sudoku64.cnf'"); println!("#rules: {}", rules.len()); let mut config = Config::default(); @@ -176,6 +177,7 @@ fn parse_sudoku() -> (Vec<(Pos, usize)>, HashMap) { (vec, pull_back) } +#[allow(dead_code)] fn csv_sudoku() { for l in SUDOKU.lines() { for c in l.chars() { diff --git a/src/sudoku.rs b/src/sudoku.rs index 77821bd..f586dc8 100644 --- a/src/sudoku.rs +++ b/src/sudoku.rs @@ -1,20 +1,51 @@ use crate::{get_range, pos::*, Rules}; +fn collect_digits(fixed: &[(Pos, usize)], p: Pos) -> Vec { + if fixed.iter().find(|r| p == r.0).is_some() { + fixed + .iter() + .filter(|(q, _)| *q != p && (p.i == q.i || p.j == q.j)) + .map(|r| r.1) + .collect::>() + } else { + vec![] + } +} + +pub fn sudoku_preset(fixed: &[(Pos, usize)]) -> Rules { + let range = get_range(); + let mut rules = Vec::new(); + for (p, d) in fixed.iter() { + for dd in 1..=range as usize { + rules.push(vec![p.state(dd, *d == dd).as_lit()]); + } + } + rules +} + /// 1. At least one number sholud be assigned on each cell. /// 2. So a positive assginment should be a trigger to assgin the rest vars negatively. -pub fn sudoku_ident() -> Rules { +/// O(n^4) +pub fn sudoku_ident(fixed: &[(Pos, usize)]) -> Rules { let range = get_range(); let mut rules = Vec::new(); for i in 1..=range { for j in 1..=range { let p = Pos::at(i, j); + if fixed.iter().any(|r| p == r.0) { + continue; + } // at-least constraints let v = (1..=(range as usize)) .map(|d| p.state(d, true).as_lit()) .collect::>(); rules.push(v); // at-most constraints + let presets = collect_digits(fixed, p); for d in 1..=(range as usize) { + if presets.contains(&d) { + continue; + } for dd in 1..(range as usize) { if d != dd { rules.push(p.state(d, true).requires(p.state(dd, false))); @@ -27,6 +58,7 @@ pub fn sudoku_ident() -> Rules { } /// 1. At least each number should be assigned on each group once. +/// O(n^2) pub fn sudoku_ident2() -> Rules { let range = get_range(); let mut rules = Vec::new(); @@ -76,7 +108,8 @@ pub fn sudoku_ident2() -> Rules { } /// 1. In Each row, each number should be assgined at most once. -pub fn sudoku_row() -> Rules { +/// O(n^4) +pub fn sudoku_row(fixed: &[(Pos, usize)]) -> Rules { let range = get_range(); let mut rules = Vec::new(); for i in 1..=range { @@ -84,8 +117,16 @@ pub fn sudoku_row() -> Rules { let p = Pos::at(i, j); for jj in j + 1..=range { let q = Pos::at(i, jj); - for d in 1..=(range as usize) { - rules.push(p.state(d, true).requires(q.state(d, false))); + if fixed.iter().any(|r| p == r.0) && fixed.iter().any(|r| q == r.0) { + continue; + } else if let Some((_, d)) = fixed.iter().find(|r| p == r.0) { + rules.push(vec![q.state(*d, false).as_lit()]); + } else if let Some((_, d)) = fixed.iter().find(|r| q == r.0) { + rules.push(vec![p.state(*d, false).as_lit()]); + } else { + for d in 1..=(range as usize) { + rules.push(p.state(d, true).requires(q.state(d, false))); + } } } } @@ -94,7 +135,8 @@ pub fn sudoku_row() -> Rules { } /// 1. In Each column, each number should be assgined at most once. -pub fn sudoku_column() -> Rules { +/// O(n^4) +pub fn sudoku_column(fixed: &[(Pos, usize)]) -> Rules { let range = get_range(); let mut rules = Vec::new(); for j in 1..=range { @@ -102,8 +144,16 @@ pub fn sudoku_column() -> Rules { let p = Pos::at(i, j); for ii in i + 1..=range { let q = Pos::at(ii, j); - for d in 1..=(range as usize) { - rules.push(p.state(d, true).requires(q.state(d, false))); + if fixed.iter().any(|r| p == r.0) && fixed.iter().any(|r| q == r.0) { + continue; + } else if let Some((_, d)) = fixed.iter().find(|r| p == r.0) { + rules.push(vec![q.state(*d, false).as_lit()]); + } else if let Some((_, d)) = fixed.iter().find(|r| q == r.0) { + rules.push(vec![p.state(*d, false).as_lit()]); + } else { + for d in 1..=(range as usize) { + rules.push(p.state(d, true).requires(q.state(d, false))); + } } } } @@ -112,7 +162,8 @@ pub fn sudoku_column() -> Rules { } /// 1. In Each square block, each number should be assgined at most once. -pub fn sudoku_block() -> Rules { +/// O(n^4) +pub fn sudoku_block(fixed: &[(Pos, usize)]) -> Rules { let range = get_range(); let bsize = (range as f64).sqrt() as isize; let mut rules = Vec::new(); @@ -129,8 +180,16 @@ pub fn sudoku_block() -> Rules { if let Some(p) = (base + block_walk[tail]).valid(range) { for offset in &block_walk[tail + 1..] { if let Some(q) = (base + *offset).valid(range) { - for d in 1..=(range as usize) { - rules.push(p.state(d, true).requires(q.state(d, false))); + if fixed.iter().any(|r| p == r.0) && fixed.iter().any(|r| q == r.0) { + continue; + } else if let Some((_, d)) = fixed.iter().find(|r| p == r.0) { + rules.push(vec![q.state(*d, false).as_lit()]); + } else if let Some((_, d)) = fixed.iter().find(|r| q == r.0) { + rules.push(vec![p.state(*d, false).as_lit()]); + } else { + for d in 1..=(range as usize) { + rules.push(p.state(d, true).requires(q.state(d, false))); + } } } }