RFC: The Future of Solving Dependency Problems in APT (SAT, CUDF)
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/.
/* solver.h - Base class for dependency problem solvers in APT.
*
* Copyright (C) 2010 Julian Andres Klode <jak@debian.org>
*
* Permission is hereby granted, free of charge, to any person
* obtaining a copy of this software and associated documentation files
* (the "Software"), to deal in the Software without restriction,
* including without limitation the rights to use, copy, modify, merge,
* publish, distribute, sublicense, and/or sell copies of the Software,
* and to permit persons to whom the Software is furnished to do so,
* subject to the following conditions:
*
* The above copyright notice and this permission notice shall be
* included in all copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
* EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
* MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
* NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS
* BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN
* ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
* CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
* SOFTWARE.
*/
class pkgDepCache;
namespace APT {
class VersionSet;
/**
* \class APT::Solver
* \brief Abstract base class for new-style dependency problem solvers.
*
* This base class defines the interface for the new dependency problem
* solvers introduced in APT 0.9. It works by preparing sets of changes,
* passing the set of changes to the solver, and then calling Solve() to
* solve the problem.
*/
class Solver {
public:
/**
* \enum Rule
* \brief Flags that change the behavior of solvers.
*
* These flags add further constraints to the solver or
* remove constraints from the solver. They are equivalent
* to the following boolean options in the "APT::Solver"
* configuration section in apt.conf:
*
* - APT::Solver::candidates-only
* - APT::Solver::no-removals
* - APT::Solver::no-new-packages
* - APT::Solver::allow-negative-pinned
* - APT::Solver::ignore-negative-dependencies
*
* By default, all options are unset.
*/
enum Rule {
/** \brief Only allow installation of candidate versions. */
CANDIDATES_ONLY = (1 << 0),
/** \brief Like calling Install() for all installed packages. */
NO_REMOVALS = (1 << 1),
/** \brief Like calling Remove() for all not-installed packages. */
NO_NEW_PACKAGES = (1 << 2),
/** \brief Allow the installation of negatively pinned packages. */
ALLOW_NEGATIVE_PINNED = (1 << 3),
/** \brief Ignore dependencies like "Breaks" or "Conflicts". */
IGNORE_NEGATIVE_DEPENDENCIES = (1 << 4)
};
/**
* \brief Creates new solver.
*
* Creates a new solver. Please note that depcache should remain the
* same for the lifetime of the solver, as the solver may cache
* information about dependencies.
*
* \param depcache The depcache that will be used to feed the solver
* with information about the universe and will be
* changed according to the solver's solution.
* \param rules The rules for the solver. If 0, the solver will
* use the values defined in apt.conf. If -1, no
* rules are set.
*/
Solver(pkgDepCache &depcache, unsigned int rules = 0);
/**
* \brief Gets the rules for the solver.
*
* \return The rules, an OR combination of APT::Solver::Rule values.
*/
unsigned int GetRules() const;
/**
* \brief Sets the rules for the solver.
*
* \param rules An OR combination of values of the APT::Solver::Rule enum.
*/
void SetRules(unsigned int rules);
/**
* \brief Marks all versions in the set for installation.
*
* Marks the given version for installation if they are not
* installed, or tells the solver to prevent their removal
* if they are installed.
*
* \param install A set of versions that shall be installed.
*/
virtual bool Install(const VersionSet &install) = 0;
/**
* \brief Marks all versions in the set for removal.
*
* Marks the given version for removal if they are installed,
* or tells the solver to prevent their installation if they
* are not installed.
*
* \param remove A set of versions that shall not be installed.
*/
virtual bool Remove(const VersionSet &remove) = 0;
/**
* \brief Tells the solver to mark all upgradable packages for upgrade.
*
* Marks every installed package for which a newer candidate version
* exists for upgrade. To upgrade only specific packages, pass their
* candidate versions to Install().
*/
virtual bool Upgrade() = 0;
/**
* \brief Finds a solution to the problem and change the depcache.
*
* Finds a solution to the problem if possible, and then changes
* the depcache according to that solution. If no solution has
* been found, the depcache remains unchanged. Once this method
* returned, the solver will be in the same state as directly
* after its construction. All calls to Install(), Remove(),
* and/or Upgrade() are forgotten.
*
* If you do not need to change the depcache, you may want to
* use Solve() instead.
*/
bool SolveAndSet();
/**
* \brief Finds a solution to the problem and returns the needed changes.
*
* Finds a solution to the problem if possible, and then returns such
* solution in the sets given to the function by reference. After the
* return, the solver removes all knowledge about the jobs and may be
* used again, as if it was freshly created.
*
* This method may also be used to run an incremental solving process,
* by passing the result of install to Install() and the result of
* remove to Remove(), doing some more changes and then calling
* Solve() again. Doing this on external solvers is not recommended,
* as this way of operation is too slow in that case.
*
* \param install A reference to a set that will contain all
* versions that shall be installed on the system.
* \param remove A reference to a set that will contain all
* versions that shall be removed from the system.
* \param automatic A reference to a set that will be a subset of
* the union of install and remove listing only
* those changes that are not requested by the user.
*/
virtual bool Solve(VersionSet &install, VersionSet &remove,
VersionSet &automatic) = 0;
protected:
/**
* \brief The depcache containing the universe
*
* This depcache defines the current status ("the universe"),
* possibly the request, and might be changed by SolveAndSet()
* to resemble the solution.
*/
pkgDepCache &depcache;
private:
/** \brief An OR combination of values from APT::Solver::Rule. */
unsigned int rules;
};
}
#include <apt-pkg/init.h>
#include <apt-pkg/cachefile.h>
#include <apt-pkg/sptr.h>
#include <apt-pkg/cacheset.h>
#include <cassert>
#include <cstddef>
#include <iostream>
#include <map>
extern "C" {
#include <picosat/picosat.h>
}
using namespace APT;
typedef std::map<unsigned short,VersionSet> GroupedVersionSet;
#define aassert(exp) \
do { \
exp; \
if (_error->PendingError()) exit((_error->DumpErrors(), 1)); \
} while (0)
static int var(const pkgCache::Version * version)
{
return version->ID + 1;
}
static std::string display_name(const pkgCache::VerIterator &version)
{
return version.ParentPkg().FullName(true) + " (" + version.VerStr() + ")";
}
static std::string display_name(const pkgCache::VerIterator &a,
const pkgCache::VerIterator &b)
{
return (a.ParentPkg().FullName(true) + " (" + a.VerStr() + " => "
+ b.VerStr() + ")");
}
void cleanup()
{
/* Final cleanup to make valgrind happy */
picosat_reset();
delete _config;
delete _error;
}
int main(int argc, const char *argv[])
{
(void) argc;
picosat_init();
bool have_trace = picosat_enable_trace_generation();
atexit(cleanup);
pkgInitConfig(*_config);
pkgInitSystem(*_config, _system);
pkgCacheFile file;
aassert(file.Open(NULL, false));
pkgCache *cache = file;
pkgDepCache *depCache = file;
picosat_adjust(cache->HeaderP->VersionCount);
SPtrArray <pkgCache::Version*> versions =
new pkgCache::Version*[cache->HeaderP->VersionCount];
std::map<int,pkgCache::Dependency*> depclauses;
std::set<int> jobs;
// Parse package specifiers given on command-line
std::list < VersionSet::Modifier > mods;
mods.push_back(VersionSet::Modifier(0, "+", VersionSet::Modifier::NONE,
VersionSet::CANDIDATE));
mods.push_back(VersionSet::Modifier(1, "-", VersionSet::Modifier::POSTFIX,
VersionSet::ALL));
mods.push_back(VersionSet::Modifier(1, "_", VersionSet::Modifier::POSTFIX,
VersionSet::ALL));
GroupedVersionSet map = APT::VersionSet::GroupedFromCommandLine(file,
argv + 1,
mods, 0);
// Prints error and exits if invalid argument was passed on command-line.
aassert((void)0);
std::cout << "Request:\n";
for (VersionSet::iterator v = map[0].begin(); v != map[0].end(); ++v) {
std::cout << " Install: " << display_name(v) << "\n";
jobs.insert(var(*v));
}
for (VersionSet::iterator v = map[1].begin(); v != map[1].end(); ++v) {
std::cout << " Remove: " << display_name(v) << "\n";
jobs.insert(-var(*v));
}
for (pkgCache::PkgIterator pkg = cache->PkgBegin(); pkg != cache->PkgEnd(); ++pkg)
for (pkgCache::VerIterator ver = pkg.VersionList(); !ver.end(); ++ver)
versions[ver->ID] = ver;
// Explain the universe and the request to picosat.
for (size_t i = 0; i < cache->HeaderP->VersionCount; ++i) {
const pkgCache::VerIterator ver(file, versions[i]);
const pkgCache::PkgIterator pkg = ver.ParentPkg();
const pkgCache::VerIterator cand = depCache->GetCandidateVer(pkg);
#if SIMULATE_APT
/* APT Simulation: Prohibit installation of non-candidate versions */
if (ver != cand && ver != pkg.CurrentVer() && jobs.find(var(ver)) == jobs.end())
picosat_assume(-var(ver));
#endif
for (pkgCache::VerIterator ver2 = pkg.VersionList(); !ver2.end(); ++ver2) {
if (ver->ID != ver2->ID) {
picosat_add(-var(ver));
picosat_add(-var(ver2));
picosat_add(0);
}
}
assert(!ver.end());
bool begins_group = true;
for (pkgCache::DepIterator dep = ver.DependsList(); !dep.end(); ++dep) {
pkgCache::Version **versions_ = dep.AllTargets();
pkgCache::Version **versionp = versions_;
switch (dep->Type) {
case pkgCache::Dep::Recommends:
// Ignore recommends from installed packages.
if (pkg.CurrentVer())
break;
case pkgCache::Dep::Depends:
case pkgCache::Dep::PreDepends:
if (begins_group)
picosat_add(-var(ver));
while (*versionp)
picosat_add(var(*versionp++));
begins_group = (dep->CompareOp & pkgCache::Dep::Or) == 0;
if ((dep->CompareOp & pkgCache::Dep::Or) == 0) {
int clause = picosat_add(0);
if (have_trace)
depclauses[clause] = dep;
}
break;
case pkgCache::Dep::Conflicts:
case pkgCache::Dep::DpkgBreaks:
while (*versionp) {
picosat_add(-var(ver));
picosat_add(-var(*versionp++));
int clause = picosat_add(0);
if (have_trace)
depclauses[clause] = dep;
}
break;
default:
break;
}
delete[]versions_;
}
bool is_installed = pkg.CurrentVer() == ver;
bool want_install = jobs.find(var(ver)) != jobs.end();
bool want_remove = jobs.find(-var(ver)) != jobs.end();
/* Keep the state of the package by default */
picosat_set_default_phase_lit(var(ver), is_installed ? 1 : -1);
if (is_installed) /* Keeping installed packages is important */
picosat_set_more_important_lit(var(ver));
else if (cand == ver) /* Keeping candidates away is not important */
picosat_set_less_important_lit(var(ver));
/* Add the jobs */
if (want_install)
picosat_assume(var(ver));
if (want_remove)
picosat_assume(-var(ver));
}
std::cout << "\n";
switch (picosat_sat(-1)) {
case PICOSAT_SATISFIABLE:
break;
case PICOSAT_UNSATISFIABLE:
std::cout << "Unsolvable:\n";
if (!have_trace) {
const int *failed = picosat_failed_assumptions();
do {
pkgCache::VerIterator ver(file, versions[abs(*failed) - 1]);
std::cout << " Cannot "
<< (*failed > 0 ? "install: " : "remove: ")
<< display_name(ver) << "\n";
} while (*++failed);
}
else{
for (int i=0; i < picosat_added_original_clauses(); i++) {
pkgCache::DepIterator dep(file, depclauses[i]);
if (dep.IsGood() && picosat_coreclause(i)) {
std::cout << " " << dep << "\n";
}
}
}
return 1;
case PICOSAT_UNKNOWN:
std::cout << "Cannot solve the problem (unknown).\n";
return 1;
default:
std::cout << "Cannot solve the problem (some error).\n";
return 1;
}
std::cout << "Solution: \n";
bool changes = false;
for (size_t i = 0; i < cache->HeaderP->VersionCount; ++i) {
const pkgCache::VerIterator ver(file, versions[i]);
const pkgCache::PkgIterator pkg = ver.ParentPkg();
const pkgCache::VerIterator current_ver = pkg.CurrentVer();
const bool is_installed = (current_ver == ver);
const int result = picosat_deref(var(ver));
if ((result == 1 && is_installed) || (result == -1 && !is_installed) ||
result == 0)
continue;
changes = true;
if (is_installed)
std::cout << " Remove: " << display_name(ver);
else if (current_ver)
std::cout << " Upgrade: " << display_name(current_ver, ver);
else
std::cout << " Install: " << display_name(ver);
std::cout << "\n";
}
if (!changes)
std::cout << " Change nothing\n";
}
Reply to: