Re: RFC: The Future of Solving Dependency Problems in APT (SAT, CUDF)
On Mi, 2010-12-22 at 18:32 +0100, Julian Andres Klode wrote:
> 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/.
#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;
}
// Needed to have output sorted by name
struct pkgSort
{
bool operator()(const pkgCache::PkgIterator &a, const pkgCache::PkgIterator &b) const
{
return a.FullName() < b.FullName();
}
};
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;
if (argv[1] && std::string(argv[1]) == "install") {
// 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 + 2,
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));
}
} else if (argv[1] && std::string(argv[1]) == "upgrade") {
std::cout << "Request: Upgrade\n";
for (pkgCache::PkgIterator pkg = cache->PkgBegin(); pkg != cache->PkgEnd(); ++pkg) {
pkgCache::VerIterator cand = depCache->GetCandidateVer(pkg);
pkgCache::VerIterator curr = pkg.CurrentVer();
if (cand && curr && cand != curr) {
jobs.insert(var(cand));
jobs.insert(-var(curr));
}
}
} else if (argv[1]) {
std::cerr << "E: Invalid command: " << argv[1] << "\n";
exit(1);
} else {
std::cerr << "E: Must specify command: install or upgrade\n";
exit(1);
}
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";
std::set<pkgCache::PkgIterator,pkgSort> p;
for (pkgCache::PkgIterator pkg = cache->PkgBegin(); pkg != cache->PkgEnd(); ++pkg)
p.insert(pkg);
bool changes = false;
for (PackageSet::iterator pkg = p.begin(); pkg != p.end(); ++pkg) {
pkgCache::VerIterator current = pkg.CurrentVer();
pkgCache::VerIterator remove;
pkgCache::VerIterator install;
for (pkgCache::VerIterator ver = pkg.VersionList(); !ver.end(); ++ver) {
const int result = picosat_deref(var(ver));
if (result == 1 && ver != current)
install = ver;
if (result == -1 && ver == current)
remove = ver;
}
if (install.IsGood() && remove.IsGood())
std::cout << " Upgrade: " << display_name(remove, install) << "\n";
else if (install.IsGood())
std::cout << " Install: " << display_name(install) << "\n";
else if (remove.IsGood())
std::cout << " Remove: " << display_name(remove) << "\n";
changes |= (install.IsGood() || remove.IsGood());
}
if (!changes)
std::cout << " Change nothing\n";
}
Reply to: