ASP-based solver: reduce input facts and add heuristic (#28848)

* Remove node_target_satisfies/3 in favor of target_satisfies/2

When emitting input facts we don't need to couple target with
packages, but we can emit fewer facts independently and let
the grounder combine them.

* Remove compiler_version_satisfies/4 in favor of compiler_version_satisfies/3

When emitting input facts we don't need to couple compilers with
packages, but we can emit fewer facts independently and let
the grounder combine them.

* Introduce heuristic in the ASP-program

With heuristic we can drive clingo to make better
initial guesses, which lead to fewer choices and
conflicts in the overall solve

2 files changed, 49 insertions, 44 deletions

diff --git a/lib/spack/spack/solver/asp.py b/lib/spack/spack/solver/asp.py
index ea603fd92f..6b656efba0 100644
--- a/lib/spack/spack/solver/asp.py
+++ b/lib/spack/spack/solver/asp.py
@@ -535,10 +535,9 @@ class PyclingoDriver(object):
 
         # Initialize the control object for the solver
         self.control = clingo.Control()
-        self.control.configuration.solve.models = nmodels
-        self.control.configuration.asp.trans_ext = 'all'
-        self.control.configuration.asp.eq = '5'
         self.control.configuration.configuration = 'tweety'
+        self.control.configuration.solve.models = nmodels
+        self.control.configuration.solver.heuristic = 'Domain'
         self.control.configuration.solve.parallel_mode = '1'
         self.control.configuration.solver.opt_strategy = "usc,one"
 
@@ -717,7 +716,7 @@ class SpackSolverSetup(object):
         if str(target) in archspec.cpu.TARGETS:
             return [single_target_fn(spec.name, target)]
 
-        self.target_constraints.add((spec.name, target))
+        self.target_constraints.add(target)
         return [fn.node_target_satisfies(spec.name, target)]
 
     def conflict_rules(self, pkg):
@@ -1218,8 +1217,7 @@ class SpackSolverSetup(object):
                 clauses.append(
                     fn.node_compiler_version_satisfies(
                         spec.name, spec.compiler.name, spec.compiler.versions))
-                self.compiler_version_constraints.add(
-                    (spec.name, spec.compiler))
+                self.compiler_version_constraints.add(spec.compiler)
 
         # compiler flags
         for flag_type, flags in spec.compiler_flags.items():
@@ -1405,9 +1403,12 @@ class SpackSolverSetup(object):
             for target in supported:
                 best_targets.add(target.name)
                 self.gen.fact(fn.compiler_supports_target(
-                    compiler.name, compiler.version, target.name))
-                self.gen.fact(fn.compiler_supports_target(
-                    compiler.name, compiler.version, uarch.family.name))
+                    compiler.name, compiler.version, target.name
+                ))
+
+            self.gen.fact(fn.compiler_supports_target(
+                compiler.name, compiler.version, uarch.family.name
+            ))
 
         # add any targets explicitly mentioned in specs
         for spec in specs:
@@ -1536,18 +1537,12 @@ class SpackSolverSetup(object):
     def define_compiler_version_constraints(self):
         compiler_list = spack.compilers.all_compiler_specs()
         compiler_list = list(sorted(set(compiler_list)))
-
-        for pkg_name, cspec in self.compiler_version_constraints:
+        for constraint in sorted(self.compiler_version_constraints):
             for compiler in compiler_list:
-                if compiler.satisfies(cspec):
-                    self.gen.fact(
-                        fn.node_compiler_version_satisfies(
-                            pkg_name,
-                            cspec.name,
-                            cspec.versions,
-                            compiler.version
-                        )
-                    )
+                if compiler.satisfies(constraint):
+                    self.gen.fact(fn.compiler_version_satisfies(
+                        constraint.name, constraint.versions, compiler.version
+                    ))
         self.gen.newline()
 
     def define_target_constraints(self):
@@ -1572,8 +1567,7 @@ class SpackSolverSetup(object):
             return allowed_targets
 
         cache = {}
-        for spec_name, target_constraint in sorted(self.target_constraints):
-
+        for target_constraint in sorted(self.target_constraints):
             # Construct the list of allowed targets for this constraint
             allowed_targets = []
             for single_constraint in str(target_constraint).split(','):
@@ -1584,11 +1578,7 @@ class SpackSolverSetup(object):
                 allowed_targets.extend(cache[single_constraint])
 
             for target in allowed_targets:
-                self.gen.fact(
-                    fn.node_target_satisfies(
-                        spec_name, target_constraint, target
-                    )
-                )
+                self.gen.fact(fn.target_satisfies(target_constraint, target))
             self.gen.newline()
 
     def define_variant_values(self):
diff --git a/lib/spack/spack/solver/concretize.lp b/lib/spack/spack/solver/concretize.lp
index f4c15397e2..13902d0892 100644
--- a/lib/spack/spack/solver/concretize.lp
+++ b/lib/spack/spack/solver/concretize.lp
@@ -15,7 +15,7 @@
 :- not 1 { version(Package, _) } 1, node(Package).
 
 % each node must have a single platform, os and target
-:- not 1 { node_platform(Package, _) } 1, node(Package).
+:- not 1 { node_platform(Package, _) } 1, node(Package), error("A node must have exactly one platform").
 :- not 1 { node_os(Package, _) } 1, node(Package).
 :- not 1 { node_target(Package, _) } 1, node(Package).
 
@@ -34,7 +34,7 @@ version_declared(Package, Version, Weight) :- version_declared(Package, Version,
 % We can't emit the same version **with the same weight** from two different sources
 :- version_declared(Package, Version, Weight, Origin1),
    version_declared(Package, Version, Weight, Origin2),
-   Origin1 != Origin2,
+   Origin1 < Origin2,
    error("Internal error: two versions with identical weights").
 
 % versions are declared w/priority -- declared with priority implies declared
@@ -450,7 +450,7 @@ variant_set(Package, Variant) :- variant_set(Package, Variant, _).
    variant_value(Package, Variant, Value2),
    variant_value_from_disjoint_sets(Package, Variant, Value1, Set1),
    variant_value_from_disjoint_sets(Package, Variant, Value2, Set2),
-   Set1 != Set2,
+   Set1 < Set2,
    build(Package),
    error("Variant values selected from multiple disjoint sets").
 
@@ -546,9 +546,6 @@ variant_single_value(Package, "dev_path")
 % Platform semantics
 %-----------------------------------------------------------------------------
 
-% one platform per node
-:- M = #count { Platform : node_platform(Package, Platform) }, M !=1, node(Package), error("A node must have exactly one platform").
-
 % if no platform is set, fall back to the default
 node_platform(Package, Platform)
  :- node(Package),
@@ -614,15 +611,21 @@ node_os(Package, OS) :- node_os_set(Package, OS), node(Package).
 %-----------------------------------------------------------------------------
 % Target semantics
 %-----------------------------------------------------------------------------
-% one target per node -- optimization will pick the "best" one
+
+% Each node has only one target chosen among the known targets
 1 { node_target(Package, Target) : target(Target) } 1 :- node(Package), error("Each node must have exactly one target").
 
-% node_target_satisfies semantics
-1 { node_target(Package, Target) : node_target_satisfies(Package, Constraint, Target) } 1
+% If a node must satisfy a target constraint the choice is reduced among the targets
+% that satisfy that constraint
+1 { node_target(Package, Target) : target_satisfies(Constraint, Target) } 1
   :- node_target_satisfies(Package, Constraint), error("Each node must have exactly one target").
+
+% If a node has a target and the target satisfies a constraint, then the target
+% associated with the node satisfies the same constraint
 node_target_satisfies(Package, Constraint)
-  :- node_target(Package, Target), node_target_satisfies(Package, Constraint, Target).
-#defined node_target_satisfies/3.
+  :- node_target(Package, Target), target_satisfies(Constraint, Target).
+
+#defined target_satisfies/2.
 
 % The target weight is either the default target weight
 % or a more specific per-package weight if set
@@ -702,20 +705,21 @@ node_compiler(Package, Compiler) :- node_compiler_version(Package, Compiler, _).
    Compiler1 != Compiler2,
    error("Internal error: mismatch between selected compiler and compiler version").
 
-% define node_compiler_version_satisfies/3 from node_compiler_version_satisfies/4
-% version_satisfies implies that exactly one of the satisfying versions
-% is the package's version, and vice versa.
+% If the compiler of a node must satisfy a constraint, then its version
+% must be chosen among the ones that satisfy said constraint
 1 { node_compiler_version(Package, Compiler, Version)
-    : node_compiler_version_satisfies(Package, Compiler, Constraint, Version) } 1 :-
+    : compiler_version_satisfies(Compiler, Constraint, Version) } 1 :-
     node_compiler_version_satisfies(Package, Compiler, Constraint),
     error("Internal error: node compiler version mismatch").
 
+% If the node is associated with a compiler and the compiler satisfy a constraint, then
+% the compiler associated with the node satisfy the same constraint
 node_compiler_version_satisfies(Package, Compiler, Constraint)
   :- node_compiler_version(Package, Compiler, Version),
-     node_compiler_version_satisfies(Package, Compiler, Constraint, Version),
+     compiler_version_satisfies(Compiler, Constraint, Version),
      build(Package).
 
-#defined node_compiler_version_satisfies/4.
+#defined compiler_version_satisfies/3.
 
 % If the compiler version was set from the command line,
 % respect it verbatim
@@ -1017,3 +1021,14 @@ opt_criterion(1, "non-preferred targets").
     : node_target_weight(Package, Weight),
       build_priority(Package, Priority)
 }.
+
+%-----------------
+% Domain heuristic
+%-----------------
+#heuristic version(Package, Version) : version_declared(Package, Version, 0), node(Package). [10, true]
+#heuristic version_weight(Package, 0) : version_declared(Package, Version, 0), node(Package). [10, true]
+#heuristic node_target(Package, Target) : default_target_weight(Target, 0), node(Package). [10, true]
+#heuristic node_target_weight(Package, 0) : node(Package). [10, true]
+#heuristic variant_value(Package, Variant, Value) : variant_default_value(Package, Variant, Value), node(Package). [10, true]
+#heuristic provider(Package, Virtual) : possible_provider_weight(Package, Virtual, 0, _), virtual_node(Virtual). [10, true]
+#heuristic node(Package) : possible_provider_weight(Package, Virtual, 0, _), virtual_node(Virtual). [10, true]