- Authors: Mikoláš Janota, Joao Marques-Silva, Inês Lynce, and Vasco Manquinho
-
Contact:
mikolas DOT-GOES-HERE janota AT-SIGN-GOES-HERE gmail DOT-GOES-HERE com
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.
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.
- msuncore, run as
packup --max-sat --external-solver 'msuncore -wl -bmo' -
minisat+ (new version), run as
packup --external-solver 'minisatp -cs -ansi' --multiplication-string ' ' -
minisat+, run as
packup(default solver)
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.
|
|
[ES06]
Translating Pseudo-Boolean Constraints into SAT.
|
|
[TZ09] Common upgradeability description format (CUDF) 2.0. Technical Report 003, MANCOOSI, November 2000
|
|
|
|
Last updated: Apr 13, 2013 14:19:59 PM |