This adds an experimental concretizer to Spack that makes use of Answer Set Programming. The new solver uses clingo, the combined grounder (gringo) and solver (clasp) from Potassco, instead of attempting to do the entire solve in Python as we did before.

Problem

The current concretizer is not exhaustive and is not guaranteed to find a solution if one exists. It is greedy, does not do backtracking, and as a result the errors it gives can be confusing. In many cases it can resolve a constraint too early -- it assigns final values to nodes as it builds the graph, and it may assign a version, variant, or other value to a node without considering the entire problem. This can result in the concretizer finding conflicts where solutions exist.

Extending the current concretizer is difficult. There are many moving pieces, and rewriting any of them can be a lot of work. Making major changes to concretization semantics is difficult, and increasingly we're unable to add features that users need.

The concretization problem that Spack solves is NP-complete (as is regular old dependency resolution with just versions), so we have decided to start using more powerful solvers to address it. Using Clingo is a step in this direction.

How it works

Answer Set programming looks like Prolog but has the advantage that, rather than trying to be a full programming language, it reduces logic problems to CDCL SAT with optimization. ASP has the nice property that solves will always terminate (unlike Prolog programs), and it follows the stable model semantics, which makes it easier to model some of the default-driven behavior in Spack. The constraints in Spack are essentially SAT clauses, and our preferences (like packages.yaml) add optimization weights to this. We don't just want a solution -- we want the best one, with preferred variants, compilers, etc.

The prior concretizer iteratively expanded nodes in the graph and attempted to unify them greedily as they were expanded. It used a fixed-point algorithm; iterating and expanding optional dependencies, replacing virtuals with providers, setting variants, versions, and compilers, etc. until there were no more changes to the DAG.

The new concretizer is less dynamic. It works like this:

1. Look at the input specs and read in all possible dependencies
2. Translate constraints in Spack's package DSL to rules and facts in ASP. e.g., zlib has some facts like this:

   version_declared("zlib","1.2.11",0).
   version_declared("zlib","1.2.8",1).
   version_declared("zlib","1.2.3",2).
   
   variant("zlib","optimize").
   variant_single_value("zlib","optimize").
   variant_default_value_from_package_py("zlib","optimize","True").
   variant_possible_value("zlib","optimize","False").
   variant_possible_value("zlib","optimize","True").

   These come directly from version() and variant() directives in the zlib/package.py file.
3. Combine these facts with the logic program in lib/spack/spack/solver/concretize.lp. This defines all the rules and optimization criteria used in concretization in Spack.
4. Send the whole program off to Clingo
5. Read back one the optimal stable model found by the solver, and build a concrete Spec from it.

One nice thing about this is that it's declarative; we can add extra constraints and features more easily now, without having to reengineer the entire algorithm. Another is that we can solve much more complex problems than we could before. Finally, it will be easier going forward to implement many of the features we have planned (compilers as dependencies, optimizing for installed packages, etc.) using a real solver.

Error reporting

We are using Clingo's support for finding unsatisfiable cores to generate error messages. If something fails to concretize, the solver will tell you why by reporting a set of facts and rules that cannot be resolved together. This can be very useful, as often it points directly to conflicts and can be used, with a little staring, to debug issues. In other cases the core can still be quite large, and thus hard to interpret. Cores are not guaranteed to be minimal by Clingo. Improving these messages and converting them to understandable sentences is on our list of follow-on activities.

Alternatives

There are more details on alternatives in this FOSDEM talk. So far, Clingo works well, but we are also investigating Z3, an SMT solver. Z3 is more widely used and has a richer API, but its input language is in some sense more primitive, in that it doesn't accept or automatically ground first-order logic like Clingo. We are investigating which solver will be easiest to include (vendor) with Spack so that we can use the new concretizer everywhere.

Using the new concretizer

There is a new section in config.yaml:

  # The concretization algorithm to use in Spack. Options are:
  #
  #   'original': Spack's original greedy, fixed-point concretizer. This
  #       algorithm can make decisions too early and will not backtrack
  #       sufficiently for many specs.
  #
  #   'clingo': Uses a logic solver under the hood to solve DAGs with full
  #       backtracking and optimization for user preferences.
  #
  # 'clingo' currently requires the clingo ASP solver to be installed and
  # built with python bindings. 'original' is built in.
  concretizer: original

1. You'll need to set concretizer: to clingo to use clingo everywhere.
2. You will also need to spack install clingo@master and get clingo on your PATH to use the new concretizer.

Even if the new concretizer is not enabled, you can use the spack solve command as you would normally use spack spec -- it will try to use the new concretizer. spack solve will eventually go away but for now we have two commands.

Bugs fixed

fixes #267
fixes #303
fixes #1781
fixes #2310
fixes #2632
fixes #3628
fixes #4635
fixes #5651
fixes #7339
fixes #8082
fixes #9025
fixes #9414
fixes #9696
fixes #9744
fixes #9753
fixes #9911
fixes #12431
fixes #19764