mikolas DOT janota AT-SIGN-GOES-HERE gmail DOT-GOES-HERE com
cudf2msu is a solver for the package upgrade problem developed as a part of the European MANCOOSI project at the SAT group based in INESC-ID. The solver inputs and outputs the CUDF format. The purpose is to investigate the suitability of an UNSAT-based MAX-SAT solver to the upgrade problem.
The solver consists of two main parts. One part takes in a CUDF file and produces a Weighted MAX-SAT formula. The second part solves that formula (the MAX-SAT solver). Both parts were developed in C++ and were integrated into one binary in order to facilitate the exchange of information between them.
The formula captures the dependencies between packages and the request as hard clauses. The optimization criteria are captured as weighted clauses (see [1]). An important part of the transformation from CUDF to a formula is a technique called slicing, which discards those packages that are not necessary for satisfying the request (see [3]).
The MAX-SAT solver used is MSUnCore. MSUnCore is an UNSAT-based solver, which means that it converges to an optimal solution from a lower bound. If the given formula encodes a lexicographic function, the solver solves each criterion in a separate iteration phase (see [2] for more details).
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.
|
[1]
Solving Linux Upgradeability Problems Using Boolean Optimization
|
|
[2] On Solving Boolean Multilevel Optimization Problems.
|
|
[3] OPIUM: Optimal Package Install/Uninstall Manager
|