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

@@ -0,0 +1 @@
+cargo run --bin sudoku400 --release < hn_singles400x400.txt

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<i32> = 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<i32> = conf
         .iter()
         .map(|(p, d)| p.state(*d, true).as_lit())
         .collect::<Vec<_>>();

src/bin/sudoku400.rs

@@ -7,16 +7,18 @@ use {
 pub fn main() {
     let range = 400;
     set_range(range);
-    let setting: Vec<i32> = parse(20)
+    let constraints: Vec<(Pos, usize)> = parse(20);
+    let setting: Vec<i32> = constraints
         .iter()
         .map(|(p, d)| p.state(*d, true).as_lit())
         .collect::<Vec<_>>();
+    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);
                     }
-
                 }
             }
         }

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<i32> = conf
         .iter()
         .map(|(p, d)| p.state(*d, true).as_lit())
         .collect::<Vec<_>>();
     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<usize, char>) {
     (vec, pull_back)
 }
 
+#[allow(dead_code)]
 fn csv_sudoku() {
     for l in SUDOKU.lines() {
         for c in l.chars() {

src/sudoku.rs

@@ -1,20 +1,51 @@
 use crate::{get_range, pos::*, Rules};
 
+fn collect_digits(fixed: &[(Pos, usize)], p: Pos) -> Vec<usize> {
+    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::<Vec<usize>>()
+    } 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::<Vec<_>>();
             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,16 +108,25 @@ 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 {
         for j in 1..=range {
             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,16 +135,25 @@ 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 {
         for i in 1..=range {
             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)));
+                                }
                             }
                         }
                     }