mikolas DOT janota AT-SIGN-GOES-HERE gmail DOT-GOES-HERE com
cudf2pbo 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 a pseudo-boolean optimization (PBO) 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).
The formula is obtained from the solver cudf2msu, which was developed by the first author. Hence, the solver supports the same type of optimization criteria as cudf2msu.
The formula representing the problem is solved using the solver WBO [2]. While WBO enables a number of approaches to solve a MAX-SAT problem, cudf2wbo uses the approach where the solution is sought from the upper bound. This means that the solver maintains a solution to the problem and gradually improves it. The approach enables to easily produce (sub-optimal) intermediate solutions in case of a timeout. If the given formula encodes a lexicographic criterion, the solver solves each function in a separate iteration phase (see [1] for more details).
|
[1] On Solving Boolean Multilevel Optimization Problems.
|
|
[2] Algorithms for Weighted Boolean Optimization.
|