diff --git a/master_changes.md b/master_changes.md
index 28d0eb9cb92..3ee4aa2ba3c 100644
--- a/master_changes.md
+++ b/master_changes.md
@@ -163,6 +163,7 @@ users)
   * Fix a rare potential GC corruption in `OpamStubs.uname` [#6880 @avsm @kit-ty-kate @andrew]
   * Fix a rare potential GC corruption in `OpamStubs.enumRegistry` on Windows [#6882 @kit-ty-kate]
   * Remove uses of `Stdlib.ignore` [#6481 @rjbou @kit-ty-kate]
+  * Mitigate potential exponential blow-up converting dependency formulae to DNF [#6831 @dra27]
 
 ## Internal: Unix
 
diff --git a/src/format/opamFormula.ml b/src/format/opamFormula.ml
index 9fc4827efc4..a5c5c12174b 100644
--- a/src/format/opamFormula.ml
+++ b/src/format/opamFormula.ml
@@ -396,15 +396,47 @@ let dnf_of_formula t =
     | And (x,y) -> mk_right (mk x) (mk y) in
   mk t
 
-let verifies f nv =
-  let name_formula =
-    map (fun ((n, _) as a) -> if n = OpamPackage.name nv then Atom a else Empty)
-      (dnf_of_formula f)
+let name_formula name f =
+  let is_name (n, _cstr) = OpamPackage.Name.equal n name in
+  let formula_or_empty cond f = if cond then f else Empty in
+  (* Determine if nv could possibly part of the solution for [f]. This
+     means checking that either [v] satisfies the constraints on name.
+     This is done by converting [f] to DNF, which allows us to transform
+     the formula into a union of intervals, where ignoring atoms for
+     different package names works. We can then ignore conjunctions
+     where [name] doesn't appear. However, this function is typically
+     used on a dependency formula, which is most normally a large
+     conjunction. We capitalise on this with a peephole simplification,
+     observing that if we're testing for package name A in the formula
+     [X & Y], then we can ignore X if it doesn't contain A (and likewise
+     Y). This eliminates unrelated sub-formula from the top-level
+     conjunction, in particular it means that
+     [Dep1 & Dep2 & (Dep3 | Dep4) & (Dep5 | Dep6)] does not cause
+     trigger worst-case expansion for DNF. *)
+  let rec simplify_formula f =
+    match f with
+    | Empty -> Empty
+    | Atom atom ->
+      formula_or_empty (is_name atom) f
+    | Block b ->
+      formula_or_empty (exists is_name b) f
+    | Or(a, b) ->
+      formula_or_empty (exists is_name a || exists is_name b) f
+    | And(a, b) ->
+      let a = simplify_formula a in
+      let b = simplify_formula b in
+      make_and a b
   in
-  name_formula <> Empty &&
+  simplify_formula f
+  |> dnf_of_formula
+  |> map (fun a -> formula_or_empty (is_name a) (Atom a))
+
+let verifies f nv =
+  let f = name_formula (OpamPackage.name nv) f in
+  f <> Empty &&
   eval (fun (_name, cstr) ->
       check_version_formula cstr (OpamPackage.version nv))
-    name_formula
+    f
 
 let all_names f =
   fold_left (fun acc (name, _) ->
@@ -412,22 +444,14 @@ let all_names f =
     OpamPackage.Name.Set.empty f
 
 let packages pkgset f =
-  let names = all_names f in
-  (* dnf allows us to transform the formula into a union of intervals, where
-     ignoring atoms for different package names works. *)
-  let dnf = dnf_of_formula f in
   OpamPackage.Name.Set.fold (fun name acc ->
-      (* Ignore conjunctions where [name] doesn't appear *)
-      let name_formula =
-        map (fun ((n, _) as a) -> if n = name then Atom a else Empty) dnf
-      in
+      let f = name_formula name f in
       OpamPackage.Set.union acc @@
       OpamPackage.Set.filter (fun nv ->
           let v = OpamPackage.version nv in
-          eval (fun (_name, cstr) -> check_version_formula cstr v)
-            name_formula)
+          eval (fun (_name, cstr) -> check_version_formula cstr v) f)
         (OpamPackage.packages_of_name pkgset name))
-    names OpamPackage.Set.empty
+    (all_names f) OpamPackage.Set.empty
 
 (* Convert a t an atom formula *)
 let to_atom_formula (t:t): atom formula =
diff --git a/src/state/opamSwitchState.ml b/src/state/opamSwitchState.ml
index 4ccf61d68f4..d2388ffaf42 100644
--- a/src/state/opamSwitchState.ml
+++ b/src/state/opamSwitchState.ml
@@ -1054,13 +1054,15 @@ let universe st
                             OpamPackage.Map.find nv u_depopts ])
       |> OpamFormula.packages st.packages
     in
-    let requested_deps =
-      OpamPackage.Set.fixpoint resolve_deps requested_allpkgs
-    in
-    requested_deps %% Lazy.force st.reinstall ++
-    match reinstall with
-    | Some set -> set
-    | None -> OpamPackage.Set.empty
+    let reinstall = Option.value ~default:OpamPackage.Set.empty reinstall in
+    let lazy switch_reinstall = st.reinstall in
+    if OpamPackage.Set.is_empty switch_reinstall then
+      reinstall
+    else
+      let requested_deps =
+        OpamPackage.Set.fixpoint resolve_deps requested_allpkgs
+      in
+      requested_deps %% Lazy.force st.reinstall ++ reinstall
   in
   let missing_depexts =
     lazy (