From 60fc6b2f742f46e2f52431435e7993c751de7e7f Mon Sep 17 00:00:00 2001
From: Josh Berdine <josh@berdine.net>
Date: Sun, 26 Jan 2025 12:09:57 +0000
Subject: [PATCH] Add ZDD-based N-queens solver benchmark

This PR adds a benchmark that solves the N-queens problem using ZDDs. The
ZDD data structure code is based on the existing ZDD benchmark. The
motivation for this benchmark is that its performance benefits greatly from
the memoization of the ZDD operations, while the existing benchmark is
faster without memoization. In this sense, this benchmark is more
representative of actual use cases where the sharing introduced and enforced
by hash-consing is used to share subcomputations using memoization to give
polynomial-time algorithms that would be exponential-time without
sharing. (Although note that some ZDD operations are polynomial time with
sharing, others still have worst-case exponential time even if in practice
they are often fast.) Additionally, this benchmark shows Ephemeron-based
caching outperforming (simplistic) Hashtbl-based caching.

Signed-off-by: Josh Berdine <josh@berdine.net>
---
 benchmarks/zdd/dune          |   6 +-
 benchmarks/zdd/zdd_queens.ml | 877 +++++++++++++++++++++++++++++++++++
 run_config.json              |  13 +
 3 files changed, 895 insertions(+), 1 deletion(-)
 create mode 100644 benchmarks/zdd/zdd_queens.ml

diff --git a/benchmarks/zdd/dune b/benchmarks/zdd/dune
index c574511a2..6ac1c5a2d 100644
--- a/benchmarks/zdd/dune
+++ b/benchmarks/zdd/dune
@@ -2,4 +2,8 @@
  (name zdd)
  (modes native))
 
-(alias (name buildbench) (deps zdd.exe words.txt))
+(executable
+ (name zdd_queens)
+ (modes native))
+
+(alias (name buildbench) (deps zdd.exe words.txt zdd_queens.exe))
diff --git a/benchmarks/zdd/zdd_queens.ml b/benchmarks/zdd/zdd_queens.ml
new file mode 100644
index 000000000..7f308c956
--- /dev/null
+++ b/benchmarks/zdd/zdd_queens.ml
@@ -0,0 +1,877 @@
+(** A simple implementation of ZDDs (Reduced Ordered Zero-Suppressed Binary
+    Decision Diagrams).
+
+    Josh Berdine, based on:
+
+    Shin-ichi Minato: Zero-Suppressed BDDs for Set Manipulation in
+    Combinatorial Problems. DAC 1993: 272-277
+
+    Shin-ichi Minato: Calculation of Unate Cube Set Algebra Using
+    Zero-Suppressed BDDs. DAC 1994: 420–424
+
+    Donald Ervin Knuth: The Art of Computer Programming. Volume 4a
+    Combinatorial Algorithms Part 1. Addison-Wesley 2011. *)
+
+include struct
+  [@@@warning "-unused-value-declaration"]
+
+  external ( = ) : int -> int -> bool = "%equal"
+  external ( <> ) : int -> int -> bool = "%notequal"
+  external ( < ) : int -> int -> bool = "%lessthan"
+  external ( > ) : int -> int -> bool = "%greaterthan"
+  external ( <= ) : int -> int -> bool = "%lessequal"
+  external ( >= ) : int -> int -> bool = "%greaterequal"
+  external compare : int -> int -> int = "%compare"
+  external equal : int -> int -> bool = "%equal"
+
+  let min x y = if x <= y then x else y
+  let max x y = if x >= y then x else y
+end
+
+let memo_hc =
+  match Sys.getenv_opt "MEMO_HC" with
+  | None -> 2
+  | Some s -> (
+    match int_of_string s with
+    | (0 | 1 | 2) as n -> n
+    | _ | (exception Failure _) -> invalid_arg ("invalid MEMO_HC: " ^ s) )
+
+let memo_op =
+  match Sys.getenv_opt "MEMO_OP" with
+  | None -> 2
+  | Some s -> (
+    match int_of_string s with
+    | (0 | 1 | 2) as n -> n
+    | _ | (exception Failure _) -> invalid_arg ("invalid MEMO_OP: " ^ s) )
+
+let memo_scale =
+  match Sys.getenv_opt "MEMO_SCALE" with
+  | None -> 1
+  | Some s -> (
+    try int_of_string s
+    with Failure _ -> invalid_arg ("invalid MEMO_SCALE: " ^ s) )
+
+let scale size = size * memo_scale
+
+(*
+ * Core ZDD representation
+ *)
+
+type order = LT | EQ | GT
+
+module Elt = struct
+  type t = int * int
+
+  let compare (c, r) (d, s) =
+    match Int.compare c d with 0 -> Int.compare r s | n -> n
+
+  let order x y =
+    let i = compare x y in
+    if i < 0 then LT else if i = 0 then EQ else GT
+
+  let ( < ) x y = compare x y < 0
+  let equal (c, r) (d, s) = Int.equal c d && Int.equal r s
+  let hash = Hashtbl.hash
+end
+
+module T = struct
+  type t =
+    | Empty  (** the empty family: ∅ *)
+    | Unit  (** the unit family: {∅} *)
+    | Ite of {v: Elt.t; t: t; e: t; hash: int}
+        (** a decision: {{v} ∪ p | p ∈ t} ∪ e, aka v⊔t ∪ e *)
+
+  let equal : t -> t -> bool = if memo_hc = 0 then Stdlib.( = ) else ( == )
+  let ( == ) = equal
+
+  let hash = function
+    | Empty -> Hashtbl.hash 0
+    | Unit -> Hashtbl.hash 1
+    | Ite {hash; _} -> hash
+end
+
+include T
+
+module H = struct
+  type t = T.t
+
+  let equal p0 q0 =
+    match (p0, q0) with
+    | Ite p, Ite q -> p.e == q.e && p.t == q.t && Elt.equal p.v q.v
+    | _ -> p0 == q0
+
+  let hash = T.hash
+end
+
+(*
+ * Inline fragment of Weak.Make so same code is used across OCaml versions
+ *)
+
+(* module WeakSet = Weak.Make (H) *)
+
+module WeakSet : sig
+  type data = H.t
+  type t
+
+  val create : int -> t
+  val merge : t -> data -> data
+  val stats : t -> int * int * int * int * int * int
+end = struct
+  open Weak
+
+  let additional_values = 2 (* CAML_EPHE_FIRST_KEY in weak.h *)
+
+  type 'a weak_t = 'a t
+
+  let weak_create = create
+  let emptybucket = weak_create 0
+
+  type data = H.t
+
+  type t =
+    { mutable table: data weak_t array
+    ; mutable hashes: int array array
+    ; mutable limit: int (* bucket size limit *)
+    ; mutable oversize: int (* number of oversize buckets *)
+    ; mutable rover: int (* for internal bookkeeping *) }
+
+  let get_index t h = h land max_int mod Array.length t.table
+  let limit = 7
+  let over_limit = 2
+
+  let create sz =
+    let sz = if sz < 7 then 7 else sz in
+    let sz =
+      if sz > Sys.max_array_length then Sys.max_array_length else sz
+    in
+    { table= Array.make sz emptybucket
+    ; hashes= Array.make sz [||]
+    ; limit
+    ; oversize= 0
+    ; rover= 0 }
+
+  let iter_weak f t =
+    let rec iter_bucket i j b =
+      if i >= length b then ()
+      else
+        match check b i with
+        | true ->
+            f b t.hashes.(j) i ;
+            iter_bucket (i + 1) j b
+        | false -> iter_bucket (i + 1) j b
+    in
+    Array.iteri (iter_bucket 0) t.table
+
+  let rec count_bucket i b accu =
+    if i >= length b then accu
+    else count_bucket (i + 1) b (accu + if check b i then 1 else 0)
+
+  let count t = Array.fold_right (count_bucket 0) t.table 0
+  let next_sz n = min ((3 * n / 2) + 3) Sys.max_array_length
+  let prev_sz n = (((n - 3) * 2) + 2) / 3
+
+  let test_shrink_bucket t =
+    let bucket = t.table.(t.rover) in
+    let hbucket = t.hashes.(t.rover) in
+    let len = length bucket in
+    let prev_len = prev_sz len in
+    let live = count_bucket 0 bucket 0 in
+    if live <= prev_len then (
+      let rec loop i j =
+        if j >= prev_len then
+          if check bucket i then loop (i + 1) j
+          else if check bucket j then (
+            blit bucket j bucket i 1 ;
+            hbucket.(i) <- hbucket.(j) ;
+            loop (i + 1) (j - 1) )
+          else loop i (j - 1)
+      in
+      loop 0 (length bucket - 1) ;
+      ( if prev_len = 0 then (
+        t.table.(t.rover) <- emptybucket ;
+        t.hashes.(t.rover) <- [||] )
+      else
+        let newbucket = weak_create prev_len in
+        blit bucket 0 newbucket 0 prev_len ;
+        t.table.(t.rover) <- newbucket ;
+        t.hashes.(t.rover) <- Array.sub hbucket 0 prev_len ) ;
+      if len > t.limit && prev_len <= t.limit then
+        t.oversize <- t.oversize - 1 ) ;
+    t.rover <- (t.rover + 1) mod Array.length t.table
+
+  let rec resize t =
+    let oldlen = Array.length t.table in
+    let newlen = next_sz oldlen in
+    if newlen > oldlen then (
+      let newt = create newlen in
+      let add_weak ob oh oi =
+        let setter nb ni _ = blit ob oi nb ni 1 in
+        let h = oh.(oi) in
+        add_aux newt setter None h (get_index newt h)
+      in
+      iter_weak add_weak t ;
+      t.table <- newt.table ;
+      t.hashes <- newt.hashes ;
+      t.limit <- newt.limit ;
+      t.oversize <- newt.oversize ;
+      t.rover <- t.rover mod Array.length newt.table )
+    else (
+      t.limit <- max_int ;
+      (* maximum size already reached *)
+      t.oversize <- 0 )
+
+  and add_aux t setter d h index =
+    let bucket = t.table.(index) in
+    let hashes = t.hashes.(index) in
+    let sz = length bucket in
+    let i = ref 0 in
+    while !i < sz && check bucket !i do
+      incr i
+    done ;
+    if !i < sz then (
+      setter bucket !i d ;
+      hashes.(!i) <- h )
+    else
+      let newsz =
+        min ((3 * sz / 2) + 3) (Sys.max_array_length - additional_values)
+      in
+      if newsz <= sz then failwith "Weak.Make: hash bucket cannot grow more" ;
+      let newbucket = weak_create newsz in
+      let newhashes = Array.make newsz 0 in
+      blit bucket 0 newbucket 0 sz ;
+      Array.blit hashes 0 newhashes 0 sz ;
+      setter newbucket sz d ;
+      newhashes.(sz) <- h ;
+      t.table.(index) <- newbucket ;
+      t.hashes.(index) <- newhashes ;
+      if sz <= t.limit && newsz > t.limit then (
+        t.oversize <- t.oversize + 1 ;
+        for _i = 0 to over_limit do
+          test_shrink_bucket t
+        done ) ;
+      if t.oversize > Array.length t.table / over_limit then resize t
+
+  (* General auxiliary function for searching for a particular value
+   * in a hash-set, and acting according to whether or not it's found *)
+
+  let find_aux t d k_found k_notfound =
+    let h = H.hash d in
+    let index = get_index t h in
+    let bucket = t.table.(index) in
+    let hashes = t.hashes.(index) in
+    let sz = length bucket in
+    let found = ref None in
+    let i = ref 0 in
+    while !i < sz && Option.is_none !found do
+      if h = hashes.(!i) then
+        match get bucket !i with
+        | Some v as opt -> if H.equal v d then found := opt else incr i
+        | _ -> incr i
+      else incr i
+    done ;
+    match !found with
+    | Some v as opt -> k_found bucket !i opt v
+    | None -> k_notfound h index
+
+  let merge t d =
+    find_aux t d
+      (fun _b _i _o v -> v)
+      (fun h i ->
+        add_aux t set (Some d) h i ;
+        d )
+
+  let stats t =
+    let len = Array.length t.table in
+    let lens = Array.map length t.table in
+    Array.sort compare lens ;
+    let totlen = Array.fold_left ( + ) 0 lens in
+    (len, count t, totlen, lens.(0), lens.(len / 2), lens.(len - 1))
+end
+
+(*
+ * Unique table
+ *)
+
+let hashtbl_stats stats =
+  let Hashtbl.
+        { num_bindings= num
+        ; num_buckets= len
+        ; max_bucket_length= max_len
+        ; bucket_histogram= histo } =
+    stats
+  in
+  let sum_len = ref 0 in
+  let min_len = ref 0 in
+  let med_len = ref 0 in
+  for i = 0 to max_len do
+    if !min_len = 0 && histo.(i) > 0 then min_len := i ;
+    sum_len := !sum_len + histo.(i) ;
+    if !med_len = 0 && !sum_len >= num / 2 then med_len := i
+  done ;
+  (len, num, !sum_len, !min_len, !med_len, max_len)
+
+let print_stats label (len, num, sum, min, med, max) =
+  if num > 0 then
+    Format.eprintf
+      "%s length: %i entries: %i bucket lengths: sum: %i min: %i median: \
+       %i max: %i@\n"
+      label len num sum min med max
+
+module type Unique = sig
+  type t
+
+  val create : int -> string -> t
+  val merge : t -> T.t -> T.t
+end
+
+module NoUnique : Unique = struct
+  type t = unit
+
+  let create _ _ = ()
+  let merge () p = p
+end
+
+module HashUnique : Unique = struct
+  module Tbl = Hashtbl.Make (H)
+
+  type t = T.t Tbl.t
+
+  let create size label =
+    let tbl = Tbl.create (scale size) in
+    at_exit (fun () -> print_stats label (hashtbl_stats (Tbl.stats tbl))) ;
+    tbl
+
+  let merge tbl elt =
+    match Tbl.find_opt tbl elt with
+    | Some elt -> elt
+    | None ->
+        Tbl.add tbl elt elt ;
+        elt
+end
+
+module WeakUnique : Unique = struct
+  include WeakSet
+
+  let create size label =
+    let tbl = create (scale size) in
+    at_exit (fun () -> print_stats label (stats tbl)) ;
+    tbl
+end
+
+let unique : (module Unique) =
+  match memo_hc with
+  | 0 -> (module NoUnique)
+  | 1 -> (module HashUnique)
+  | 2 -> (module WeakUnique)
+  | _ -> assert false
+
+module Unique = (val unique)
+
+let unique_set = Unique.create 2048 "unique set"
+
+let unique v ~t ~e =
+  if t == Empty then e
+  else
+    let hash = Hashtbl.hash (2, Elt.hash v, T.hash e, T.hash t) in
+    let node = Ite {v; t; e; hash} in
+    Unique.merge unique_set node
+
+(*
+ * Memoization tables for operations
+ *)
+
+module type MemoT = sig
+  type 'a t
+
+  val create : int -> string -> 'a t
+  val find_or_add : 'a t -> T.t -> (T.t -> 'a) -> 'a
+end
+
+module NoMemoT : MemoT = struct
+  type 'a t = unit
+
+  let create _ _ = ()
+  let find_or_add () p k = k p
+end
+
+module HashMemoT : MemoT = struct
+  module Tbl = Hashtbl.Make (T)
+
+  type 'a t = 'a Tbl.t
+
+  let create size label =
+    let tbl = Tbl.create (scale size) in
+    at_exit (fun () -> print_stats label (hashtbl_stats (Tbl.stats tbl))) ;
+    tbl
+
+  let find_or_add tbl p k =
+    match Tbl.find_opt tbl p with
+    | Some r -> r
+    | None ->
+        let r = k p in
+        Tbl.add tbl p r ;
+        r
+end
+
+module EpheMemoT : MemoT = struct
+  module Tbl = Ephemeron.K1.Make (T)
+
+  type 'a t = 'a Tbl.t
+
+  let create size label =
+    let tbl = Tbl.create (scale size) in
+    at_exit (fun () -> print_stats label (hashtbl_stats (Tbl.stats tbl))) ;
+    tbl
+
+  let find_or_add tbl p k =
+    match Tbl.find_opt tbl p with
+    | Some r -> r
+    | None ->
+        let r = k p in
+        Tbl.add tbl p r ;
+        r
+end
+
+let memoT : (module MemoT) =
+  match memo_op with
+  | 0 -> (module NoMemoT)
+  | 1 -> (module HashMemoT)
+  | 2 -> (module EpheMemoT)
+  | _ -> assert false
+
+module MemoT = (val memoT)
+
+module type MemoTT = sig
+  type 'a t
+
+  val create : int -> string -> 'a t
+  val find_or_add : 'a t -> T.t -> T.t -> (T.t -> T.t -> 'a) -> 'a
+end
+
+module NoMemoTT : MemoTT = struct
+  type 'a t = unit
+
+  let create _ _ = ()
+  let find_or_add () p q k = k p q
+end
+
+module HashMemoTT : MemoTT = struct
+  module Tbl = Hashtbl.Make (struct
+    type t = T.t * T.t
+
+    let equal (p, q) (r, s) = p == r && q == s
+    let hash = Hashtbl.hash
+  end)
+
+  type 'a t = 'a Tbl.t
+
+  let create size label =
+    let tbl = Tbl.create (scale size) in
+    at_exit (fun () -> print_stats label (hashtbl_stats (Tbl.stats tbl))) ;
+    tbl
+
+  let find_or_add tbl p q k =
+    match Tbl.find_opt tbl (p, q) with
+    | Some r -> r
+    | None ->
+        let r = k p q in
+        Tbl.add tbl (p, q) r ;
+        r
+end
+
+module EpheMemoTT : MemoTT = struct
+  module Tbl = Ephemeron.K2.Make (T) (T)
+
+  type 'a t = 'a Tbl.t
+
+  let create size label =
+    let tbl = Tbl.create (scale size) in
+    at_exit (fun () -> print_stats label (hashtbl_stats (Tbl.stats tbl))) ;
+    tbl
+
+  let find_or_add tbl p q k =
+    match Tbl.find_opt tbl (p, q) with
+    | Some r -> r
+    | None ->
+        let r = k p q in
+        Tbl.add tbl (p, q) r ;
+        r
+end
+
+let memoTT : (module MemoTT) =
+  match memo_op with
+  | 0 -> (module NoMemoTT)
+  | 1 -> (module HashMemoTT)
+  | 2 -> (module EpheMemoTT)
+  | _ -> assert false
+
+module MemoTT = (val memoTT)
+
+module type MemoIT = sig
+  type 'a t
+
+  val create : int -> string -> 'a t
+  val find_or_add : 'a t -> int -> T.t -> (int -> T.t -> 'a) -> 'a
+end
+
+module NoMemoIT : MemoIT = struct
+  type 'a t = unit
+
+  let create _ _ = ()
+  let find_or_add () n q k = k n q
+end
+
+module HashMemoIT : MemoIT = struct
+  module Tbl = Hashtbl.Make (struct
+    type t = int * T.t
+
+    let equal (m, p) (n, q) = m = n && p == q
+    let hash = Hashtbl.hash
+  end)
+
+  type 'a t = 'a Tbl.t
+
+  let create size label =
+    let tbl = Tbl.create (scale size) in
+    at_exit (fun () -> print_stats label (hashtbl_stats (Tbl.stats tbl))) ;
+    tbl
+
+  let find_or_add tbl p q k =
+    match Tbl.find_opt tbl (p, q) with
+    | Some r -> r
+    | None ->
+        let r = k p q in
+        Tbl.add tbl (p, q) r ;
+        r
+end
+
+module EpheMemoIT : MemoIT = struct
+  module Tbl =
+    Ephemeron.K2.Make
+      (struct
+        type t = int
+
+        let equal m n = m = n
+        let hash = Hashtbl.hash
+      end)
+      (T)
+
+  type 'a t = 'a Tbl.t
+
+  let create size label =
+    let tbl = Tbl.create (scale size) in
+    at_exit (fun () -> print_stats label (hashtbl_stats (Tbl.stats tbl))) ;
+    tbl
+
+  let find_or_add tbl p q k =
+    match Tbl.find_opt tbl (p, q) with
+    | Some r -> r
+    | None ->
+        let r = k p q in
+        Tbl.add tbl (p, q) r ;
+        r
+end
+
+let memoIT : (module MemoIT) =
+  match memo_op with
+  | 0 -> (module NoMemoIT)
+  | 1 -> (module HashMemoIT)
+  | 2 -> (module EpheMemoIT)
+  | _ -> assert false
+
+module MemoIT = (val memoIT)
+
+(*
+ * ZDD constructors and operations
+ *)
+
+(** ∅ *)
+let empty = Empty
+
+(** {∅} *)
+let unit = Unit
+
+(** {{v}} *)
+let elem v = unique v ~t:Unit ~e:Empty
+
+(** [div1 f v] is [f/{{v}}], the quotient of division of family [f] by
+    elementary family [{{v}}]. That is, [f/{{v}}] is the elements of [f]
+    that contain [v], with [v] removed.
+
+    Similarly, [rem1 f v] is [f%{{v}}] the remainder of division of family
+    [f] by elementary family [{{v}}]. That is, [f%{{v}}] is the elements of
+    [f] that do not contain [v].
+
+    [div1] and [rem1] are the elementary special cases of general division
+    [div] and remainder [rem]. Division and remainder satisfy the equation:
+    [f = g⊔(f/g) ∪ (f%g)]. *)
+
+let div1_tbl = MemoT.create 1 "div1 memo table"
+
+(** [f/{{w}}], written [f/w], = [{ p-w | w ∈ p ∈ f }], or equivalently
+    [{q | q ∪ {w} ∈ f and q ∩ {w} = ∅}] *)
+let rec div1 f w =
+  match f with
+  | Empty ->
+      (* ∅/w = ∅ *)
+      Empty
+  | Unit ->
+      (* {∅}/w = ∅ *)
+      Empty
+  | Ite i -> (
+    match Elt.order i.v w with
+    | GT ->
+        (* v > w => (v⊔t ∪ e)/w = ∅ *)
+        Empty
+    | EQ ->
+        (* (w⊔t ∪ e)/w = t *)
+        i.t
+    | LT -> div1_memo f w )
+
+and div1_memo f w =
+  MemoT.find_or_add div1_tbl f
+  @@ fun f ->
+  let[@warning "-partial-match"] (Ite f) = f in
+  (* v < w => (v⊔t ∪ e)/w = v⊔(t/w) ∪ (e/w) *)
+  unique f.v ~t:(div1 f.t w) ~e:(div1 f.e w)
+
+let rem1_tbl = MemoT.create 1 "rem1 memo table"
+
+(** [f%{{w}}], written [f%w], = [{ p | w ∉ p ∈ f }] *)
+let rec rem1 f w =
+  match f with
+  | Empty ->
+      (* ∅%w = ∅ *)
+      Empty
+  | Unit ->
+      (* {∅}%w = {∅} *)
+      Unit
+  | Ite i -> (
+    match Elt.order i.v w with
+    | GT ->
+        (* v > w => (v⊔t ∪ e)%w = (v⊔t ∪ e) *)
+        f
+    | EQ ->
+        (* (w⊔t ∪ e)%w = e *)
+        i.e
+    | LT -> rem1_memo f w )
+
+and rem1_memo f w =
+  MemoT.find_or_add rem1_tbl f
+  @@ fun f ->
+  let[@warning "-partial-match"] (Ite f) = f in
+  (* v < w => (v⊔t ∪ e)%w = v⊔(t%w) ∪ (e%w) *)
+  unique f.v ~t:(rem1 f.t w) ~e:(rem1 f.e w)
+
+let union_tbl = MemoTT.create 65536 "union memo table"
+
+(** [f ∪ g] = [{ p | p ∈ f or p ∈ g }] *)
+let rec union f g =
+  if f == g then (* f ∪ f = f *) f
+  else if f == Empty then (* ∅ ∪ g = g *) g
+  else if g == Empty then (* f ∪ ∅ = f *) f
+  else union_memo f g
+
+and union_memo f g =
+  MemoTT.find_or_add union_tbl f g
+  @@ fun f g ->
+  match (f, g) with
+  | Ite i, Unit | Unit, Ite i ->
+      (* (v⊔t ∪ e) ∪ {∅} = v⊔t ∪ (e ∪ {∅}) *)
+      unique i.v ~t:i.t ~e:(union i.e Unit)
+  | Ite i, Ite j -> (
+    match Elt.order i.v j.v with
+    | LT ->
+        (* v < v' => (v⊔t ∪ e) ∪ (v'⊔t' ∪ e') = v⊔t ∪ (e ∪ (v'⊔t' ∪ e')) *)
+        unique i.v ~t:i.t ~e:(union i.e g)
+    | GT ->
+        (* v > v' => (v⊔t ∪ e) ∪ (v'⊔t' ∪ e') = v'⊔t' ∪ ((v⊔t ∪ e) ∪ e') *)
+        unique j.v ~t:j.t ~e:(union f j.e)
+    | EQ ->
+        (* (v⊔t ∪ e) ∪ (v⊔t' ∪ e') = v⊔(t ∪ t') ∪ (e ∪ e') *)
+        unique i.v ~t:(union i.t j.t) ~e:(union i.e j.e) )
+  | Empty, _ | _, Empty | Unit, Unit -> assert false
+
+let join_tbl = MemoTT.create 16 "join memo table"
+
+(** [f ⊔ g] = [{ p ∪ q | p ∈ f and q ∈ g }]. *)
+let rec join f g =
+  match (f, g) with
+  | Empty, _ | _, Empty ->
+      (* f ⊔ ∅ = ∅ *)
+      Empty
+  | Unit, f | f, Unit ->
+      (* f ⊔ {∅} = f *)
+      f
+  | Ite i, Ite j -> (
+    match Elt.order i.v j.v with
+    | GT ->
+        (* f ⊔ g = g ⊔ f *)
+        join_memo g f
+    | LT | EQ -> join_memo f g )
+
+and join_memo f g =
+  MemoTT.find_or_add join_tbl f g
+  @@ fun f g ->
+  let[@warning "-partial-match"] (Ite f) = f in
+  (* g = v⊔(g/v) ∪ g%v *)
+  let g_t = div1 g f.v in
+  let g_e = rem1 g f.v in
+  (*= (v⊔t ∪ e) ⊔ (v⊔(g/v) ∪ g%v)
+      = v⊔((t ⊔ g/v) ∪ (t ⊔ g%v) ∪ (e ⊔ g/v)) ∪ (e ⊔ g%v) *)
+  let t = union (join f.t g_t) (union (join f.t g_e) (join f.e g_t)) in
+  let e = join f.e g_e in
+  unique f.v ~t ~e
+
+let diff_tbl = MemoTT.create 512 "diff memo table"
+
+(** [p ∖ q] = [{ c | c ∈ p ∧ c ∉ q }] *)
+let rec diff p q =
+  if p == q then (* p ∖ p = ∅ *) empty
+  else if p == empty then (* ∅ ∖ _ = ∅ *) empty
+  else if q == empty then (* p ∖ ∅ = p *) p
+  else diff_memo p q
+
+and diff_memo p q =
+  MemoTT.find_or_add diff_tbl p q
+  @@ fun p q ->
+  match (p, q) with
+  | Ite i, Unit ->
+      (* (a*t ∨ e) ∖ {∅} = a*t ∨ (e ∖ {∅}) *)
+      unique i.v ~t:i.t ~e:(diff i.e unit)
+  | Unit, Ite j ->
+      (* {∅} ∖ (a*t ∨ e) = {∅} ∖ e *)
+      diff unit j.e
+  | Ite i, Ite j -> (
+    match Elt.order i.v j.v with
+    | LT ->
+        (* a < a' ⇒ (a*t ∨ e) ∖ (a'*t' ∨ e') = a*t ∨ (e ∖ (a'*t' ∨ e')) *)
+        unique i.v ~t:i.t ~e:(diff i.e q)
+    | EQ ->
+        (* (a*t ∨ e) ∖ (a*t' ∨ e') = (a*(t ∖ t') ∨ (e ∖ e')) *)
+        unique i.v ~t:(diff i.t j.t) ~e:(diff i.e j.e)
+    | GT ->
+        (* a > a' ⇒ (a*t ∨ e) ∖ (a'*t' ∨ e') = (a*t ∨ e) ∖ e' *)
+        diff p j.e )
+  | Empty, _ | _, Empty | Unit, Unit -> assert false
+
+let restrict_tbl = MemoTT.create 8192 "restrict memo table"
+
+(** [p Δ q] = [{ c | c ∈ p ∧ ∃d ∈ q. d ⊆ c }] *)
+let rec restrict p q =
+  if p == q then (* p Δ p = p *) p
+  else if p == empty then (* ∅ Δ q = ∅ *) empty
+  else if q == empty then (* p Δ ∅ = ∅ *) empty
+  else if q == unit then (* p Δ {∅} = p *) p
+  else restrict_memo p q
+
+and restrict_memo p q =
+  MemoTT.find_or_add restrict_tbl p q
+  @@ fun p q ->
+  match (p, q) with
+  | Unit, Ite j ->
+      (* {∅} Δ (a*t ∨ e) = {∅} Δ e *)
+      restrict unit j.e
+  | Ite i, Ite j -> (
+    match Elt.order i.v j.v with
+    | LT ->
+        (* a < a' ⇒ (a*t ∨ e) Δ (a'*t' ∨ e') = a*(t Δ q) ∨ (e Δ q) *)
+        unique i.v ~t:(restrict i.t q) ~e:(restrict i.e q)
+    | EQ ->
+        (* (a*t ∨ e) Δ (a*t' ∨ e') = a*(t Δ (t' ∪ e')) ∨ (e Δ e') *)
+        unique i.v ~t:(restrict i.t (union j.t j.e)) ~e:(restrict i.e j.e)
+    | GT ->
+        (* a > a' ⇒ (a*t ∨ e) Δ (a'*t' ∨ e') = a*(t Δ e') ∨ (e Δ e') *)
+        unique i.v ~t:(restrict i.t j.e) ~e:(restrict i.e j.e) )
+  | Empty, _ | _, Empty | Unit, Unit | Ite _, Unit -> assert false
+
+let bound_tbl = MemoIT.create 128 "bound memo table"
+
+(** [bound n p] = [{c | c ∈ p ∧ |c| ≤ n}] *)
+let rec bound n p =
+  if p == empty then empty
+  else if p == unit then unit
+  else if n <= 0 then unit
+  else bound_memo n p
+
+and bound_memo n p =
+  MemoIT.find_or_add bound_tbl n p
+  @@ fun n p ->
+  let[@warning "-partial-match"] (Ite p) = p in
+  unique p.v ~t:(bound (n - 1) p.t) ~e:(bound n p.e)
+
+let count_tbl = MemoT.create 2 "count memo table"
+
+(** [count f] is the number of sets in the family [f] *)
+let rec count f =
+  match f with Empty -> 0 | Unit -> 1 | Ite _ -> count_memo f
+
+and count_memo f =
+  MemoT.find_or_add count_tbl f
+  @@ fun f ->
+  let[@warning "-partial-match"] (Ite f) = f in
+  count f.t + count f.e
+
+(*
+ * Main
+ *)
+
+(* This encoding of the N-queens problem results in the diagrams growing and
+   then shrinking as the computation proceeds. This is ok for benchmarking
+   purposes, but note that Minato 1994 describes an alternate encoding that
+   avoids this. *)
+let main () =
+  let n = int_of_string Sys.argv.(1) in
+  let q c r = elem (c, r) in
+  (* all placements of 0 to n² queens on n×n board *)
+  let all =
+    let a = ref unit in
+    for i = 0 to n - 1 do
+      for j = 0 to n - 1 do
+        a := join !a (union unit (q i j))
+      done
+    done ;
+    !a
+  in
+  (* all pairs of positions that attack each other *)
+  let attacks =
+    let a = ref empty in
+    for i = 0 to n - 1 do
+      for j = 0 to n - 1 do
+        (* attacks down *)
+        for k = i + 1 to n - 1 do
+          a := union !a (join (q i j) (q k j))
+        done ;
+        (* attacks right *)
+        for k = j + 1 to n - 1 do
+          a := union !a (join (q i j) (q i k))
+        done ;
+        (* attacks down-right *)
+        for k = 1 to min (n - i) (n - j) - 1 do
+          a := union !a (join (q i j) (q (i + k) (j + k)))
+        done ;
+        (* attacks down-left *)
+        for k = 1 to min (n - i) (j + 1) - 1 do
+          a := union !a (join (q i j) (q (i + k) (j - k)))
+        done
+      done
+    done ;
+    !a
+  in
+  (* placements containing at least one attack *)
+  let unsafe = restrict all attacks in
+  (* placements not containing any attacks *)
+  let safe = diff all unsafe in
+  (* placements not containing any attacks but with too few queens *)
+  let small = bound (n - 1) safe in
+  (* safe placements that have enough queens *)
+  let solution = diff safe small in
+  (* output results *)
+  let num_results = count solution in
+  print_int n ;
+  print_char ' ' ;
+  print_int num_results ;
+  print_newline ()
+
+;;
+main ()
diff --git a/run_config.json b/run_config.json
index 78c48e815..4f7fa9333 100644
--- a/run_config.json
+++ b/run_config.json
@@ -1534,6 +1534,19 @@
         }
       ]
     },
+    {
+      "executable": "benchmarks/zdd/zdd_queens.exe",
+      "name": "zdd_queens",
+      "tags": [
+        "10s_100s",
+        "macro_bench"
+      ],
+      "runs": [
+        {
+          "params": "7"
+        }
+      ]
+    },
     {
       "executable": "benchmarks/markbench/markbench.exe",
       "name": "markbench",