Solver is often stumped by restrictive upper bounds

[snoyberg]

To define the term: by "restrictive upper bound" I mean an upper bound which excludes some packages available from Hackage. So if foo 1.0, 1.1, and 1.2 are available on Hackage, a bound of foo < 1.3 would not be restrictive, whereas foo < 1.2 would be restrictive.

I went to build a project I haven't touched in a few months (haskellers.com), and cabal was unable to produce a build plan. Eventually, I whittled this down to this cabal file. In this file, there is only one restrictive upper bound: http-conduit. I then ran the following command with both cabal-install 1.16 + GHC 7.6 and cabal-install 1.18 + GHC 7.8:

clear;date;cabal install --dry-run --reorder-goals --max-backjumps=-1;date

In both cases, there was no response for approximately 15 minutes, at which point I killed cabal. However, I was able to cause the dry run to succeed almost immediately (< 10 seconds) with either of the following:

1. Adding: --constraint 'http-conduit == 1.9.6'
2. Relaxing the upper bound on http-conduit to allow the newest version.

I'd like to note that these are the kinds of errors Yesod users complained about regularly in the past. The ultimate "solution" I settled on was (1) encourage usage of yesod-platform to help out the constraint solver, and (2) remove most upper bounds in cabal files. Obviously it would be better if cabal was better able to handle these situations.

[tibbe]

I would be interested to know if a proper SMT solver would come up with a solution, when fed with the constraints. It would be possible to have cabal just print all the constraints and then copy-n-paste them into an off-the-shelf constraint solver.

[NathanHowell]

I mostly hacked together a Cabal version constraint solver prototype using Z3 a while back. It works, and it is fast. Like all of Hackage in less than a second fast. There needs to be a lot more work done to produce user friendly errors, and to apply some other common sense rules.. it also needs some patches to the z3 bindings to support incremental solves. Etc etc.

https://gist.github.com/NathanHowell/5688647

[tibbe]

@NathanHowell That's really cool. Do you have an example of the kind of error messages it gives and your thoughts on how they could be improved? I would like to investigate using a real solver. It might get rid of lots of the problems we have.

Ideally the solver error message would include a minimal sense of constraints that cause a conflict to appear. Can Z3 produce such a thing?

[byorgey]

Whoops, I was writing a comment but then decided against it, and accidentally clicked "close".

[avsm]

@tibbe : we use aspcud in OPAM, which uses a format called CUDF as the interchange format to external solvers. Would probably be effective for Cabal too...

[NathanHowell]

@tibbe SAT and SMT solvers provide some tools for this but generally you need to do it yourself. If a solution is found it may not be the best one, but it is a solution. And for counterexamples they can be complex, not a simple one... So you need to do that yourself. Incremental solvers like z3 can make it faster but it's still a lot of code to write.

[snoyberg]

I'm beginning to think this is caused exclusively by --reorder-goals. I was doing some investigation into something similar the other day, and was able to get cabal to sit at "Resolving dependencies" for over an hour. Removing --reorder-goals and keeping just --max-backjumps=-1 let it complete in under a minute.

[23Skidoo]

@snoyberg

I'm beginning to think this is caused exclusively by --reorder-goals.

cabal-install 1.24 will have some performance improvements to --reorder-goals (#3208).

[Blaisorblade]

There's also a wiki page on constraint-solving through SAT-solving:
https://github.com/haskell/cabal/wiki/Constraint-Solving

I think that could be really cool.

The wiki-page is somehow confused on conditional constraints — implications seem easy to encode as boolean formulas. What might be harder is enabling flags automatically if they add dependencies that are available, if desired (I'm not sure that's the current behavior of flags, but such flags are desirable in a few scenarios, say https://www.reddit.com/r/haskell/comments/4pf86b/cabal_build_variants/d4kv7yp).

EDIT: to be sure, you can easily express in a boolean formula that the presence of a package implies a certain flag, but that forces the flag. It seems one would need to somehow use MaxSAT (that maximizes the number of enabled booleans in a solution) but use "maximize" only some variables, I don't know if that's available out-of-the-box.

[hvr]

@Blaisorblade translating the cabal constraint satisfaction problem into SAT or SMT language is mostly straight-forward; several people (including myself) have done this in the past, and it's mostly a matter of sitting down on a calm weekend. And in fact, solvers like Z3 then can easily beat the modular cabal solver finding some arbitrary solution. However, as soon as you want an optimal solution according to some criteria (which you then need to encode in the SMT/SAT language as well), things get ugly and demotivating, and then the realization sets in that the modular cabal solver is not that bad after all... :-/

[Blaisorblade]

Just found #2860, answering there...

[cartazio]

Question: has anyone tried using a datalog variant?
In some respects we want the max of viable build plans , and if two build
plans are incomparable in the partial order of versions that's where things
get interesting!

I may have a poke at seeing if the data log tools in z3 and friends are
helpful here. There's been a lot of interesting work in the past two or
three years at this intersection

On Friday, July 8, 2016, Herbert Valerio Riedel [email protected]
wrote:

@Blaisorblade https://github.com/Blaisorblade translating the cabal
constraint satisfaction problem into SAT or SMT language is mostly
straight-forward; several people (including myself) have done this in the
past, and it's mostly a matter of sitting down on a calm weekend. And in
fact, solvers like Z3 then can easily beat the modular cabal solver finding
some arbitrary solution. However, as soon as you want an optimal solution
according to some criteria (which you then need to encode in the SMT/SAT
language as well), things get ugly quite and demotivating, and the modular
cabal solver turns out to be better suited... :-/

—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub
#1783 (comment), or mute
the thread
https://github.com/notifications/unsubscribe/AAAQwii2okK4Djy4w-lp_PLx_Hhef-l7ks5qTgMZgaJpZM4BzR2c
.

[grayjay]

I think that cabal is much better at handling restrictive upper bounds now that it can reorder goals with the conflict counting feature added in #3513. If a package has a restrictive upper bound and it occurs frequently in conflict sets, conflict counting causes the solver to choose the packages affected by the constraint earlier. Then it can make choices that take the constraint into account.

I tried to reproduce the original problem by specifying --index-state and turning off conflict counting, and the results seemed consistent. I ran cabal install --dry-run --reorder-goals --max-backjumps=-1 --index-state 2014-04-15T22:20:17Z --no-count-conflicts on haskellers.cabal with GHC 7.6.3. cabal was still running after 15 minutes. Adding --constraint 'http-conduit == 1.9.6' or lifting the upper bound on http-conduit caused it to finish in ~7 seconds.

Turning --count-conflicts back on allowed cabal to find a solution in ~20 seconds with the first command. In fact, --reorder-goals wasn't necessary, and cabal install --dry-run --max-backjumps=-1 --index-state 2014-04-15T22:20:17Z finished in 4 seconds. The -v3 log showed that the solver chose http-conduit at level 154 on its first descent of the search tree but chose it at level 6 before descending to the solution, so --count-conflicts had moved it higher up in the tree.

Please open another issue if there is still a problem.