diff --git a/lib/spack/spack/solver/cycle_detection.lp b/lib/spack/spack/solver/cycle_detection.lp
index b148591760..310c543623 100644
--- a/lib/spack/spack/solver/cycle_detection.lp
+++ b/lib/spack/spack/solver/cycle_detection.lp
@@ -3,9 +3,15 @@
 %
 % SPDX-License-Identifier: (Apache-2.0 OR MIT)
 
+%=============================================================================
 % Avoid cycles in the DAG
-% some combinations of conditional dependencies can result in cycles;
-% this ensures that we solve around them
+%
+% Some combinations of conditional dependencies can result in cycles;
+% this ensures that we solve around them. Note that these rules are quite
+% demanding on both grounding and solving, since they need to compute and
+% consider all possible paths between pair of nodes.
+%=============================================================================
+
 
 #program no_cycle.
 path(Parent, Child) :- depends_on(Parent, Child).
diff --git a/lib/spack/spack/solver/heuristic.lp b/lib/spack/spack/solver/heuristic.lp
index cb1f548e3b..80c3c529ad 100644
--- a/lib/spack/spack/solver/heuristic.lp
+++ b/lib/spack/spack/solver/heuristic.lp
@@ -3,6 +3,11 @@
 %
 % SPDX-License-Identifier: (Apache-2.0 OR MIT)
 
+%=============================================================================
+% Heuristic to speed-up solves
+%=============================================================================
+
+
 %-----------------
 % Domain heuristic
 %-----------------
diff --git a/lib/spack/spack/solver/os_compatibility.lp b/lib/spack/spack/solver/os_compatibility.lp
index a484a90a3d..3c0c223a86 100644
--- a/lib/spack/spack/solver/os_compatibility.lp
+++ b/lib/spack/spack/solver/os_compatibility.lp
@@ -3,9 +3,11 @@
 %
 % SPDX-License-Identifier: (Apache-2.0 OR MIT)
 
+%=============================================================================
 % OS compatibility rules for reusing solves.
 % os_compatible(RecentOS, OlderOS)
 % OlderOS binaries can be used on RecentOS
+%=============================================================================
 
 % macOS
 os_compatible("monterey", "bigsur").
diff --git a/lib/spack/spack/solver/when_possible.lp b/lib/spack/spack/solver/when_possible.lp
index 7a8ddfef1c..b887c9175f 100644
--- a/lib/spack/spack/solver/when_possible.lp
+++ b/lib/spack/spack/solver/when_possible.lp
@@ -3,6 +3,13 @@
 %
 % SPDX-License-Identifier: (Apache-2.0 OR MIT)
 
+%=============================================================================
+% Minimize the number of literals that are not solved
+%
+% This minimization is used for the "when_possible" concretization mode,
+% otherwise we assume that all literals must be solved.
+%=============================================================================
+
 % Give clingo the choice to solve an input spec or not
 { solve_literal(ID) } :- literal(ID).
 literal_not_solved(ID) :- not solve_literal(ID), literal(ID).