Version 2 (modified by nominolo, 5 years ago)

begin SAT-translation thoughts

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>
```