PackUP, PACKage Upgradability Problem solver


packup solves the package upgradability problem specified in CUDF [TZ09] with the use of an external solver. By default minisat+ [ES06] is used but a different solver can be used by specifying the pertaining command line option.

Technical Information

The solver translates the problem into a Weighted MAX-SAT formula. It calls a MaxSAT or optimization-pseudo-Boolean (OPB) solver to solve it. An OPB solver is invoked several times, cf. [ALMS09].

The solver supports optimization criteria designed for the 3rd MISC Live competition. The criterion to be optimized by the solver is specified as a lexicographic ordering on a set of utility functions, which can be further minimized or maximized. Internally the criteria "trendy" and "paranoid" are treated as special cases of the more general lexicographic ordering specification, i.e., there are no specific techniques invoked in the case of these two criteria.


src-0.6, man page, man page.html, release notes
src-0.5, man page, release notes


The solver participated in the 3rd MISC Live competition using msuncore and bmo-plex as a backend (as cudf2msu and cudf2pbo).

Here are some more results using the current versions of our and other solvers.


(C) 2011 Mikolas Janota

packup is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version.

packup is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.

You should have received a copy of the GNU General Public License along with packup. If not, see GNU Licence.

[ALMS09] On Solving Boolean Multilevel Optimization Problems.
Josep Argelich, Inês Lynce, and Joao Marques-Silva
[ES06] Translating Pseudo-Boolean Constraints into SAT.
Niklas Een and Niklas Sorensson
[TZ09] Common upgradeability description format (CUDF) 2.0. Technical Report 003, MANCOOSI, November 2000
Ralf Treinen and Stefano Zacchiroli

Valid XHTML 1.0 Strict VI Improved Last updated: Apr 13, 2013 14:19:59 PM