Change sudoku sat and minor performance improvements

src/bin/gen_sudoku.rs

@@ -1,24 +1,14 @@
 fn main() {
-    // exactly one for each position
+    // at most one at each position
     for x in 1..=9 {
         for y in 1..=9 {
             for i in 1..=9 {
-                print!("(");
                 for j in 1..=9 {
-                    if i != j {
-                        print!("!")
+                    if i < j {
+                        println!("!(s{x}{y}{j}&s{x}{y}{i})");
                     }
-                    print!("s{x}{y}{j}");
-                    if j != 9 {
-                        print!("&")
-                    }
-                }
-                print!(")");
-                if i != 9 {
-                    print!("|")
                 }
             }
-            println!()
         }
     }
 
@@ -64,4 +54,30 @@ fn main() {
             }
         }
     }
+
+    // set fields
+    println!("s119");
+    println!("s148");
+    println!("s193");
+    println!("s238");
+    println!("s267");
+    println!("s282");
+    println!("s322");
+    println!("s359");
+    println!("s386");
+    println!("s424");
+    println!("s491");
+    println!("s536");
+    println!("s574");
+    println!("s611");
+    println!("s672");
+    println!("s729");
+    println!("s754");
+    println!("s785");
+    println!("s833");
+    println!("s842");
+    println!("s877");
+    println!("s911");
+    println!("s963");
+    println!("s998");
 }

src/dpll_normal_form.rs

@@ -1,4 +1,6 @@
-use std::collections::HashSet;
+use std::{
+    borrow::BorrowMut, cell::RefCell, collections::HashSet, ops::DerefMut, sync::RwLockWriteGuard,
+};
 
 use crate::{dpll::Index, normal_form::NormalForm};
 
@@ -11,8 +13,14 @@ fn unit_propagate(cnf: &mut NormalForm, solution: &mut Vec<Index>) {
     }
 }
 
+thread_local! {
+    static LITERALS: RefCell<HashSet<Index>> = RefCell::new(HashSet::new());
+}
+
 fn pure_literal_assign(cnf: &mut NormalForm, solution: &mut Vec<Index>) {
-    let mut literals: HashSet<Index> = HashSet::new();
+    let mut literals = LITERALS.take();
+    literals.clear();
+
     for (s, _, _) in cnf.iter() {
         literals.extend(s.iter());
     }
@@ -23,6 +31,8 @@ fn pure_literal_assign(cnf: &mut NormalForm, solution: &mut Vec<Index>) {
             cnf.remove_literal(l);
         }
     }
+
+    LITERALS.set(literals);
 }
 
 pub fn dpll(cnf: &NormalForm, solution: &mut Vec<Index>) -> bool {
@@ -30,6 +40,16 @@ pub fn dpll(cnf: &NormalForm, solution: &mut Vec<Index>) -> bool {
     let mut own_cnf = cnf.to_owned();
 
     unit_propagate(&mut own_cnf, solution);
+
+    if own_cnf.is_empty() {
+        return true;
+    }
+
+    if own_cnf.empty_clauses() {
+        solution.truncate(prev_solution);
+        return false;
+    }
+
     pure_literal_assign(&mut own_cnf, solution);
 
     if own_cnf.is_empty() {

src/main.rs

@@ -36,7 +36,10 @@ fn main() -> Result<()> {
     cnf.stats();
 
     let mut solution = Vec::new();
+    let start = std::time::Instant::now();
     dbg!(crate::dpll_normal_form::dpll(&cnf, &mut solution));
+    let elapsed = start.elapsed();
+    println!("Time dpll: {elapsed:?}");
 
     // dbg!(&solution);
     // dbg!(e.clone().conjunctiveNormalForm());
@@ -55,13 +58,19 @@ fn main() -> Result<()> {
     // let inv_map: HashMap<_, _> = map.into_iter().map(|(k, v)| (v, k)).collect();
 
     // dbg!(&solution);
+
+    let mut s = Vec::new();
     for i in solution {
         if i > 0 {
-            println!("{}: true", map.backward(i));
+            s.push((map.backward(i), true));
         } else {
-            println!("{}: false", map.backward(i.abs()));
+            s.push((map.backward(i.abs()), false));
         }
     }
+    s.sort();
+    for (s, b) in s {
+        println!("{s}: {b}");
+    }
 
     // let mut nf = NormalForm::from_slices(&cnf);
     // dbg!(&nf);