Discussion:
RFC: The Future of Solving Dependency Problems in APT (SAT, CUDF)
(too old to reply)
Julian Andres Klode
2010-12-22 17:32:20 UTC
Permalink
Hi,

as discussed on IRC; the time is ready for APT to gain some more
advanced facilities in the area of solving dependency problems.

The first file that I attach is solver.h. This outlines my proposal for
a new solver API. It contains the interface of an abstract base class
APT::Solver that provides an interface for solving changes, inspired by
discussions with some members of the community.

It shall be the base for two new classes: SatSolver and CudfSolver. The
first class implements a solver based on the boolean satisfiability
problem, the second one an interface to an external solver with data
exchange happening via the CUDF format[1]. We'd also be willing to merge
aptitude's solver into this new infrastructure if useful.

The second attachment, sat-solver.cc, is a proof of concept stand-alone
SAT solver on APT, utilizing the SAT solver 'picosat' for the actual
solving process. The version of 'picosat' in Debian is built without
trace support, if you link the program against a version with trace
support, it can tell which dependencies could not be satisfied (but it
requires a bit more memory then, mostly for storing which clause belongs
to which dependency).

I also have a proof of concept CUDF writer written in Python, but
decided that we do not really need it now (it only writes the universe
to stdout, no request). And yes, pure CUDF, no Debian-specific version
thereof.

If there are no objections, I will create a new branch, and implement a
SatSolver using picosat therein (as that's fairly easy and produces good
results). I would also like to create the CudfSolver, but I'd need a
solver to test with. If anyone knows such solvers, please write.

The following is a list of CCed persons and their relation to the
content of this email:
zack: Member of Mancoosi, proposed external solvers using CUDF
dburrows: Developer of aptitude
mt: Maintainer of picosat

All attachments to this email are provided under the terms of the MIT
license, see solver.h for further details.

[1] http://www.mancoosi.org/reports/tr3.pdf
--
Julian Andres Klode - Debian Developer, Ubuntu Member

See http://wiki.debian.org/JulianAndresKlode and http://jak-linux.org/.
Julian Andres Klode
2010-12-22 19:45:51 UTC
Permalink
Post by Julian Andres Klode
The second attachment, sat-solver.cc, is a proof of concept stand-alone
SAT solver on APT, utilizing the SAT solver 'picosat' for the actual
solving process. The version of 'picosat' in Debian is built without
trace support, if you link the program against a version with trace
support, it can tell which dependencies could not be satisfied (but it
requires a bit more memory then, mostly for storing which clause belongs
to which dependency).
Here is an update with two commands: "install" and "upgrade", and an
alphabetical output that is also cleaned up a bit for upgrades
(previously every upgrade was accompanied by a remove line for the old
version, that's gone now).
--
Julian Andres Klode - Debian Developer, Ubuntu Member

See http://wiki.debian.org/JulianAndresKlode and http://jak-linux.org/.
Stefano Zacchiroli
2010-12-23 09:09:57 UTC
Permalink
Post by Julian Andres Klode
as discussed on IRC; the time is ready for APT to gain some more
advanced facilities in the area of solving dependency problems.
I surely concur :)
Post by Julian Andres Klode
The first file that I attach is solver.h. This outlines my proposal for
a new solver API. It contains the interface of an abstract base class
APT::Solver that provides an interface for solving changes, inspired by
discussions with some members of the community.
I leave the comments on this API to the tech APT people.

However, to my recalling, there was an unsolved problem in dealing with
an external solver, namely how to discriminate between packages coming
from APT repositories and identically-looking packages which have been
possibly locally rebuilt by the user. Does your API rely on hashing of
some set of package field to generate package identifiers as the current
APT?

I believe this problem deserves a cleaner solution, but the only
solutions I can imagine require support at the dpkg level as well.
Post by Julian Andres Klode
It shall be the base for two new classes: SatSolver and CudfSolver. The
first class implements a solver based on the boolean satisfiability
problem, the second one an interface to an external solver with data
exchange happening via the CUDF format[1]. We'd also be willing to merge
aptitude's solver into this new infrastructure if useful.
<snip>
Post by Julian Andres Klode
I also have a proof of concept CUDF writer written in Python, but
decided that we do not really need it now (it only writes the universe
to stdout, no request). And yes, pure CUDF, no Debian-specific version
thereof.
I'm glad to hear this. Is the code in APT2? I'd appreciate pointers to
it to have a look. Also, I've noticed a backlog on IRC (sorry, too late
to reply to it) about some very interesting performances of your writer;
care to report them here?
Post by Julian Andres Klode
If there are no objections, I will create a new branch, and implement
a SatSolver using picosat therein (as that's fairly easy and produces
good results).
Here, are you referring to an APT branch or ...?
Post by Julian Andres Klode
I would also like to create the CudfSolver, but I'd need a solver to
test with. If anyone knows such solvers, please write.
In the Mancoosi project we do have quite some of them, coming from the
MISC 2010 competition http://www.mancoosi.org/misc-2010/ . In general,
we have two variants of each participant solver, one implementing a
"trendy" optimization strategy (try to upgrade as much packages as
possible), and another one implementing a "paranoid" strategy (try to
satisfy user request, but by changing as little packages as
possible). Mind you though, as the participants were free to use the
language they want, there's quite some Java around which is not exactly
"fast" in CUDF parsing.

I'm adding to Cc: Pietro Abate, a co-worker of mine in the Mancoosi
project. He has been one of the main organizers of the MISC competition
and he has collected the code of all participant solvers. Unfortunately
there is at least one case in which we cannot re-distribute the code of
a participating solver (it was licensed to us only for the purposes of
the competition), but all other solvers are free software. Pietro can
give you the actual code and/or point you to where the solvers are
available for download.

( Pietro: for reference the initial mail of this thread is at
http://lists.debian.org/deity/2010/12/msg00053.html )

Cheers.
--
Stefano Zacchiroli -o- PhD in Computer Science \ PostDoc @ Univ. Paris 7
zack@{upsilon.cc,pps.jussieu.fr,debian.org} -<>- http://upsilon.cc/zack/
Quando anche i santi ti voltano le spalle, | . |. I've fans everywhere
ti resta John Fante -- V. Capossela .......| ..: |.......... -- C. Adams
Julian Andres Klode
2010-12-23 11:17:07 UTC
Permalink
Post by Stefano Zacchiroli
Post by Julian Andres Klode
as discussed on IRC; the time is ready for APT to gain some more
advanced facilities in the area of solving dependency problems.
I surely concur :)
Post by Julian Andres Klode
The first file that I attach is solver.h. This outlines my proposal for
a new solver API. It contains the interface of an abstract base class
APT::Solver that provides an interface for solving changes, inspired by
discussions with some members of the community.
I leave the comments on this API to the tech APT people.
However, to my recalling, there was an unsolved problem in dealing with
an external solver, namely how to discriminate between packages coming
from APT repositories and identically-looking packages which have been
possibly locally rebuilt by the user. Does your API rely on hashing of
some set of package field to generate package identifiers as the current
APT?
The script I wrote drops duplicates currently. The right solution is to
add the version ID to the package: field and to add a provides package:

package: apt%1
provides: apt

I'm also using this trick for splitting virtual packages from real ones
like this:
package: apt
provides: virtual%packagename, virtual%apt

(each virtual package gets virtual% prepended, and also provides itself
with virtual%)- then I change all unversioned dependencies such as
"depends: apt" to "depends: virtual%apt".

In this case, I used the '%' character as that's not allowed in package
names and does not seem to be reserved in CUDF either.
Post by Stefano Zacchiroli
I believe this problem deserves a cleaner solution, but the only
solutions I can imagine require support at the dpkg level as well.
Post by Julian Andres Klode
It shall be the base for two new classes: SatSolver and CudfSolver. The
first class implements a solver based on the boolean satisfiability
problem, the second one an interface to an external solver with data
exchange happening via the CUDF format[1]. We'd also be willing to merge
aptitude's solver into this new infrastructure if useful.
<snip>
Post by Julian Andres Klode
I also have a proof of concept CUDF writer written in Python, but
decided that we do not really need it now (it only writes the universe
to stdout, no request). And yes, pure CUDF, no Debian-specific version
thereof.
I'm glad to hear this. Is the code in APT2? I'd appreciate pointers to
it to have a look. Also, I've noticed a backlog on IRC (sorry, too late
to reply to it) about some very interesting performances of your writer;
care to report them here?
It's just a simple prototype to test how I can create CUDF. I attached
the script. It defines some extra unused properties for now, but
converts predepends to depends and breaks to conflicts; so the solver
can handle them. The output is valid according to cudf-check -univ.

(I'm using a minus-dash as a seperator instead of '%' in this script,
but the '%' is clearly superior).
Post by Stefano Zacchiroli
Post by Julian Andres Klode
If there are no objections, I will create a new branch, and implement
a SatSolver using picosat therein (as that's fairly easy and produces
good results).
Here, are you referring to an APT branch or ...?
Yes.
Post by Stefano Zacchiroli
Post by Julian Andres Klode
I would also like to create the CudfSolver, but I'd need a solver to
test with. If anyone knows such solvers, please write.
In the Mancoosi project we do have quite some of them, coming from the
MISC 2010 competition http://www.mancoosi.org/misc-2010/ . In general,
we have two variants of each participant solver, one implementing a
"trendy" optimization strategy (try to upgrade as much packages as
possible), and another one implementing a "paranoid" strategy (try to
satisfy user request, but by changing as little packages as
possible). Mind you though, as the participants were free to use the
language they want, there's quite some Java around which is not exactly
"fast" in CUDF parsing.
I'm adding to Cc: Pietro Abate, a co-worker of mine in the Mancoosi
project. He has been one of the main organizers of the MISC competition
and he has collected the code of all participant solvers. Unfortunately
there is at least one case in which we cannot re-distribute the code of
a participating solver (it was licensed to us only for the purposes of
the competition), but all other solvers are free software. Pietro can
give you the actual code and/or point you to where the solvers are
available for download.
( Pietro: for reference the initial mail of this thread is at
http://lists.debian.org/deity/2010/12/msg00053.html )
Cheers.
--
Julian Andres Klode - Debian Developer, Ubuntu Member

See http://wiki.debian.org/JulianAndresKlode and http://jak-linux.org/.
Stefano Zacchiroli
2010-12-23 14:38:57 UTC
Permalink
Post by Julian Andres Klode
The script I wrote drops duplicates currently. The right solution is
to add the version ID to the package: field and to add a provides
package: apt%1
provides: apt
I'm also using this trick for splitting virtual packages from real ones
package: apt
provides: virtual%packagename, virtual%apt
I see, this does indeed address the corresponding glitch I've mentioned
in my follow-up to David.
Post by Julian Andres Klode
In this case, I used the '%' character as that's not allowed in
package names and does not seem to be reserved in CUDF either.
It is only suggested to use that for escaping (a la URL encoding), but
it doesn't indeed have any special meaning.
Post by Julian Andres Klode
It's just a simple prototype to test how I can create CUDF. I attached
the script. It defines some extra unused properties for now, but
converts predepends to depends and breaks to conflicts; so the solver
can handle them. The output is valid according to cudf-check -univ.
Nice, thanks, I'll have a look at it.

Cheers.
--
Stefano Zacchiroli -o- PhD in Computer Science \ PostDoc @ Univ. Paris 7
zack@{upsilon.cc,pps.jussieu.fr,debian.org} -<>- http://upsilon.cc/zack/
Quando anche i santi ti voltano le spalle, | . |. I've fans everywhere
ti resta John Fante -- V. Capossela .......| ..: |.......... -- C. Adams
Michael Tautschnig
2010-12-23 15:30:28 UTC
Permalink
Hi all,

Sorry for chiming in a bit late, but I'm pretty busy with real life these days
(as Pietro already knows :-) ).

[...]
It think we should look at this third category of solvers as the allow
us to specify sane optimization criteria for install and upgrades.
http://www.cs.uni-potsdam.de/wv/aspcud/
http://wiki.eclipse.org/Equinox/p2/CUDFResolver
http://sat.inesc-id.pt/~mikolas/cudf2pbo.html
http://sat.inesc-id.pt/~mikolas/cudf2msu.html
My preference is the aspcud that did pretty well in the competition and
is GPL.
[...]

If you want to go for answer set programming (ASP), then you might also want to
know that some of those solvers are currently sitting in NEW and waiting for the
ftp-master's approval, in particular gringo and clasp.

I'll keep an eye on this thread, but please don't expect too much input from my
side before end of January.

Best regards,
Michael

PS.: Please keep me CC'ed, unlike zack I'm not subscribed to ***@l.d.o
Stefano Zacchiroli
2010-12-23 15:42:41 UTC
Permalink
Post by Michael Tautschnig
If you want to go for answer set programming (ASP), then you might
also want to know that some of those solvers are currently sitting in
NEW and waiting for the ftp-master's approval, in particular gringo
and clasp.
I'm glad to hear that. In fact, this prompt me to express a more general
"platform requirement" for all this discussion. It would be a worthwhile
goal, once an interface with APT and friends is set up, to define a
common way for package shipping dependency solvers to register
themselves as alternative solvers. Ideally, the sysadm might want to
change the solver used by APT by simply specifying a configuration
option, possibly on the command line.

I understand I'm jumping the gun a bit with that, but it's something we
should keep in mind as a goal. Maintainers of (several!, hint hint)
solver packages might in fact already advance proposals on how to
declare / register solvers.

Cheers.
--
Stefano Zacchiroli -o- PhD in Computer Science \ PostDoc @ Univ. Paris 7
zack@{upsilon.cc,pps.jussieu.fr,debian.org} -<>- http://upsilon.cc/zack/
Quando anche i santi ti voltano le spalle, | . |. I've fans everywhere
ti resta John Fante -- V. Capossela .......| ..: |.......... -- C. Adams
Pietro Abate
2010-12-23 15:14:50 UTC
Permalink
Hi all,
Post by Stefano Zacchiroli
Post by Julian Andres Klode
I would also like to create the CudfSolver, but I'd need a solver to
test with. If anyone knows such solvers, please write.
In the Mancoosi project we do have quite some of them, coming from the
MISC 2010 competition http://www.mancoosi.org/misc-2010/ . In general,
we have two variants of each participant solver, one implementing a
"trendy" optimization strategy (try to upgrade as much packages as
possible), and another one implementing a "paranoid" strategy (try to
satisfy user request, but by changing as little packages as
possible). Mind you though, as the participants were free to use the
language they want, there's quite some Java around which is not exactly
"fast" in CUDF parsing.
during the latest run of the misc-live (basically the same as misc-2010
but it is not an official competition) we also opened up a third track,
the "user track" where solver were asked to optimize a given expression.

Within this track we can encode the paranoid and trendy tracks. For
example the trendy track can be given by the following optimization
function :

lex( min removed, min notuptodate, min unmet_recommends, min new)

while the paranoid track as :

lex( min removed, min changed)

It think we should look at this third category of solvers as the allow
us to specify sane optimization criteria for install and upgrades.

GPL solver :
http://www.cs.uni-potsdam.de/wv/aspcud/

Eclipse licence :
http://wiki.eclipse.org/Equinox/p2/CUDFResolver

Non free solvers :( but we have the right to redistribute them :
http://sat.inesc-id.pt/~mikolas/cudf2pbo.html
http://sat.inesc-id.pt/~mikolas/cudf2msu.html

My preference is the aspcud that did pretty well in the competition and
is GPL.

It is important to notice, that picosat will be able to tell you a
solution, but probably it won't be a good one. These solvers should be
able to tell you the best solution accordingly to given objective
function.

I've also written a python prototype (mpm.py) available here as zack
mentioned :
http://gforge.info.ucl.ac.be/plugins/scmsvn/viewcvs.php/trunk/updb/mpm/?root=mancoosi

It uses a couple of external binaries to convert Packages to Cudf, but I
think we would easily integrate your script to do the job. Something
else that is left to do it to update the status file once the package is
installed... If you just want to check the solver part and run it as
normal user, you can just comment out the "commit" part. I think this
can be a nice starting point to play and settle on a correct level of
abstraction for the API.

A small whish item since we are here: can we also expose the function
that computes the installation order. It would be nice to somehow
formalize this algorithm and let the "user" access the list in some
other way then throught a debugging option...

hope this helps.

p
--
----
http://en.wikipedia.org/wiki/Posting_style
--
To UNSUBSCRIBE, email to deity-***@lists.debian.org
with a subject of "unsubscribe". Trouble? Contact ***@lists.debian.org
Archive: http://lists.debian.org/***@uranium.pps.jussieu.fr
Julian Andres Klode
2010-12-23 16:09:23 UTC
Permalink
Post by Pietro Abate
It is important to notice, that picosat will be able to tell you a
solution, but probably it won't be a good one. These solvers should be
able to tell you the best solution accordingly to given objective
function.
picosat allows us to specify a lot of things, like keeping installed
packages if possible, or preferring candidate versions over
non-candidate ones. In my tests, it created wonderful solutions.
Post by Pietro Abate
A small whish item since we are here: can we also expose the function
that computes the installation order. It would be nice to somehow
formalize this algorithm and let the "user" access the list in some
other way then throught a debugging option...
Different part of APT.
--
Julian Andres Klode - Debian Developer, Ubuntu Member

See http://wiki.debian.org/JulianAndresKlode and http://jak-linux.org/.
--
To UNSUBSCRIBE, email to deity-***@lists.debian.org
with a subject of "unsubscribe". Trouble? Contact ***@lists.debian.org
Archive: http://lists.debian.org/***@jak-thinkpad
Julian Andres Klode
2010-12-24 11:53:15 UTC
Permalink
Post by Pietro Abate
A small whish item since we are here: can we also expose the function
that computes the installation order. It would be nice to somehow
formalize this algorithm and let the "user" access the list in some
other way then throught a debugging option...
The installation order is done by class pkgOrderList in
apt-pkg/orderlist.cc and is a container that you can order, and the
ordering appears to be complicated (1100 lines total, 695 SLOC) and
AFAIK also has some problems. If we can improve this situation, I would
be happy.
--
Julian Andres Klode - Debian Developer, Ubuntu Member

See http://wiki.debian.org/JulianAndresKlode and http://jak-linux.org/.
--
To UNSUBSCRIBE, email to deity-***@lists.debian.org
with a subject of "unsubscribe". Trouble? Contact ***@lists.debian.org
Archive: http://lists.debian.org/***@jak-thinkpad
David Kalnischkies
2011-01-05 11:26:20 UTC
Permalink
Post by Julian Andres Klode
Post by Pietro Abate
A small whish item since we are here: can we also expose the function
that computes the installation order. It would be nice to somehow
formalize this algorithm and let the "user" access the list in some
other way then throught a debugging option...
The installation order is done by class pkgOrderList in
apt-pkg/orderlist.cc and is a container that you can order, and the
ordering appears to be complicated (1100 lines total, 695 SLOC) and
AFAIK also has some problems. If we can improve this situation, I would
be happy.
Your are not the only one. I had a lot of "fun" with it already and
Michael is a big fan of it, too. In theory that is something dpkg should
do as it has superior knowledge (e.g. which maintainer script exists for
loop unbreaking) but stuff like #526774 doesn't help in making it less
complicated…


Best regards

David Kalnischkies
--
To UNSUBSCRIBE, email to deity-***@lists.debian.org
with a subject of "unsubscribe". Trouble? Contact ***@lists.debian.org
Archive: http://lists.debian.org/AANLkTikngwSQMHMMoHE7tkRXUv6ja2pFh+***@mail.gmail.com
David Kalnischkies
2010-12-23 12:47:59 UTC
Permalink
Ho, ho, ho all :)
Post by Julian Andres Klode
as discussed on IRC; the time is ready for APT to gain some more
advanced facilities in the area of solving dependency problems.
(as said on IRC, i am a bit low on time, but some comments anyway)
Post by Julian Andres Klode
The first file that I attach is solver.h. This outlines my proposal for
a new solver API. It contains the interface of an abstract base class
APT::Solver that provides an interface for solving changes, inspired by
discussions with some members of the community.
Passing a depCache into an abstract resolver seems a bit strange as
it is the key part of the internal APT resolver including a lot of stuff which
will properly not be used by another resolver (okay, aptitude, but picosat?),
e.g. State of dependencies, autoremove flags and so on.

What we want is exporting only the pkgCache to the resolver to save them
from the hassle of parsing the Packages files on their own. Resolvers who
can handle a pkgCache will be happy, others need an intermediate level to
reformat it to some other format (e.g. {C,D}UDF).
(thinking of pkgCache as a really big {Package,Version}Set)

Further more, i would like to have a Hold(VersionSet) to tell the resolver
e.g. about dpkg holds and maybe even a Keep(PackageSet) to tell the
resolver to never remove this set of packages (but upgrade is fine) which
could be handy for essentials and co.

In return i would expect a set of versions of packages to install and to
remove.

Solver::Rules is a mystery for me. Most complains about the resolver in
APT evolve from the fact that it doesn't switch candidate versions if it
has to (the popular car v2 with wheels v3 and v2 example comes to mind).
How to transport the meaning of candidate after all?
For me, candidate is an (important) implementation detail of the APT resolver.
Another resolver should be able to choose freely if he wants to put on wheel
v3 or v2 and therefore doesn't need a concept of candidate version.

I would say that every version i tell the solver about should be a candidate
for him to choose from -- why should i tell him about versions i don't want
in the first place after all? So in the end pkgCache is maybe the wrong
choice and we should give the solver a (big) VersionSet as problem space.

The problem with these multiple candidates would be that while an experimental
package can be a candidate, if at all possible stable should be preferred
which leads us to think about how we exposure pkgPolicy to the resolver world.
Wasn't in an old thread yet-another-description language mentioned for
exactly this task?
Post by Julian Andres Klode
It shall be the base for two new classes: SatSolver and CudfSolver. The
first class implements a solver based on the boolean satisfiability
problem, the second one an interface to an external solver with data
exchange happening via the CUDF format[1]. We'd also be willing to merge
aptitude's solver into this new infrastructure if useful.
I would divide Solvers into Internal (i can pass pkgCache/VersionSet directly
into it) and External (i need to reformat pkgCache/VersionSet) and subclass
it for {D,C}UDF and maybe other formats of other resolvers.
After all, how a solver solves isn't really interesting for the implementation
of an interface to it - and hard to define or in what category belongs
APT/aptitude?
Beside that a CUDFSolver could be a SATSolver internally (noone forbids
writing a picosat solver based on cudf data)…
Post by Julian Andres Klode
The second attachment, sat-solver.cc, is a proof of concept stand-alone
SAT solver on APT, utilizing the SAT solver 'picosat' for the actual
solving process. The version of 'picosat' in Debian is built without
trace support, if you link the program against a version with trace
support, it can tell which dependencies could not be satisfied (but it
requires a bit more memory then, mostly for storing which clause belongs
to which dependency).
If i see it correctly your proof of concept doesn't use the depCache -
beside for the sake of simulating more what APT does - so that would
be a proof by experiment for my theory above. :)

Integrating the proof into apt-get directly should be relatively simple but i
would like to see the abstraction to be in first so that APT doesn't need to
be linked against picosat (and all the others which will come maybe).
Some sort of plugin system maybe…
The version system (and a bit of other stuff) in APT has some sort of
built-in plugin system, if we could make that more dynamic…
(yes, i am dreaming a bit now)
Post by Julian Andres Klode
I also have a proof of concept CUDF writer written in Python, but
decided that we do not really need it now (it only writes the universe
to stdout, no request). And yes, pure CUDF, no Debian-specific version
thereof.
You forgot in your implementation that Debian has a lot of implicit
dependencies (or conflicts if you like) as it doesn't allow two different
version of the same package to be installed (minor, but to consider)
and i think there were other obstacles mentioned in the older threads
which make it helpful at least to use a debian specific format if possible,
but i am not sure and again i can't find it right now.
Post by Julian Andres Klode
If there are no objections, I will create a new branch, and implement a
SatSolver using picosat therein (as that's fairly easy and produces good
results). I would also like to create the CudfSolver, but I'd need a
solver to test with. If anyone knows such solvers, please write.
Regarding picosat, feel free to go on, i am interested to see what will
happen and it could "simplify" abstraction if we have two solvers to
"hide" under a common interface instead of just the APT beast as we
have only one try to get it right before the front-ends will (ab)use it…

On the other hand, i would like to claim CUDF for me as i am currently
in the process of setting up a stay at "mancoosi headquarter" around
April to work on teaching APT how to read/write CUDF and doing
something meaningful in between. :)


After all an interesting year 2011 is upcoming, but until then:
Merry package management days… -uh, i mean Christmas :)

David
--
To UNSUBSCRIBE, email to deity-***@lists.debian.org
with a subject of "unsubscribe". Trouble? Contact ***@lists.debian.org
Archive: http://lists.debian.org/AANLkTimjs6BJSN229eVXULb=***@mail.gmail.com
Julian Andres Klode
2010-12-23 14:19:55 UTC
Permalink
Post by David Kalnischkies
Ho, ho, ho all :)
Post by Julian Andres Klode
as discussed on IRC; the time is ready for APT to gain some more
advanced facilities in the area of solving dependency problems.
(as said on IRC, i am a bit low on time, but some comments anyway)
Post by Julian Andres Klode
The first file that I attach is solver.h. This outlines my proposal for
a new solver API. It contains the interface of an abstract base class
APT::Solver that provides an interface for solving changes, inspired by
discussions with some members of the community.
Passing a depCache into an abstract resolver seems a bit strange as
it is the key part of the internal APT resolver including a lot of stuff which
will properly not be used by another resolver (okay, aptitude, but picosat?),
e.g. State of dependencies, autoremove flags and so on.
What we want is exporting only the pkgCache to the resolver to save them
from the hassle of parsing the Packages files on their own. Resolvers who
can handle a pkgCache will be happy, others need an intermediate level to
reformat it to some other format (e.g. {C,D}UDF).
(thinking of pkgCache as a really big {Package,Version}Set)
Further more, i would like to have a Hold(VersionSet) to tell the resolver
e.g. about dpkg holds and maybe even a Keep(PackageSet) to tell the
resolver to never remove this set of packages (but upgrade is fine) which
could be handy for essentials and co.
We do not really need hold, that's completely identical to marking the
package for installation, although it might be useful just for the
semantics. Does Keep(PackageSet) work with multi-arch where an install
pkg:all becomes architecture-dependent? I merged the changes into the
header.
Post by David Kalnischkies
In return i would expect a set of versions of packages to install and to
remove.
That's what Solve() gives you.
Post by David Kalnischkies
Solver::Rules is a mystery for me. Most complains about the resolver in
APT evolve from the fact that it doesn't switch candidate versions if it
has to (the popular car v2 with wheels v3 and v2 example comes to mind).
How to transport the meaning of candidate after all?
For me, candidate is an (important) implementation detail of the APT resolver.
Another resolver should be able to choose freely if he wants to put on wheel
v3 or v2 and therefore doesn't need a concept of candidate version.
I removed all options except for the candidate one (which I switched,
it's IGNORE_CANDIDATE_STATUS now), and the one for ignoring conflicts;
as the latter one is really useful for building Debian images - for
example, debimg has it's own solver mainly in order to ignore conflicts.
Post by David Kalnischkies
I would say that every version i tell the solver about should be a candidate
for him to choose from -- why should i tell him about versions i don't want
in the first place after all? So in the end pkgCache is maybe the wrong
choice and we should give the solver a (big) VersionSet as problem space.
No. VersionSet costs too much space from my experience. That's one
reason why I use mostly sets of pointers in my sat-solver prototype
(made multiple MB difference or something like that) - possibly because
it's a binary tree and allocates empty iterator objects for unused
nodes.
Post by David Kalnischkies
The problem with these multiple candidates would be that while an experimental
package can be a candidate, if at all possible stable should be preferred
which leads us to think about how we exposure pkgPolicy to the resolver world.
Wasn't in an old thread yet-another-description language mentioned for
exactly this task?
The current prototype prefers candidate versions of packages over
non-candidate versions. That is a sane choice in my opinion. I chose to
use pkgDepCache because it brings a cache and a GetCandidateVer(), but
we don't really need it and can use:

Solver(pkgCache &cache, pkgPolicy &policy, unsigned int rules = 0);

instead.
Post by David Kalnischkies
Post by Julian Andres Klode
It shall be the base for two new classes: SatSolver and CudfSolver. The
first class implements a solver based on the boolean satisfiability
problem, the second one an interface to an external solver with data
exchange happening via the CUDF format[1]. We'd also be willing to merge
aptitude's solver into this new infrastructure if useful.
I would divide Solvers into Internal (i can pass pkgCache/VersionSet directly
into it) and External (i need to reformat pkgCache/VersionSet) and subclass
it for {D,C}UDF and maybe other formats of other resolvers.
After all, how a solver solves isn't really interesting for the implementation
of an interface to it - and hard to define or in what category belongs
APT/aptitude?
All solvers need to reformat the problem. The CUDF solver transfers it
to CUDF, the SAT solvers translate everything to CNF. Both takes more
time than solving the problem itself (200 ms for the picosat solver). I
don't think we need to differentiate between Internal and External
solvers within the class hierarchy.
Post by David Kalnischkies
Beside that a CUDFSolver could be a SATSolver internally (noone forbids
writing a picosat solver based on cudf data)

I know, I want to write a CUDF solver using picosat. But a CUDF solver
is named CudfSolver because it talks using CUDF.
Post by David Kalnischkies
Post by Julian Andres Klode
The second attachment, sat-solver.cc, is a proof of concept stand-alone
SAT solver on APT, utilizing the SAT solver 'picosat' for the actual
solving process. The version of 'picosat' in Debian is built without
trace support, if you link the program against a version with trace
support, it can tell which dependencies could not be satisfied (but it
requires a bit more memory then, mostly for storing which clause belongs
to which dependency).
If i see it correctly your proof of concept doesn't use the depCache -
beside for the sake of simulating more what APT does - so that would
be a proof by experiment for my theory above. :)
It uses GetCandidateVer(), but that just forwards the call to pkgPolicy,
so yes, it's useless.
Post by David Kalnischkies
Integrating the proof into apt-get directly should be relatively simple but i
would like to see the abstraction to be in first so that APT doesn't need to
be linked against picosat (and all the others which will come maybe).
Some sort of plugin system maybe

The version system (and a bit of other stuff) in APT has some sort of
built-in plugin system, if we could make that more dynamic

(yes, i am dreaming a bit now)
Dynamically loading solvers is a bit more complicated and it's easier to
link it in. We still have external solvers using CUDF for other cases.
Post by David Kalnischkies
Post by Julian Andres Klode
I also have a proof of concept CUDF writer written in Python, but
decided that we do not really need it now (it only writes the universe
to stdout, no request). And yes, pure CUDF, no Debian-specific version
thereof.
You forgot in your implementation that Debian has a lot of implicit
dependencies (or conflicts if you like) as it doesn't allow two different
version of the same package to be installed (minor, but to consider)
and i think there were other obstacles mentioned in the older threads
which make it helpful at least to use a debian specific format if possible,
but i am not sure and again i can't find it right now.
Self-conflicts are added in lines 93-94. I took care of all things
listed at <http://www.mancoosi.org/cudf/debian/>.
Post by David Kalnischkies
Post by Julian Andres Klode
If there are no objections, I will create a new branch, and implement a
SatSolver using picosat therein (as that's fairly easy and produces good
results). I would also like to create the CudfSolver, but I'd need a
solver to test with. If anyone knows such solvers, please write.
Regarding picosat, feel free to go on, i am interested to see what will
happen and it could "simplify" abstraction if we have two solvers to
"hide" under a common interface instead of just the APT beast as we
have only one try to get it right before the front-ends will (ab)use it

On the other hand, i would like to claim CUDF for me as i am currently
in the process of setting up a stay at "mancoosi headquarter" around
April to work on teaching APT how to read/write CUDF and doing
something meaningful in between. :)
I thought mancoosi ends in February - the website states "The project
has started February 1st, 2008, and will have a duration of 3 years.".

Would you license your solution under the LGPL-2.1+ then, so I can
incorporate it in the APT2 project as well? OK, I already have most of
what I need locally, but I like sharing stuff.
Post by David Kalnischkies
Merry package management days
 -uh, i mean Christmas :)
I am attaching the updated proposal. Maybe we should make this whole
class internal as APT::SolverImpl and expose a real class APT::Solver in
the public API that creates an APT::SolverImpl and forwards method calls
to it - that's very efficient in terms of ABI stability, and we would
get a nice constructor like:

Solver(string name, pkgCache cache, pkgPolicy policy);

(replace objects with constant references to them)
--
Julian Andres Klode - Debian Developer, Ubuntu Member

See http://wiki.debian.org/JulianAndresKlode and http://jak-linux.org/.
Stefano Zacchiroli
2010-12-23 14:45:45 UTC
Permalink
Post by Julian Andres Klode
Post by David Kalnischkies
On the other hand, i would like to claim CUDF for me as i am currently
in the process of setting up a stay at "mancoosi headquarter" around
April to work on teaching APT how to read/write CUDF and doing
something meaningful in between. :)
I thought mancoosi ends in February - the website states "The project
has started February 1st, 2008, and will have a duration of 3 years.".
I'm flattered about how much you folks know about the project :-)

That said, the project has been extended 6 months (and thanks for
noticing that we need to mention that on the homepage!). ... but the
actual end date of the project doesn't matter much for us. We have
opened up a research center called IRILL (http://www.irill.org); the
"Mancoosi group" which is hosted there is interested in dependency
solving issues and is also interested in working/helping the
communities, with a love for Debian which is difficult to hide. So, no
matter the actual end date, we'll have people working on dependency
solving issues.

Cheers.
--
Stefano Zacchiroli -o- PhD in Computer Science \ PostDoc @ Univ. Paris 7
zack@{upsilon.cc,pps.jussieu.fr,debian.org} -<>- http://upsilon.cc/zack/
Quando anche i santi ti voltano le spalle, | . |. I've fans everywhere
ti resta John Fante -- V. Capossela .......| ..: |.......... -- C. Adams
David Kalnischkies
2011-01-05 11:21:44 UTC
Permalink
Post by Julian Andres Klode
Post by David Kalnischkies
Further more, i would like to have a Hold(VersionSet) to tell the resolver
e.g. about dpkg holds and maybe even a Keep(PackageSet) to tell the
resolver to never remove this set of packages (but upgrade is fine) which
could be handy for essentials and co.
We do not really need hold, that's completely identical to marking the
package for installation, although it might be useful just for the
semantics.
Install request can be unversioned, but yes, holds could be mapped to
versioned install requests, but i can think of solvers who would like to
have this separation available - aptitude for example can propose solutions
in which (one) package is requested but not installed. It would be bad
if it would ignore holds this way (maybe it also wants to do this, but
give it a different score, who knows).
Post by Julian Andres Klode
Does Keep(PackageSet) work with multi-arch where an install
pkg:all becomes architecture-dependent? I merged the changes into the
header.
I think i don't understand what you mean. "My" APT implementation "just"
creates a bunch of pseudo-versions which are architecture-dependent
and depend themselves on pkg:all which caries mostly the installation
state of the package. If i want to keep such an all package, fine, i can
even say that i want to keep an pkg:any package - it just doesn't make
a lot of sense without marking the "real" pkg:all, too, as a remove will
effect both… This way a change from :all to :any and vise versa is just a
matter of a new version with different dependencies -- but this is a trick
to avoid modifying great heaps of the resolver. A resolver working on his
own datastructure (as e.g. a cudf based one) doesn't need to know about
these pseudo-versions: the solver needs to implement his own tricks to
cope with MultiArch…

I think of keep() mostly useful for situation i know beforehand that a
solution including the remove of these packages is unacceptable,
e.g. is the remove of the xserver on a desktop machine not the best
thing a package manager could do on dist-upgrade even if this means to
remove even more (but less important) packages - i imagine the API
breaking X12 upload breaking every possible x application as an
exaggerated example (maybe even more clear if you add 'unattended'
to the situation).
Post by Julian Andres Klode
Post by David Kalnischkies
In return i would expect a set of versions of packages to install and to
remove.
That's what Solve() gives you.
Ah, my mistake, i overlooked the & and thought the sets are the request…
SolveAndSet() gave the impression that the result is a modified depCache.
Post by Julian Andres Klode
Post by David Kalnischkies
Solver::Rules is a mystery for me. Most complains about the resolver in
APT evolve from the fact that it doesn't switch candidate versions if it
has to (the popular car v2 with wheels v3 and v2 example comes to mind).
How to transport the meaning of candidate after all?
For me, candidate is an (important) implementation detail of the APT resolver.
Another resolver should be able to choose freely if he wants to put on wheel
v3 or v2 and therefore doesn't need a concept of candidate version.
I removed all options except for the candidate one (which I switched,
it's IGNORE_CANDIDATE_STATUS now), and the one for ignoring conflicts;
as the latter one is really useful for building Debian images - for
example, debimg has it's own solver mainly in order to ignore conflicts.
Post by David Kalnischkies
I would say that every version i tell the solver about should be a candidate
for him to choose from -- why should i tell him about versions i don't want
in the first place after all? So in the end pkgCache is maybe the wrong
choice  and we should give the solver a (big) VersionSet as problem space.
No. VersionSet costs too much space from my experience. That's one
reason why I use mostly sets of pointers in my sat-solver prototype
(made multiple MB difference or something like that) - possibly because
it's a binary tree and allocates empty iterator objects for unused
nodes.
Yeah, i thought more of concept wise, not implementation wise.
And VersionSet implementation is by far not optimal yet - i wonder what
would happen if it would use something like c++0x std::unordered_set instead
of the ordered std::set for example. The sets were mostly created to pass
around packages and versions while parsing the commandline and these requests
are much smaller than a package universe can be and therefore not optimized.
Post by Julian Andres Klode
Post by David Kalnischkies
The problem with these multiple candidates would be that while an experimental
package can be a candidate, if at all possible stable should be preferred
which leads us to think about how we exposure pkgPolicy to the resolver world.
Wasn't in an old thread yet-another-description language mentioned for
exactly this task?
The current prototype prefers candidate versions of packages over
non-candidate versions. That is a sane choice in my opinion. I chose to
use pkgDepCache because it brings a cache and a GetCandidateVer(), but
What i really want to transport with this sentence (and a few more) was that
there is no general concept of a 'candidate'. A resolver can choose whatever
version he wants as a candidate for his own.
Fine if your resolver wants to use the same as the APT resolver
(at least as a hint) but after all many resolvers will not care for a
concept of a single candidate -- they may work in a "all versions i know
about are candidates" fashion and just want to know which version they
should choose if they have an option:

Thats why i thought about modifying the universe in APT and only pass
possibly a subset to the solver: If the user for example has a negative pin
for a version - why should it be exposed to the solver? There are other
possible hard constraints that APT could do directly for all solvers so
these can focus on the soft constraints there we have a choice…
(user doesn't want gnome packages installed (APT) vs. user prefers
KDE packages if at all possible (solver))
Post by Julian Andres Klode
Post by David Kalnischkies
Post by Julian Andres Klode
It shall be the base for two new classes: SatSolver and CudfSolver. The
first class implements a solver based on the boolean satisfiability
problem, the second one an interface to an external solver with data
exchange happening via the CUDF format[1]. We'd also be willing to merge
aptitude's solver into this new infrastructure if useful.
I would divide Solvers into Internal (i can pass pkgCache/VersionSet directly
into it) and External (i need to reformat pkgCache/VersionSet) and subclass
it for {D,C}UDF and maybe other formats of other resolvers.
After all, how a solver solves isn't really interesting for the implementation
of an interface to it - and hard to define or in what category belongs
APT/aptitude?
All solvers need to reformat the problem. The CUDF solver transfers it
to CUDF, the SAT solvers translate everything to CNF. Both takes more
time than solving the problem itself (200 ms for the picosat solver). I
don't think we need to differentiate between Internal and External
solvers within the class hierarchy.
Not all. The APT resolver works directly on the pkgCache - as well as
aptitude does. The main point was more that there is no general SatSolver
as i doubt picosat works on the same datastructure as another solver -
in this case it maybe is CNF rather than a Sat classification through -, but
pkgCache, depCache and {C,D}UDF are datastructures, some are build
anyway (pkgCache), some not (CUDF), while APT starts up.

Regarding speed, we can cache CUDF transformation results too at both ends
of the process and after all:
a) if a cudf solver performs good it shouldn't be to hard to make it work
directly on pkgCache instead/too
b) is speed not the biggest concern. I can wait a while for the calculation
as long as the result is a good one…
Post by Julian Andres Klode
Post by David Kalnischkies
Integrating the proof into apt-get directly should be relatively simple but i
would like to see the abstraction to be in first so that APT doesn't need to
be linked against picosat (and all the others which will come maybe).
Some sort of plugin system maybe…
The version system (and a bit of other stuff) in APT has some sort of
built-in plugin system, if we could make that more dynamic…
(yes, i am dreaming a bit now)
Dynamically loading solvers is a bit more complicated and it's easier to
link it in. We still have external solvers using CUDF for other cases.
Sure is linking in easier, but i doubt there exists a "one size fits all"
solver for all usecases. APT for example has proven again to work better in
a non-interactive fashion as required in a dist-upgrade while aptitude is the
king of interactive package management, but failing big time in converting
a lenny into a squeeze installation if we trust the drafted release notes.
They all currently are not perfect for sbuild usage…

While the user interface shouldn't change too much between different
usecases i am pretty sure we will need to provide different solvers for
different actions - at least install, (dist-)upgrade, build-dep and
autoremove… beside that different usergroups may have different
solvergroups satisfying there needs…

Thats also why i would like to keep the current APT solver as the fallback
as it performs okay for many years now and would like to have all the new
and shine resolvers as optional (but recommend) alternative.


Best regards

David Kalnischkies
--
To UNSUBSCRIBE, email to deity-***@lists.debian.org
with a subject of "unsubscribe". Trouble? Contact ***@lists.debian.org
Archive: http://lists.debian.org/AANLkTimzXOvnUg16sBzzWo5z6cNjxD74uh-XTu9mmc+***@mail.gmail.com
Stefano Zacchiroli
2010-12-23 14:36:30 UTC
Permalink
Post by David Kalnischkies
Solver::Rules is a mystery for me. Most complains about the resolver in
APT evolve from the fact that it doesn't switch candidate versions if it
has to (the popular car v2 with wheels v3 and v2 example comes to mind).
How to transport the meaning of candidate after all?
For me, candidate is an (important) implementation detail of the APT resolver.
Another resolver should be able to choose freely if he wants to put on wheel
v3 or v2 and therefore doesn't need a concept of candidate version.
If I read you correctly, this is indeed one of the reasons from which
APT incompleteness (i.e. the inability to find a solution to a
dependency problem where one does exist). I concur that it should not be
promoted from an APT's solver implementation detail to a part of the
problem description. Doing so will seriously undermine the room of
improvement to dependency solving capabilities that an external solver
could contribute.
Post by David Kalnischkies
The problem with these multiple candidates would be that while an
experimental package can be a candidate, if at all possible stable
should be preferred which leads us to think about how we exposure
pkgPolicy to the resolver world. Wasn't in an old thread
yet-another-description language mentioned for exactly this task?
Yes, but it ain't easy to find the good balance in designing such a
language. That is why for our competition we have decided, for the
moment, to have different tracks where solvers have optimized different
strategies.

The challenge ahead of us for an external solver is deciding which, of
current APT behavior, is part of the problem description
(i.e. constraint that cannot be violated) and which are not. Those who
are not can then be expressed as optimization criteria that external
solver will be required to address.

For instance, the one about experimental will most likely become a hard
constraint, while other aspects (e.g. installation of Recommends) can
become soft constraints that the solvers will have to optimize.
Post by David Kalnischkies
I would divide Solvers into Internal (i can pass pkgCache/VersionSet
directly into it) and External (i need to reformat
pkgCache/VersionSet) and subclass it for {D,C}UDF and maybe other
formats of other resolvers. After all, how a solver solves isn't
really interesting for the implementation of an interface to it - and
hard to define or in what category belongs APT/aptitude? Beside that
a CUDFSolver could be a SATSolver internally (noone forbids writing a
picosat solver based on cudf data)

As a matter of fact, we already have solvers CUDF solvers based on a
wide range of techniques, including: SAT, MaxSAT, PBO (Pseudo Boolean
Optimization), ASP (Answer Set Programming), and
zecret-proprietary-stuff. The results we have up to know show that no
one-size-does-fit-all solution is better than the others in all the
scenarios we have tested so far. While on one hand this might be seen as
depressing, on the other hand it is a motivation for not committing to
any specific technique, even if only in the name.
Post by David Kalnischkies
You forgot in your implementation that Debian has a lot of implicit
dependencies (or conflicts if you like) as it doesn't allow two
different version of the same package to be installed (minor, but to
consider) and i think there were other obstacles mentioned in the
older threads which make it helpful at least to use a debian specific
format if possible, but i am not sure and again i can't find it right
now.
There are a couple of glitches in getting the conversion right. One is
the one you mention about implicit conflicts (which should be made
explicit, as dependency problems coming from other distros---most
notably those RPM-based---do not have them). Another one is the
disambiguation of package names which appear both as virtual and as
non-virtual packages, as the policy requires to treat them differently
when it comes to versioned dependencies.

Cheers.

PS I'm subscribed to ***@lists.d.o, feel free to drop an explicit Cc
to me when following up
--
Stefano Zacchiroli -o- PhD in Computer Science \ PostDoc @ Univ. Paris 7
zack@{upsilon.cc,pps.jussieu.fr,debian.org} -<>- http://upsilon.cc/zack/
Quando anche i santi ti voltano le spalle, | . |. I've fans everywhere
ti resta John Fante -- V. Capossela .......| ..: |.......... -- C. Adams
Julian Andres Klode
2010-12-24 12:08:29 UTC
Permalink
Post by David Kalnischkies
Integrating the proof into apt-get directly should be relatively simple but i
would like to see the abstraction to be in first so that APT doesn't need to
be linked against picosat (and all the others which will come maybe).
Some sort of plugin system maybe…
The version system (and a bit of other stuff) in APT has some sort of
built-in plugin system, if we could make that more dynamic…
(yes, i am dreaming a bit now)
OK, currently it's linked in, but here's an idea:

(1) Create Dir::Bin::Solvers = /usr/lib/apt/solvers/
(2) Files in this directory and ending with .so are modules
(3) Other files in this directory are executables using CUDF

Every module has a function getSolver() returning a new solver.
--
Julian Andres Klode - Debian Developer, Ubuntu Member

See http://wiki.debian.org/JulianAndresKlode and http://jak-linux.org/.
--
To UNSUBSCRIBE, email to deity-***@lists.debian.org
with a subject of "unsubscribe". Trouble? Contact ***@lists.debian.org
Archive: http://lists.debian.org/***@jak-thinkpad
Julian Andres Klode
2010-12-23 17:50:21 UTC
Permalink
Post by Julian Andres Klode
If there are no objections, I will create a new branch, and implement a
SatSolver using picosat therein (as that's fairly easy and produces good
results). I would also like to create the CudfSolver, but I'd need a
solver to test with. If anyone knows such solvers, please write.
I pushed the branch to bzr+ssh://bzr.debian.org/bzr/apt/apt/solver/, and
uploaded 0.8.10+expnewsolvers1 to experimental. It uses the SAT solver
for install, remove, upgrade, dist-upgrade, but it can currently not
handle unsatisfiable upgrades correctly (that is, it currently does not
hold an upgrade back if it is impossible) - use with caution. And it may
destroy detection of automatically installed packages.
--
Julian Andres Klode - Debian Developer, Ubuntu Member

See http://wiki.debian.org/JulianAndresKlode and http://jak-linux.org/.
--
To UNSUBSCRIBE, email to deity-***@lists.debian.org
with a subject of "unsubscribe". Trouble? Contact ***@lists.debian.org
Archive: http://lists.debian.org/***@jak-thinkpad
Julian Andres Klode
2010-12-28 13:14:16 UTC
Permalink
Post by Julian Andres Klode
Post by Julian Andres Klode
If there are no objections, I will create a new branch, and implement a
SatSolver using picosat therein (as that's fairly easy and produces good
results). I would also like to create the CudfSolver, but I'd need a
solver to test with. If anyone knows such solvers, please write.
I pushed the branch to bzr+ssh://bzr.debian.org/bzr/apt/apt/solver/, and
uploaded 0.8.10+expnewsolvers1 to experimental. It uses the SAT solver
for install, remove, upgrade, dist-upgrade, but it can currently not
handle unsatisfiable upgrades correctly (that is, it currently does not
hold an upgrade back if it is impossible) - use with caution. And it may
destroy detection of automatically installed packages.
I am using this version on my main system, and that's helpful in
measuring the quality of standard tasks, where it performed almost as
good as aptitude and on the average, better than standard APT. On
non-standard tasks like solving sudokus[1], it performs better than
aptitude. I pushed a fix into bzr that makes partial upgrades possible,
by keeping back impossible changes. The following is a report on the bzr
version.

[1]
http://algebraicthunk.net/~dburrows/blog/entry/package-management-sudoku/

======
Report
======

Behaviour
=========
Fully Working:
* apt-get upgrade
* apt-get install -f

Partially working:
* apt-get install
* Bug: Too Conservative. Installing mysql-server with
-texperimental will choose the mysql-server-5.1 from
unstable if libmysqlclient is already installed, because
this requires no upgrade of the installed package.
* Maybe Bug: Prefers removals over upgrades. Upgrading
nautilus to experimental causes removal of nautilus-dbg,
rather than an upgrade. Can be solved by adding package
sets to 'upgrade'.
* apt-get dist-upgrade
* Might remove every package instead of ignoring an
update. At least if you do apt-get dist-upgrade -t
experimental. We might need to keep() (manually)
installed packages first, and remove the keep() if the
user asks for it, instead of allowing the solver to do
what it wants with installed packages.

Programming interface
=====================
As it turns out, the current set of actions (install, remove, automatic)
is not enough. I propose to add two new VersionSets, 'upgrade', being
identical to 'install' in terms of the end result, but better from a
semantic point of view and easier to output; and 'keep' which is a set
of changes that were not done.

Secondly, we may want to have an interactive solver like aptitude. For
this, I propose a class APT::Solver::Helper, that contains callbacks for
various events. My current local prototype looks like this:

+
+ struct Helper {
+ /**
+ * \brief Callback invoked when a solution has been found.
+ *
+ * Represents the solution to the user and asks for confirmation
+ * of the solution. If the user does not want the solution, another
+ * solution may be found or the solver may end without a solution.
+ *
+ * \param install Packages that will be installed
+ * \param remove Packages that will be removed
+ * \param keep If the complete request cannot be satisfied, a set of
+ * packages that will not be changed.
+ * \return true if the user accepts the solution, false otherwise.
+ */
+ virtual bool Accept(const VersionSet &upgrade,
+ const VersionSet &install,
+ const VersionSet &remove,
+ const VersionSet &keep) = 0;
+ };

SatSolver bugs: Keep()
======================
Rules added by Keep() are preserved between multiple Solve() calls; that
is, the following clause is added:

Keep(P) = (P_1 | P_2 | ... |P_n)

We do not want this, as we want to allow the user to choose to remove a
package later on. Thus I propose we change this to:

Keep(P) = (-P | P_1 | P_2 | ... | P_n )

Where P is the literal describing the package and P_1..P_n are the
literals describing the package versions. This allows us to assume(P)
when solving and just stop assuming it in case we want to allow its
removal later on. In pseudo(maths+C):

P = lit(package) = cache.HeaderP->VersionCount + package->ID + 1;
P_i = lit(version) = version->ID + 1;

Meaning: The IDs of versions start at 1 and end at VersionCount. The IDs
for packages start at VersionCount + 1 and end at VersionCount +
PackageCount.

External issues
===============
* picosat is built without tracing support (Bug#607943)
* picosat prefers B in A | B if B > A (higher version ID wins)
* picosat does not allow for optional clauses, Recommends are thus
treated as Depends. I should ask them if they are interested in
adding this.

The future
==========
* Trying more solvers: clasp, minisat
* Replacing and deprecating pkgProblemSolver
* Interface for dynamically loading solvers at run-time
--
Julian Andres Klode - Debian Developer, Ubuntu Member

See http://wiki.debian.org/JulianAndresKlode and http://jak-linux.org/.
--
To UNSUBSCRIBE, email to deity-***@lists.debian.org
with a subject of "unsubscribe". Trouble? Contact ***@lists.debian.org
Archive: http://lists.debian.org/***@jak-thinkpad
Michael Tautschnig
2010-12-28 13:33:18 UTC
Permalink
Hi all,

[...]
Post by Julian Andres Klode
External issues
===============
* picosat is built without tracing support (Bug#607943)
I'm aware of that, but please don't expect a solution before end of January (but
NMUs or patches are welcome!).
Post by Julian Andres Klode
* picosat prefers B in A | B if B > A (higher version ID wins)
picosat doesn't care. If either of them poses a valid solution, it will give you
one of them. Which of them is chose purely depends on heuristics implemented in
picosat (might even be tied to the literal ids). If you want it to prefer a
different solution, that has to be encoded.
Post by Julian Andres Klode
* picosat does not allow for optional clauses, Recommends are thus
treated as Depends. I should ask them if they are interested in
adding this.
What would be the semantics of "optional clauses" in terms of Boolean
satisfiability? What I could envision, however, is adding additional clauses
after the first round of solving the problem for Depends, using incremental SAT
solving. Add one of the Recommends at a time and see whether the problem can
still be solved. My question here would in particular be which semantics users
can expect from "Recommends" - will these packages always be installed or just
as many as possible or ...? As a user of apt I'd expect that either all of them
or none of them gets installed (depending on my apt config). Therefore I don't
see any need for "optional clauses", but I have to admit that I'm not that much
into apt development.

[...]

Best regards,
Michael
Pietro Abate
2010-12-28 14:21:25 UTC
Permalink
hello.
Post by Michael Tautschnig
Post by Julian Andres Klode
* picosat prefers B in A | B if B > A (higher version ID wins)
picosat doesn't care. If either of them poses a valid solution, it will give you
one of them. Which of them is chose purely depends on heuristics implemented in
picosat (might even be tied to the literal ids). If you want it to prefer a
different solution, that has to be encoded.
The problems about the quality of the solution produced by a SAT solver
is exactly what I meant when I said that picosat probably is not going
to be the best choice here. The upgrade/installation problem is by
nature an optimization problem. The solvers of the misc competition are
all able to accept a function that allow you to express the use
preferences or optional constraints.

There are techniques to encode these preferences in SAT (like with
minisat+), but I don't think this is the way to go. SAT solvers are only
concerned about the existence of a solution, while here we want to find
a good solution (among an exponental number of possible solutions) that
respect your constraints.
Post by Michael Tautschnig
Post by Julian Andres Klode
* picosat does not allow for optional clauses, Recommends are thus
treated as Depends. I should ask them if they are interested in
adding this.
What would be the semantics of "optional clauses" in terms of Boolean
satisfiability? What I could envision, however, is adding additional clauses
after the first round of solving the problem for Depends, using incremental SAT
solving. Add one of the Recommends at a time and see whether the problem can
still be solved. My question here would in particular be which semantics users
can expect from "Recommends" - will these packages always be installed or just
as many as possible or ...? As a user of apt I'd expect that either all of them
or none of them gets installed (depending on my apt config). Therefore I don't
see any need for "optional clauses", but I have to admit that I'm not that much
into apt development.
You can easily encode "optional clauses" with the misc solver just
giving to these clauses a different weigth in the search strategy.
Certainly you can came up with nice encodings in SAT, but again, I think
this is not the right tool here.

The entire idea about cudf is to let an external tool to deal with the
encoding of the problem and decouple apt from all these low level
issues. Using picosat and hard encoding optimization criteria in apt is
basically going toward the same slippery slope of using an, abelit
advanced, custom solution solver as we have now in apt.

p
--
----
http://en.wikipedia.org/wiki/Posting_style
--
To UNSUBSCRIBE, email to deity-***@lists.debian.org
with a subject of "unsubscribe". Trouble? Contact ***@lists.debian.org
Archive: http://lists.debian.org/***@uranium.pps.jussieu.fr
Julian Andres Klode
2010-12-28 14:47:22 UTC
Permalink
Post by Pietro Abate
hello.
Post by Michael Tautschnig
Post by Julian Andres Klode
* picosat prefers B in A | B if B > A (higher version ID wins)
picosat doesn't care. If either of them poses a valid solution, it will give you
one of them. Which of them is chose purely depends on heuristics implemented in
picosat (might even be tied to the literal ids). If you want it to prefer a
different solution, that has to be encoded.
The problems about the quality of the solution produced by a SAT solver
is exactly what I meant when I said that picosat probably is not going
to be the best choice here. The upgrade/installation problem is by
nature an optimization problem. The solvers of the misc competition are
all able to accept a function that allow you to express the use
preferences or optional constraints.
There are techniques to encode these preferences in SAT (like with
minisat+), but I don't think this is the way to go. SAT solvers are only
concerned about the existence of a solution, while here we want to find
a good solution (among an exoneponental number of possible solutions) that
respect your constraints.
Not really, you can declare literals more or less important than others
which deals with almost every case I throw at it.

/* Keep manually installed packages or installed packages that are
* candidates on the system and non-candidates away if possible. */
if (is_installed && (!is_automatic || cand == ver))
picosat_set_more_important_lit(var(ver));
else if (!is_installed && cand != ver)
picosat_set_more_important_lit(var(ver));

The solver will first try to solve the problems by setting non-candidate
versions to -1 and installed versions (manually installed or candidates)
to 1 and then trying other solutions.
Post by Pietro Abate
Post by Michael Tautschnig
Post by Julian Andres Klode
* picosat does not allow for optional clauses, Recommends are thus
treated as Depends. I should ask them if they are interested in
adding this.
What would be the semantics of "optional clauses" in terms of Boolean
satisfiability? What I could envision, however, is adding additional clauses
after the first round of solving the problem for Depends, using incremental SAT
solving. Add one of the Recommends at a time and see whether the problem can
still be solved. My question here would in particular be which semantics users
can expect from "Recommends" - will these packages always be installed or just
as many as possible or ...? As a user of apt I'd expect that either all of them
or none of them gets installed (depending on my apt config). Therefore I don't
see any need for "optional clauses", but I have to admit that I'm not that much
into apt development.
You can easily encode "optional clauses" with the misc solver just
giving to these clauses a different weigth in the search strategy.
Certainly you can came up with nice encodings in SAT, but again, I think
this is not the right tool here.
You can encode an all-or-nothing solution as (-VER | -RECOMMENDS | A |
B) and fine-grained solutions as (-VER | -RECOMMENDS_i | A_i | B_i). And
then removing RECOMMENDS from the set of assumptions if they have no
solution. Or you can solve the problem incrementally.
Post by Pietro Abate
The entire idea about cudf is to let an external tool to deal with the
encoding of the problem and decouple apt from all these low level
issues. Using picosat and hard encoding optimization criteria in apt is
basically going toward the same slippery slope of using an, abelit
advanced, custom solution solver as we have now in apt.
CUDF solvers are nice, but not a substitute for a good default solver.
--
Julian Andres Klode - Debian Developer, Ubuntu Member

See http://wiki.debian.org/JulianAndresKlode and http://jak-linux.org/.
--
To UNSUBSCRIBE, email to deity-***@lists.debian.org
with a subject of "unsubscribe". Trouble? Contact ***@lists.debian.org
Archive: http://lists.debian.org/***@jak-thinkpad
Pietro Abate
2010-12-28 15:17:55 UTC
Permalink
Post by Julian Andres Klode
Post by Pietro Abate
The entire idea about cudf is to let an external tool to deal with the
encoding of the problem and decouple apt from all these low level
issues. Using picosat and hard encoding optimization criteria in apt is
basically going toward the same slippery slope of using an, abelit
advanced, custom solution solver as we have now in apt.
CUDF solvers are nice, but not a substitute for a good default solver.
My sugestion here was more to adopt a cudf solver as default solver
(possibly as a dynamically linked library) rather then reinvent the
wheel and re-encode the upgrading problem yet again with picosat. The
people competing in the misc competition put a lot of efforts to came up
with very optimized encondings of the problem.

If you look at it a cudf solver is just

- a cudf parser (there are already independent
implementations of it in c / c++ / python / ocaml)
- the problem encoding (this is the important and creative/difficult part)
- an off-the-shelf solver (there are many around, here you just want to
pick the best avalaible)

using picosat effectively is writing yet another encoding of the problem
using picaosat a sat solver... By since you are using a pure sat solver
you will be forced to encode the problem in pure sat that is too low
level for the nature of the problem. Nothing against it. I'm just trying
to give you the picture and the state of art.

If you adopt one solver as default solver of course you won't need to
feed it cudf, but you could use build the internal data structure by
hand exatcly as you are doing with picosat. Cudf IHMO is a nice
abstracion, but in the end is just a way to allow solver poeple to focus
only on the interesting part of the problem without dealing with other
low level details. As apt-get upstream if of course in your (our)
interest to adopt the best solution brewed by the misc competition and
integrate it at a lower level of abastraction in apt-get. Maintaing a
cudf interface of course will be a plus as will give ppl the possibility
to keep playing with other solvers if the want to and to advance the
state of art.

Here there is a description of the encoding used by other solvers :
http://mancoosi.org/reports/d4.2.pdf

It might be an interesting read.

my 2 cents.
p
--
----
http://en.wikipedia.org/wiki/Posting_style
--
To UNSUBSCRIBE, email to deity-***@lists.debian.org
with a subject of "unsubscribe". Trouble? Contact ***@lists.debian.org
Archive: http://lists.debian.org/***@uranium.pps.jussieu.fr
Julian Andres Klode
2010-12-28 16:51:16 UTC
Permalink
Post by Pietro Abate
Post by Julian Andres Klode
Post by Pietro Abate
The entire idea about cudf is to let an external tool to deal with the
encoding of the problem and decouple apt from all these low level
issues. Using picosat and hard encoding optimization criteria in apt is
basically going toward the same slippery slope of using an, abelit
advanced, custom solution solver as we have now in apt.
CUDF solvers are nice, but not a substitute for a good default solver.
My sugestion here was more to adopt a cudf solver as default solver
(possibly as a dynamically linked library) rather then reinvent the
wheel and re-encode the upgrading problem yet again with picosat. The
people competing in the misc competition put a lot of efforts to came up
with very optimized encondings of the problem.
If you look at it a cudf solver is just
- a cudf parser (there are already independent
implementations of it in c / c++ / python / ocaml)
- the problem encoding (this is the important and creative/difficult part)
- an off-the-shelf solver (there are many around, here you just want to
pick the best avalaible)
using picosat effectively is writing yet another encoding of the problem
using picaosat a sat solver... By since you are using a pure sat solver
you will be forced to encode the problem in pure sat that is too low
level for the nature of the problem. Nothing against it. I'm just trying
to give you the picture and the state of art.
If you adopt one solver as default solver of course you won't need to
feed it cudf, but you could use build the internal data structure by
hand exatcly as you are doing with picosat.
For a linked-in solver, the following points must be true:
* GPL-2 compatible license
* Acceptable performance
* C/C++ API, and no dependencies except for libc, libstdc++
* A documented API
* In Debian

My personal wishlist for use in other projects as well:
* LGPL-2.1 compatible license
* C API, no dependency except for libc

I never said that the picosat solution will stay, it's just one proposal
that I started to implement because it was in the archive, and has a
simple API. Once there are other solvers in the archive, we can
implement them as well, and choose the best solution at the end.
--
Julian Andres Klode - Debian Developer, Ubuntu Member

See http://wiki.debian.org/JulianAndresKlode and http://jak-linux.org/.
--
To UNSUBSCRIBE, email to deity-***@lists.debian.org
with a subject of "unsubscribe". Trouble? Contact ***@lists.debian.org
Archive: http://lists.debian.org/***@jak-thinkpad
Julian Andres Klode
2010-12-29 16:06:47 UTC
Permalink
Post by Pietro Abate
http://mancoosi.org/reports/d4.2.pdf
It might be an interesting read.
I read it, and tried the cudfsolver, but was a bit disappointed that it
* takes 50 seconds to solve a simple problem[1] (lpsolve/glpk)
* wants to remove the whole system when using lpsolve, even in
paranoid

In contrast to this, aspcud-paranoid-1.3 takes 1.3 seconds, and seems to
produce a better result. I also played a bit with liblpsolve, but even
adding self-conflicts seems to take 1 second. The result: Solutions
using lpsolve and glpk are disqualified for a standard solver (glpk in
general, as it's license is incompatible).

The problem chosen was installing nautilus from experimental which
should be equal to an upgrade to experimental. I have put it as a
gz-compressed document at my website[1].

[1] http://jak-linux.org/tmp/example.cudf.gz
--
Julian Andres Klode - Debian Developer, Ubuntu Member

See http://wiki.debian.org/JulianAndresKlode and http://jak-linux.org/.
--
To UNSUBSCRIBE, email to deity-***@lists.debian.org
with a subject of "unsubscribe". Trouble? Contact ***@lists.debian.org
Archive: http://lists.debian.org/***@jak-thinkpad
Pietro Abate
2011-01-12 12:15:24 UTC
Permalink
Post by Pietro Abate
http://mancoosi.org/reports/d4.2.pdf
It might be an interesting read.
This is another encoding used by zypp...
http://en.opensuse.org/openSUSE:Libzypp_satsolver_basics

They are using minisat (another sat solver) and hardcoding heuristics
to find a good solution in the problem encoding. I'm not sure if they
run the solver multiple times (restart) to refine the solution.

Another interesting encoding is the one used in apt-pbo (there are a
couple of articles on the web, easy to find). This one uses minisat+
(not packaged in debian) that is a pseudo boolean solver built on top of
minisat where you can spacify the optimization function (ex: paranoid,
trendy, etc) along side with the problem encoding.

pietro
--
----
http://en.wikipedia.org/wiki/Posting_style
--
To UNSUBSCRIBE, email to deity-***@lists.debian.org
with a subject of "unsubscribe". Trouble? Contact ***@lists.debian.org
Archive: http://lists.debian.org/***@uranium.pps.jussieu.fr
Julian Andres Klode
2011-01-12 16:29:48 UTC
Permalink
Post by Pietro Abate
Post by Pietro Abate
http://mancoosi.org/reports/d4.2.pdf
It might be an interesting read.
This is another encoding used by zypp...
http://en.opensuse.org/openSUSE:Libzypp_satsolver_basics
They are using minisat (another sat solver) and hardcoding heuristics
to find a good solution in the problem encoding. I'm not sure if they
run the solver multiple times (restart) to refine the solution.
The picosat-based solver is based on that document, although it may not
do everything in the correct way. But they wrote their own specific
solver (sat-solver) instead of using a general one. My solution started
as a proof of concept that I can use a general-purpose SAT solver to
find sane solutions.
Post by Pietro Abate
Another interesting encoding is the one used in apt-pbo (there are a
couple of articles on the web, easy to find). This one uses minisat+
(not packaged in debian) that is a pseudo boolean solver built on top of
minisat where you can spacify the optimization function (ex: paranoid,
trendy, etc) along side with the problem encoding.
minisat+ does not seem to be maintained, and the performance does not
appear to be acceptable from what I read.

So while all this stuff is good in theory, in practice it does not get
us anywhere without a library implementing it which has a compatible
license, and stable enough API and ABI. For my purposes, less than or
equal to LGPL-2.1 restrictions and written in C; for APT-only purposes a
library written in C++ and GPL-2 compatible is also acceptable.

Most solvers shared in source form seem to be undocumented, without
license notes, and not suitable for libraries - completely unusable for
many people, except maybe its author (at least for a short amount of
time, until they forget how it works).

[OPINION]
And many solvers are written in C++ and/or by Windows users, both good
indicators of idiots at work - yes, good C++ code can exist, but as C++
is a large[1] piece of shit[2], most code written in it is as well[3].

[1] They can't seem to have enough features
[2] Linus:
"C++ is a horrible language. It's made more horrible by the fact
that a lot of substandard programmers use it, to the point where
it's much much easier to generate total and utter crap with it.
Quite frankly, even if the choice of C were to do *nothing* but
keep the C++ programmers out, that in itself would be a huge
reason to use C."
[3] The same as 2
[/OPINION]
--
Julian Andres Klode - Debian Developer, Ubuntu Member

See http://wiki.debian.org/JulianAndresKlode and http://jak-linux.org/.
--
To UNSUBSCRIBE, email to deity-***@lists.debian.org
with a subject of "unsubscribe". Trouble? Contact ***@lists.debian.org
Archive: http://lists.debian.org/***@jak-thinkpad
Julian Andres Klode
2011-01-13 16:51:04 UTC
Permalink
Post by Julian Andres Klode
[OPINION]
And many solvers are written in C++ and/or by Windows users, both good
indicators of idiots at work - yes, good C++ code can exist, but as C++
is a large[1] piece of shit[2], most code written in it is as well[3].
OK, "idiots" may be a bit too strong. Many of them may be sub-standard
programmers, but that may be OK for them, because they see code solely
as a tool to achieve their goals, and do not care about re-usability or
stuff like this). What I want to express is that we need code written by
people who understand our requirements as well, and not only care about
themselves.
--
Julian Andres Klode - Debian Developer, Ubuntu Member

See http://wiki.debian.org/JulianAndresKlode and http://jak-linux.org/.
--
To UNSUBSCRIBE, email to deity-***@lists.debian.org
with a subject of "unsubscribe". Trouble? Contact ***@lists.debian.org
Archive: http://lists.debian.org/***@jak-thinkpad
Stefano Zacchiroli
2010-12-30 08:26:13 UTC
Permalink
Post by Julian Andres Klode
Not really, you can declare literals more or less important than
others which deals with almost every case I throw at it.
/* Keep manually installed packages or installed packages that are
* candidates on the system and non-candidates away if possible. */
if (is_installed && (!is_automatic || cand == ver))
picosat_set_more_important_lit(var(ver));
else if (!is_installed && cand != ver)
picosat_set_more_important_lit(var(ver));
Problem is: by doing this, you're now adding quite some implicit
requirements not only on a SAT solver (which is just one among several
possible solving techniques), but also on a solver that supports an
interface like the above. The possibility of changing the solver
according to a standardized interface of the user is, if not
jeopardized, significantly diminished.
Post by Julian Andres Klode
The solver will first try to solve the problems by setting
non-candidate versions to -1 and installed versions (manually
installed or candidates) to 1 and then trying other solutions.
It sounds like it will explode pretty soon. Have you tried running it
with several suites (e.g. stable+testing+unstable) trying to install
packages from the non-default-candidate suite?

Don't get me wrong, I'm far from being in a position of arguing in favor
or against any specific solver. Nonetheless I'm more than convinced that
blessing a specific solver is risky as it's very difficult, later on, to
get rid of the implicit requirements that the blessing poses. In looking
for a better solver than current APT's, it is worth to make an effort to
standardize over an interface that makes no assumptions on specific
solving techniques. It does not necessarily need to be CUDF, but it
should have some of its good properties, like solver technique
independence. (i.e. AOL on Pietro's mail)

Cheers.
--
Stefano Zacchiroli -o- PhD in Computer Science \ PostDoc @ Univ. Paris 7
zack@{upsilon.cc,pps.jussieu.fr,debian.org} -<>- http://upsilon.cc/zack/
Quando anche i santi ti voltano le spalle, | . |. I've fans everywhere
ti resta John Fante -- V. Capossela .......| ..: |.......... -- C. Adams
Julian Andres Klode
2010-12-30 10:17:42 UTC
Permalink
Post by Stefano Zacchiroli
Post by Julian Andres Klode
Not really, you can declare literals more or less important than
others which deals with almost every case I throw at it.
/* Keep manually installed packages or installed packages that are
* candidates on the system and non-candidates away if possible. */
if (is_installed && (!is_automatic || cand == ver))
picosat_set_more_important_lit(var(ver));
else if (!is_installed && cand != ver)
picosat_set_more_important_lit(var(ver));
Problem is: by doing this, you're now adding quite some implicit
requirements not only on a SAT solver (which is just one among several
possible solving techniques), but also on a solver that supports an
interface like the above. The possibility of changing the solver
according to a standardized interface of the user is, if not
jeopardized, significantly diminished.
I don't see why. I just tell the solver to respect the policy and do the
expected thing. Without it, it does too much non-sense. Perhaps we could
introduce APT::Solver::Policy with values like "paranoid" and "trendy".
Currently, the solver tends to go more into the "paranoid" direction.
Post by Stefano Zacchiroli
Post by Julian Andres Klode
The solver will first try to solve the problems by setting
non-candidate versions to -1 and installed versions (manually
installed or candidates) to 1 and then trying other solutions.
It sounds like it will explode pretty soon. Have you tried running it
with several suites (e.g. stable+testing+unstable) trying to install
packages from the non-default-candidate suite?
I'm running on unstable + experimental, and installing packages from
experimental or doing upgrades with -texperimental works. What I'm doing
is picosat_set_default_phase_lit(var(ver), is_installed ? 1 : -1); - I
set the initial phase of a particular variable if picked as decision
variable.

The solver is then free to set something else if this does not work. It
will then first try the variables not marked as important, and
afterwards the ones marked as important, as far as I can tell.
Post by Stefano Zacchiroli
Don't get me wrong, I'm far from being in a position of arguing in favor
or against any specific solver. Nonetheless I'm more than convinced that
blessing a specific solver is risky as it's very difficult, later on, to
get rid of the implicit requirements that the blessing poses. In looking
for a better solver than current APT's, it is worth to make an effort to
standardize over an interface that makes no assumptions on specific
solving techniques. It does not necessarily need to be CUDF, but it
should have some of its good properties, like solver technique
independence. (i.e. AOL on Pietro's mail)
I don't see how implementing a generic solver interface using one
solution blesses a specific solver or makes assumptions on specific
solving techniques. The solver interface[1] is generic and supports
every kind of solver (such as one using clasp, one using CUDF, one using
a binary version of CUDF [let's call it BCUDF], one communicating with
external solvers using D-Bus, ...).

[1]
http://bzr.debian.org/scm/loggerhead/apt/apt/solver/annotate/head:/apt-pkg/solver.h
--
Julian Andres Klode - Debian Developer, Ubuntu Member

See http://wiki.debian.org/JulianAndresKlode and http://jak-linux.org/.
--
To UNSUBSCRIBE, email to deity-***@lists.debian.org
with a subject of "unsubscribe". Trouble? Contact ***@lists.debian.org
Archive: http://lists.debian.org/***@jak-thinkpad
Julian Andres Klode
2010-12-28 14:51:28 UTC
Permalink
Post by Michael Tautschnig
Hi all,
[...]
Post by Julian Andres Klode
External issues
===============
* picosat is built without tracing support (Bug#607943)
I'm aware of that, but please don't expect a solution before end of January (but
NMUs or patches are welcome!).
Post by Julian Andres Klode
* picosat prefers B in A | B if B > A (higher version ID wins)
picosat doesn't care. If either of them poses a valid solution, it will give you
one of them. Which of them is chose purely depends on heuristics implemented in
picosat (might even be tied to the literal ids). If you want it to prefer a
different solution, that has to be encoded.
The heuristics are prefering the larger literal from my testing, if all
other stuff like importance or the number uses in other clauses equals.
Post by Michael Tautschnig
Post by Julian Andres Klode
* picosat does not allow for optional clauses, Recommends are thus
treated as Depends. I should ask them if they are interested in
adding this.
What would be the semantics of "optional clauses" in terms of Boolean
satisfiability? What I could envision, however, is adding additional clauses
after the first round of solving the problem for Depends, using incremental SAT
solving. Add one of the Recommends at a time and see whether the problem can
still be solved. My question here would in particular be which semantics users
can expect from "Recommends" - will these packages always be installed or just
as many as possible or ...? As a user of apt I'd expect that either all of them
or none of them gets installed (depending on my apt config). Therefore I don't
see any need for "optional clauses", but I have to admit that I'm not that much
into apt development.
As many as possible. Each recommendation forms one clause in the solver,
and the solver may treat an unsolvable recommends clause as if it were
solved.
--
Julian Andres Klode - Debian Developer, Ubuntu Member

See http://wiki.debian.org/JulianAndresKlode and http://jak-linux.org/.
--
To UNSUBSCRIBE, email to deity-***@lists.debian.org
with a subject of "unsubscribe". Trouble? Contact ***@lists.debian.org
Archive: http://lists.debian.org/***@jak-thinkpad
David Kalnischkies
2011-01-05 11:28:43 UTC
Permalink
Post by Michael Tautschnig
can expect from "Recommends" - will these packages always be installed or just
as many as possible or ...? As a user of apt I'd expect that either all of them
or none of them gets installed (depending on my apt config). Therefore I don't
see any need for "optional clauses", but I have to admit that I'm not that much
into apt development.
Debian policy says that recommends are installed on all but unusual systems.
This means for an installation in a stable environment that recommends are
similar to dependencies as they will be installable - minus the rare cases
that a recommend package conflicts with an installed package.

In an unstable environment it could be that a recommend package is
currently not installable, but this shouldn't hinder the installation of the
package recommending it, so its not really an APT thing but policy related.


Best regards

David Kalnischkies
--
To UNSUBSCRIBE, email to deity-***@lists.debian.org
with a subject of "unsubscribe". Trouble? Contact ***@lists.debian.org
Archive: http://lists.debian.org/AANLkTinNAz2Y=sSLdRKH5fJOaaQT-wusg3ESvQJ5X=***@mail.gmail.com
Julian Andres Klode
2010-12-28 16:58:50 UTC
Permalink
Post by Julian Andres Klode
Post by Julian Andres Klode
I pushed the branch to bzr+ssh://bzr.debian.org/bzr/apt/apt/solver/, and
uploaded 0.8.10+expnewsolvers1 to experimental.
I am using this version on my main system, and that's helpful in
measuring the quality of standard tasks[...]. I pushed a fix into
bzr that makes partial upgrades possible, by keeping back impossible changes.
Uploaded 0.8.10+expnewsolvers2.
Post by Julian Andres Klode
* apt-get install
* Bug: Too Conservative. Installing mysql-server with
-texperimental will choose the mysql-server-5.1 from
unstable if libmysqlclient is already installed, because
this requires no upgrade of the installed package.
Fixed. The solution is to NOT mark the literals representing
automatically installed packages as important; and to mark literals
representing non-installed non-candidate versions as important, instead
of marking candidates as less important.
Post by Julian Andres Klode
* apt-get dist-upgrade
* Might remove every package instead of ignoring an
update. At least if you do apt-get dist-upgrade -t
experimental. We might need to keep() (manually)
installed packages first, and remove the keep() if the
user asks for it, instead of allowing the solver to do
what it wants with installed packages.
The produced solution is better than the one pkgProblemResolver creates,
so it's not that bad.
--
Julian Andres Klode - Debian Developer, Ubuntu Member

See http://wiki.debian.org/JulianAndresKlode and http://jak-linux.org/.
--
To UNSUBSCRIBE, email to deity-***@lists.debian.org
with a subject of "unsubscribe". Trouble? Contact ***@lists.debian.org
Archive: http://lists.debian.org/***@jak-thinkpad
Daniel Burrows
2011-06-22 04:46:44 UTC
Permalink
At some point, you're so late to the party that you might as well just
barge in and pretend you meant to do it all along. In this spirit:

Has this gone anywhere? I took a quick peek around the current apt
source tree and didn't see any sign of solvers.h.

Also, I dispute the notion that writing C++ rots the mind. Why, I've
been programming in C++ for over ten years, and warble gargle snaph
gheet...

Daniel
--
To UNSUBSCRIBE, email to deity-***@lists.debian.org
with a subject of "unsubscribe". Trouble? Contact ***@lists.debian.org
Archive: http://lists.debian.org/***@windrider.lan
Stefano Zacchiroli
2011-06-22 07:42:09 UTC
Permalink
Post by Daniel Burrows
At some point, you're so late to the party that you might as well
just barge in and pretend you meant to do it all along. In this
Eh, you made my day with this comment :-)
Post by Daniel Burrows
Has this gone anywhere? I took a quick peek around the current apt
source tree and didn't see any sign of solvers.h.
Yes, it has gone somewhere, mainly after a sort of "sprint" carried on
by myself and David (who deserves all credits for the APT part),
sponsored by the Mancoosi project and completed about 1 month ago. I
take the chance of this mail to apologize for not having send a report
here before; it was planned, but I didn't manage to write it down before
this mail of yours.

For the impatient, the code is available at
<https://code.launchpad.net/~donkult/+junk/mancoosi> and the keyword to
find the right files is "EDSP" for External Dependency Solver
Protocol. The protocol itself is documented at
<http://anonscm.debian.org/loggerhead/users/zack/apt.mancoosi/annotate/head:/doc/external-dependency-solver-protocol.txt>,
although it's not entirely in sync with the code, so shout before
relying on it as a spec. With respect to what have been discussed on
this list in the past, the following major changes happened:

- the protocol is independent from CUDF, although pretty close to it
(the reason is that we need to do some heavy changes to CUDF and we
don't want to constraint the APT implementation to our changes)

- nonetheless, it's trivial to do conversions back and forth and we
already have all the needed scaffolding (see below)

BTW: David, you mentioned you merged my branch with the doc, but I can't
find the .txt file in your branch above, am I missing something or it's
just too early in the morning?

I understand that the APT code is ready to be merged into the next
"merge window" of APT.

In parallel to the APT side, I've worked together with Ralf Treinen and
Pietro Abate to make CUDF-based solvers available in Debian and to
enable them to talk with APT using the EDSP protocol. A few pointers:

- at present, 3 packages in the archive now "Provides: cudf-solver" (the
random lurker can find it with "apt-cache showpkg cudf-solver")

- in experimental, you can find the new binary package "apt-cudf". When
installed, it will automatically bind installed CUDF solvers as
external solvers for APT

In short, the following needs to happen before having full support for
external solvers: the "mancoosi" branch gets merged into APT trunk and
uploaded + apt-cudf gets uploaded to unstable.

On the dark side, ATM we don't have support for multi-arch, as we need
some changes in CUDF for that. Luckily, the EDSP protocol itself is
already multi-arch enabled, so we will be able to support it without
touching the APT code (hopefully).

Cheers.
--
Stefano Zacchiroli -o- PhD in Computer Science \ PostDoc @ Univ. Paris 7
zack@{upsilon.cc,pps.jussieu.fr,debian.org} -<>- http://upsilon.cc/zack/
Quando anche i santi ti voltano le spalle, | . |. I've fans everywhere
ti resta John Fante -- V. Capossela .......| ..: |.......... -- C. Adams
David Kalnischkies
2011-06-28 16:55:40 UTC
Permalink
Post by Stefano Zacchiroli
  Has this gone anywhere?  I took a quick peek around the current apt
source tree and didn't see any sign of solvers.h.
It depends. In regards to solver.h its not done so far.

What Stefano described can be considered a very low-level interface
which is "perfectly" hidden in the old stuff, so that all the frontends
currently using the internal resolver can switch to use an external with
no code change as it still looks like as the internal resolver did the work.

solver.h would be way more general but currently it would be designing an
interface for a running target. As Stefano said CUDF isn't stable^W
feature-complete so far and it isn't exactly clear what external solvers
will need, what will be optional and what can be dropped completely.
The key concept of APT regarding a candidate-version is seriously
flawed if some solvers are concerned for example, so best of all do
not calculate it if nobody needs it, but what else is optional?
CUDF is optional, but how to expose APT's mmap cleanly?
And we haven't yet answered questions like how to work with
interactive solver (like the one in aptitude) at all…


Lets assume Daniel asked because he is interested in making the aptitude
solver available as an external solver: Easy! (Maybe?)
You can do something similar to what APT does for his internal solver:
http://bazaar.launchpad.net/~donkult/apt/experimental/view/head:/cmdline/apt-internal-solver.cc
(missing is preferences and autobit so far through, so it's not complete)
Its a bit slow to convert MMap to EDSP and back, but it is quiet interesting
for testing at least and binary transfer hard-depends on solver.h …

If you want to support EDSP in aptitude to use external resolver, too,
you might get along with using at least parts of edsp.{cc,h}, but i
don't know the aptitude code to provide a good answer to that.
Post by Stefano Zacchiroli
BTW: David, you mentioned you merged my branch with the doc, but I can't
find the .txt file in your branch above, am I missing something or it's
just too early in the morning?
Not your fault, i wasn't too clear about that…
I moved on to lp:~donkult/apt/experimental
which bundles a few more more or less unfinished & (un)related abi-breaks
(in a now again seriously outdated branch regarding to debian-sid…
time oh time, where are you?)
But yes, mancoosi-stuff is absolutely on the agenda for the next
abi break, but nobody has an serious ETA then this will happen.
Post by Stefano Zacchiroli
- in experimental, you can find the new binary package "apt-cudf". When
 installed, it will automatically bind installed CUDF solvers as
 external solvers for APT
btw: Sounds good. Will try that later. :)


Best regards

David Kalnischkies
--
To UNSUBSCRIBE, email to deity-***@lists.debian.org
with a subject of "unsubscribe". Trouble? Contact ***@lists.debian.org
Archive: http://lists.debian.org/BANLkTi=***@mail.gmail.com
Stefano Zacchiroli
2011-06-29 10:10:14 UTC
Permalink
Post by David Kalnischkies
The key concept of APT regarding a candidate-version is seriously
flawed if some solvers are concerned for example, so best of all do
not calculate it if nobody needs it, but what else is optional?
Indeed. Or, to be more precise, it's a bit too constraining if we want
to exploit advantages that state of the art solvers can offer. The
question is whether the notion of candidate-version established via
pinning is part of the specification of what a solver *must* do (i.e. no
solver will be allowed to deviate from it), or rather a quality criteria
to be fulfilled in some best effort way, possibly coupled with a warning
of deviation before applying a proposed solution.

The way we did that in EDSP is that, by default, pinning *must* be
obeyed to, whereas users can explicitly request to be more flexible (the
keyword in the protocol description is "Strict-Pinning", IIRC).

But this really is a major policy point that should be decided by our
beloved deities.
Post by David Kalnischkies
CUDF is optional, but how to expose APT's mmap cleanly?
<snip>
Post by David Kalnischkies
Its a bit slow to convert MMap to EDSP and back, but it is quiet
interesting for testing at least and binary transfer hard-depends on
solver.h 

The day we will be satisfied with EDSP as a long term solution---I *am*
satisfied ATM, but as a matter of fact we haven't yet started testing
with real users, so we should better be cautious---we can imagine having
a binary version of the EDSP protocol. And yes, at that point we will
need an answer to your question above.
Post by David Kalnischkies
And we haven't yet answered questions like how to work with
interactive solver (like the one in aptitude) at all

Indeed. By the way, here in Paris we are interested in working on this,
but we need people with implementation experience on interacting solving
as peers (as far as I understand, that set of people is the singleton
set containing Daniel). So if you are interested in working on this,
please let me know.
Post by David Kalnischkies
Not your fault, i wasn't too clear about that

I moved on to lp:~donkult/apt/experimental
Ah, that explains it, thanks for the pointer!

Cheers.
--
Stefano Zacchiroli -o- PhD in Computer Science \ PostDoc @ Univ. Paris 7
zack@{upsilon.cc,pps.jussieu.fr,debian.org} -<>- http://upsilon.cc/zack/
Quando anche i santi ti voltano le spalle, | . |. I've fans everywhere
ti resta John Fante -- V. Capossela .......| ..: |.......... -- C. Adams
Loading...