new function count_sat_in

more efficient version of test/queen.ml

CHANGES

@@ -1,3 +1,6 @@
+
+ o new function `count_sat_int`
+
 November 13, 2018 (VERSION 0.4)
 -------------------------------
  o no more set_max_var -> a functor Make and a function 'make' instead

lib/bdd.ml

@@ -52,6 +52,7 @@ module type BDD = sig
   val build : formula -> t
   val is_sat : t -> bool
   val tautology : t -> bool
+  val count_sat_int : t -> int
   val count_sat : t -> Int64.t
   val any_sat : t -> (variable * bool) list
   val random_sat : t -> (variable * bool) list
@@ -526,6 +527,25 @@ let rec int64_two_to = function
       let r2 = Int64.mul r r in
       if n mod 2 == 0 then r2 else Int64.mul (Int64.of_int 2) r2
 
+let count_sat_int b =
+  let cache = H1.create cache_default_size in
+  let rec count b =
+    try
+      H1.find cache b
+    with Not_found ->
+      let n = match b.node with
+	| Zero -> 0
+	| One -> 1
+	| Node (v, l, h) ->
+	    let dvl = var l - v - 1 in
+	    let dvh = var h - v - 1 in
+	    (1 lsl dvl) * count l + (1 lsl dvh) * count h
+      in
+      H1.add cache b n;
+      n
+  in
+  (1 lsl (var b - 1)) * count b
+
 let count_sat b =
   let cache = H1.create cache_default_size in
   let rec count b =

lib/bdd.mli

@@ -133,6 +133,7 @@ module type BDD = sig
   val tautology : t -> bool
     (** Checks if a bdd is a tautology i.e. equal to [one] *)
 
+  val count_sat_int : t -> int
   val count_sat : t -> Int64.t
     (** Counts the number of different ways to satisfy a bdd. *)
 

test/queen.ml

@@ -21,7 +21,7 @@ let n = match int_of_string Sys.argv.(1) with
   | n when n <= 0 -> failwith "size should be greater than 0"
   | n -> n
 
-include (val Bdd.make (n * n))
+include (val Bdd.make ~size:60000 (n * n))
 
 let fold_and i j f =
   let rec mk k = if k > j then one else mk_and (f k) (mk (k+1)) in
@@ -35,44 +35,43 @@ let fold_for i j f =
   let rec fold k acc = if k > j then acc else fold (k+1) (f k acc) in
   fold i
 
+let fold_for_rev i j f =
+  let rec fold k acc = if k < j then acc else fold (k-1) (f k acc) in
+  fold i
+
 (* 0..n-1 x 0..n-1 -> 1..n x n *)
 let vars =
   Array.init n (fun i -> Array.init n (fun j -> mk_var (1 + n * i + j)))
 let var i j = vars.(i).(j)
 
-let constraints i j =
-  let b1 =
-    fold_and 0 (n-1)
-      (fun l -> if l = j then one else mk_not (var i l))
-  in
-  let b2 =
-    fold_and 0 (n-1)
-      (fun k -> if k = i then one else mk_not (var k j))
-  in
-  let b3 =
-    fold_and 0 (n-1)
-      (fun k ->
-	 let ll = j+k-i in
-	 if ll >= 0 && ll < n && k <> i then mk_not (var k ll) else one)
-  in
-  let b4 =
-    fold_and 0 (n-1)
-      (fun k ->
-	 let ll = j+i-k in
-	 if ll >= 0 && ll < n && k <> i then mk_not (var k ll) else one)
-  in
-  mk_and b1 (mk_and b2 (mk_and b3 b4))
-
+let queens_s i j =
+  let var i j = mk_var (1 + i * n + j) in
+  fold_for_rev (n-1) 0 (fun row bdd ->
+      if i = row then
+        fold_for_rev (n-1) 0 (fun col bdd ->
+            if j = col then
+              mk_and bdd (var row col)
+            else
+              mk_and bdd (mk_not (var row col))
+          ) bdd
+      else
+        let d = abs (i - row) in
+        let bdd = if j + d < n then
+                    mk_and bdd (mk_not (var row (j + d))) else bdd in
+        let bdd = mk_and bdd (mk_not (var row j)) in
+        if d <= j then
+          mk_and bdd (mk_not (var row (j - d))) else bdd
+    ) one
+let queens_r i =
+  fold_for 0 (n-1) (fun j bdd -> mk_or bdd (queens_s i j)) zero
 let bdd =
-  fold_and 0 (n-1) (fun i -> fold_or 0 (n-1) (fun j -> var i j))
+  fold_for 0 (n-1) (fun i bdd -> mk_and bdd (queens_r i)) one
 
-let bdd =
-  fold_for 0 (n-1)
-    (fun i acc ->
-       fold_for 0 (n-1)
-	 (fun j acc ->
-	    mk_and acc (mk_imp (var i j) (constraints i j)))
-	 acc)
-    bdd
+let () = printf "There are %d solutions@." (count_sat_int bdd)
 
-let () = printf "There are %Ld solutions@." (count_sat bdd)
+let () = exit 0
+let () =
+  let print v (tl, e, sum, smallest, median, biggest) =
+    printf "v=%d: size=%d #entries=%d sum=%d small/med/big=%d/%d/%d@."
+      v tl e sum smallest median biggest in
+  Array.iteri print (stats ())