[SCM] minisat+ packaging branch, master, updated. upstream/2011.05.10-14-g572421b

[Ralf Treinen]

The following commit has been merged in the master branch:
commit a25bf625a4350b6ad8213fb7adc79bca28344edf
Author: Ralf Treinen <treinen at free.fr>
Date:   Wed May 11 16:16:22 2011 +0200

    finalise first version of a manpage

diff --git a/debian/minisat+.1 b/debian/minisat+.1
index 10a50b4..43f7e8a 100644
--- a/debian/minisat+.1
+++ b/debian/minisat+.1
@@ -2,6 +2,10 @@
 .SH NAME
 minisat+ \- A Solver for Pseudo-Boolean Constraints
 
+.SH SYNOPSIS
+.B minisat+
+.R  <input\-file> [<result\-file>] [<option> ...]
+
 .SH DESCRIPTION
 MiniSat+ is a solver for Pseudo-Boolean constraints, based on MiniSat.
 
@@ -11,79 +15,79 @@ can take as values only 0 or 1. (In-)equations used in hard
 constraints and objective functions, however, may use arbitrary
 integer coefficients.
 
-.SH
-USAGE:
-minisat+ <input\-file> [<result\-file>] [\-<option> ...]
+Minisat+ accepts problem specifications written in the OPB format.
 
 .SH OPTIONS
 .SS "Solver options:"
 .TP
-\fB\-M\fR \fB\-minisat\fR
+.BR \-M , \-minisat
 Use MiniSat v1.13 as backend (default)
 .TP
-\fB\-S\fR \fB\-satelite\fR
+\.BR \-S , \-satelite
 Use SatELite v1.0 as backend
 .TP
-\fB\-ca\fR \fB\-adders\fR
+.BR \-ca , \-adders
 Convert PB\-constrs to clauses through adders.
 .TP
-\fB\-cs\fR \fB\-sorters\fR
+.BR -cs , -sorters
 Convert PB\-constrs to clauses through sorters.
 .TP
-\fB\-cb\fR \fB\-bdds\fR
+.BR -cb , \-bdds
 Convert PB\-constrs to clauses through bdds.
 .TP
-\fB\-cm\fR \fB\-mixed\fR
+.BR \-cm , \-mixed
 Convert PB\-constrs to clauses by a mix of the above. (default)
 .TP
-\fB\-ga\fR/gs/gb/gm
+.BR -ga , -gs , -gb , -gm
 Override conversion for goal function (long name: \fB\-goal\-xxx\fR).
 .TP
-\fB\-w\fR \fB\-weak\-off\fR
+.BR \-w , \-weak\-off
 Clausify with equivalences instead of implications.
 .TP
-\fB\-bdd\-thres=\fR
-Threshold for prefering BDDs in mixed mode.        [def: 3]
+\fB\-bdd \fIn\fR, \fB\-thres=\fIn\fR
+Set threshold for preferring BDDs in mixed mode to \fIn\fR (default: 3)
 .TP
-\fB\-sort\-thres=\fR
-Threshold for prefering sorters. Tried after BDDs. [def: 20]
+\fB\-sort\-thres=\fIn\fR
+Set threshold for preferring sorters to \fIn\fR. Tried after BDDs (default: 20)
 .TP
-\fB\-goal\-bias=\fR
-Bias goal function convertion towards sorters.     [def: 3]
+\fB\-goal \fIn\fR, \fB\-bias=\fIn\fR
+Set bias goal function conversion towards sorters to \fIn\fR (default: 3).
 .TP
-\fB\-1\fR \fB\-first\fR
+\fB\-1\fR, \fB\-first\fR
 Don't minimize, just give first solution found
 .TP
-\fB\-A\fR \fB\-all\fR
+\fB\-A\fR, \fB\-all\fR
 Don't minimize, give all solutions
 .TP
-\fB\-goal=\fR<num>
-Set initial goal limit to '<= num'.
+\fB\-goal=\fIn\fR
+Set initial goal limit to \fIn\fR.
 .TP
-\fB\-p\fR \fB\-pbvars\fR
+\fB\-p\fR, \fB\-pbvars\fR
 Restrict decision heuristic of SAT to original PB variables.
 .TP
 \fB\-ps\fR{+,\-,0}
 Polarity suggestion in SAT towards/away from goal (or neutral).
+
 .SS "Input options:"
 .TP
-\fB\-of\fR \fB\-old\-fmt\fR
+\fB\-of\fR, \fB\-old\-fmt\fR
 Use old variant of OPB file format.
+
 .SS "Output options:"
 .TP
-\fB\-s\fR \fB\-satlive\fR
+\fB\-s\fR, \fB\-satlive\fR
 Turn off SAT competition output.
 .TP
-\fB\-a\fR \fB\-ansi\fR
+\fB\-a\fR, \fB\-ansi\fR
 Turn off ANSI codes in output.
 .TP
-\fB\-v0\fR,\-v1,\-v2
-Set verbosity level (1 default)
+\fB\-v\fIn\fR Set verbosity level to \fIn\fR. Possible values for
+\fIn\fR are 1,2,3 (default: 1).
 .TP
-\fB\-cnf=\fR<file>
-Write SAT problem to a file. Trivial UNSAT => no file written.
+\fB\-cnf=\fIfile\fR
+Write SAT problem to a file \fIfile\fR. If the input problem is found to be
+trivially unsatisfiable then no file is written.
 .PP
 
 .SH AUTHORS
- Minisat+ was written by Niklas Een and Niklas Sorensson.
-
+Minisat+ was written by Niklas Een and Niklas Sorensson.

-- 
minisat+ packaging