1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
|
.TH PACKUP 1 "May 2011" "" "User Commands"
.SH NAME
PackUP -- PACKage Upgradability Problem solver
.SH SYNOPSIS
.B packup
[OPTIONS] input_file_name [output_file_name]
.SH DESCRIPTION
.PP
packup is a solver for the package upgradability problem specified in CUDF [TZ09].
It repeatedly invokes an optimization pseudo-Boolean solver in order to solve the
problem. By default minisat+ [ES06] is used for that purpose but a different
solver can be used by specifying the pertaining command line option.
.PP
If input_file_name is '-', input is read from the standard input. If the
output_file_name is omitted, output is produced to the standard output.
.SH OPTIONS
.TP
\fB\-t\fR
Use trendy criterion
.TP
\fB\-p\fR
Use paranoid criterion
.TP
\fB\-u\fR \fIcs\fR
Use user criterion \fIcs\fR. A criterion is a lexicographic combination of
the utility functions removed, notuptodate, unmet_recommends, new, and
changed. Each of them with a polarity ("+" for a function to maximize, "-" for
a function to minimize). The functions are listed in decreasing order of
priority, and separated by the symbol ",". For instance, the paranoid criterion
could be written as -removed,-changed.
For more details see: http://www.mancoosi.org/misc-live/20101126/criteria/
.TP
\fB\-\-external-solver\fR
command for the external solver default 'minisat+ -ansi'
.TP
\fB\-\-multiplication-string\fR
string between coefficients and variables when communicating to the solver, default '*'
.TP
\fB\-\-temporary-directory\fR \fIDIR\fR
directory where temporary files are created. If this option is not given
then the value of $TMPDIR is used if defined, otherwise temporary files
are placed in '/tmp'.
.TP
\fB\-\-leave-temporary-files\fR
do not delete temporary files
.SH AUTHOR
Written by Mikolas Janota and Joao Marques Silva
.SH REPORTING BUGS
Please report any problems with the solver to mikolas@sat.inesc-id.pt
.SH REFERENCES
.PP
[ES06] Niklas Een and Niklas Sorensson. Translating Pseudo-Boolean Constraints into SAT. SAT, 2006
.PP
[TZ09] Ralf Treinen and Stefano Zacchiroli. Common upgradeability description format (CUDF) 2.0.
Technical Report 003, MANCOOSI, November 200
.SH COPYRIGHT NOTICE
.PP
(C) 2011 Mikolas Janota
.PP
This file is part of packup.
.PP
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.
.PP
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 <http://www.gnu.org/licenses/>.
|
