[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

SAT-Britney status and howto


a quick status update for those who are not at DebConf to hear me
rambling about it (or who are here but might have missed the odd

It basically works, and even reasonably fast. Also the problem of
finding a Free PMAX-SAT solver is solved: Matthew Gwynne pointed me to
clasp which is already in Debian, was backported to squeeze by me and
installation on ries has been requested (though not performed yet, until
then it still uses minimaxsat).

If you want to play with it: Some information can be found on
and from the --help output, which I paste here for your convenience:

$ export GCONV_PATH=/usr/lib64/gconv
$ ./SAT-Britney --help
Usage: SAT-Britney -d DIR [OPTION...]

  -d DIR       --dir=DIR                  directory containing britney data
  -a ARCH,..   --arches=ARCH,..           comma-separated list of arches to consider at all.
                                          Defaults to all
  -r ARCH,...  --release-arches=ARCH,...  comma-separated list of arches to consider release critical.
                                          Defaults to all
               --relaxation=FILE          print relaxation clauses to this file
               --clauses=FILE             print literate clauses to this file
               --dimacs=FILE              print SAT solver input in dimacs format to this file
               --difference=FILE          print result overview to this file
               --hints=FILE               print britney2 hints to this file
               --migrate=PKG              find a migration containing this package.
                                          If it is a source package, it ignores this package's age
               --large                    find a transition as large as possible (default)
               --small                    find a transition as small as possible (useful with --migrate)
               --many-small               find a large transition and split it into many small
                                          transitions when printing hints
               --any-size                 find any transition (slightly faster)

Instead of FILE, "-" can be used to print to the standard output.

Some useful things to do would be, for example, 
$ ./SAT-Britney -d /srv/release.debian.org/britney/var/data-b2/ \
	--hints hints.txt 
(4 minutes) to calculate what SAT-Britney assumes to be the largest
valid transition (which unfortunately is not valid, as it does not yet
parse block hints and because of the issue with Conflicts).

It is hence slightly more useful to break up the transition into
individual bits:
$ ./SAT-Britney -d /srv/release.debian.org/britney/var/data-b2/ \
	--hints hints.txt --many-small
(5 minutes) which gives multiple "easy" hints, each of which should be
able to go through on its own. The current output in the hints file
(with comments stripped) is:
easy banshee-community-extensions/2.0.1-2 zeitgeist-sharp/
easy eclipse/3.5.2-11 sat4j/2.3.0-1

And lastly it can be used to try to migrate individual packages. It will
ignore the age of the package mentioned on the command line (but not for
possible dependencies):
$ ./SAT-Britney -d /srv/release.debian.org/britney/var/data-b2/ \
	--hints hints.txt -a i386 --migrate ghc_7.0.4-4_src --small
(19 seconds) tells you that ghc cannot migrate because haskell-filestore
is too new, while 
$ ./SAT-Britney -d /srv/release.debian.org/britney/var/data-b2/ \
	--hints hints.txt -a i386 --migrate sat4j_2.3.0-1_src --small
gives the above hint about sat4j (and only that hint) in 20 seconds.

If you want to play around with it, just log onto ries:~nomeata. If you
want to play with the code, you can fetch it with
$ darcs get http://darcs.nomeata.de/sat-britney/

On #debian-release it was asked if it is easily possible to get it to
build on squeeze, but this would require quite a bit of backporting of
new packages and updating others and binNMUing of thirds. Not something
that really belongs into squeeze-backports. So what I am doing is to
build it on unstable statically (flags for that are already set in the
build configuration) and upload that. All dependencies, especially all
used the Haskell libraries, are packaged in unstable. If that is not
acceptable then it will have to stay a manual tool for local use, e.g.
to generate the hints for a large transition, until wheeze is released.


Joachim "nomeata" Breitner
Debian Developer
  nomeata@debian.org | ICQ# 74513189 | GPG-Keyid: 4743206C
  JID: nomeata@joachim-breitner.de | http://people.debian.org/~nomeata

Attachment: signature.asc
Description: This is a digitally signed message part

Reply to: