Constraint Solving

Imported from Trac wiki; be wary of outdated information or markup mishaps.

Trying to "finalise" a GenericPackageDescription to a PackageDescription can be seen as a constraint satisfaction problem. In this page we'll try to formalise the problem and give a translation of the problem into a constraint language.

Simple constraints

Simple packages just depend on a fixed number of packages and have version predicates as constraints.

name: foo
version: 1.0
build-depends: bar >= 1.2 && < 1.4, baz

So the problem here is to find versions of bar and baz that satisfy these version constraints.

bar >= 1.2
bar < 1.4

So there is no constraint on baz and two on bar. A key point is that we must pick a single version of bar and baz that satisfy all these constraints simultaneously. We've set up the constraints above so that will always be true by picking just one variable for each package name. So the form of constraints here is very simple, we have variables which range over versions and we have atomic constraints using ==, >=, >, <=, < operators. Complex version range expressions can be expanded out into this form.

To solve this we also need to know the possible values that bar and baz can take. These correspond to the versions of the installed or available packages.

Translation to Propositional Formulas

SAT-solvers for propositional formulas can be very fast and compact as demonstrated by miniSAT (600 SLOC of C++ code). To be able to use them, however, we need to be able to express our problem in a form that can be solved by miniSAT, though.

A SAT-solver accepts clauses as input. A clause is a disjunction of possibly negated variables. A propositional variable can either be true or false. The goal of the SAT-solver is to find an assignments to for each variable that makes all clauses true.

Say we have the following versions of the package bar available: bar-1.2, bar-1.2.3, bar-1.3, bar-1.4 Then the constraint bar > 1.2 can be expressed as bar == 1.2.3 || bar == 1.3 || bar == 1.4. We can translate this into propositional variables:

not <bar-1.2>, <bar-1.2.3>, <bar-1.3>, <bar-1.4>

Conditional constraints

With the addition of configurations to the cabal syntax we have a more complex satisfaction problem.

name: foo
version: 1.0
flag: f
if flag(f)
  build-depends: bar >= 1.2

This gives us a constraint of the form

f => (bar >= 1.2)

They can be nested:

flag f
flag g
if flag(f)
  if flag(g)
    build-depends: bar >= 1.2
  else
    build-depends: baz >= 1.0

giving:

f &&  g => bar >= 1.2
f && ¬g => baz >= 1.0

Additionally we have to be clear about what it means to depend on a package now that they are optional. One way is to use as a constraint that the package must take the value of one of the available versions. So for example if we have foo-1.0 and foo-1.1 and we know we depend on some version of foo then we have the constraint

baz == 1.0 || baz == 1.1

That allows us to give meaning to:

name: foo
version: 1.0
flag: f
if flag(f)
  build-depends: baz

f => (baz == 1.0 || baz == 1.1)

So the obvious question now is what is a => implication constraint exactly and how do we solve them.