[SCM] minisat+ packaging branch, master, updated. upstream/1.0-5-ge3da230

Ralf Treinen treinen at free.fr
Thu May 12 20:33:08 UTC 2011


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

    add debian tree

diff --git a/debian/changelog b/debian/changelog
new file mode 100644
index 0000000..21d15c3
--- /dev/null
+++ b/debian/changelog
@@ -0,0 +1,6 @@
+minisat+ (1.0-1) unstable; urgency=low
+
+  * Initial package.
+
+ -- Ralf Treinen <treinen at debian.org>  Tue, 10 May 2011 17:08:02 +0200
+
diff --git a/debian/compat b/debian/compat
new file mode 100644
index 0000000..45a4fb7
--- /dev/null
+++ b/debian/compat
@@ -0,0 +1 @@
+8
diff --git a/debian/control b/debian/control
new file mode 100644
index 0000000..147d8ad
--- /dev/null
+++ b/debian/control
@@ -0,0 +1,23 @@
+Source: minisat+
+Section: science
+Priority: extra
+Maintainer: Debian Science Maintainers <debian-science-maintainers at lists.alioth.debian.org>
+Uploaders: Ralf Treinen <treinen at debian.org>
+Build-Depends: debhelper (>= 8), libgmp3-dev
+Standards-Version: 3.9.2
+Homepage: http://minisat.se/MiniSat+.html
+Vcs-Git: git://git.debian.org/git/debian-science/packages/minisat+.git
+Vcs-Browser: http://git.debian.org/?p=debian-science/packages/minisat+.git
+
+Package: minisat+
+Architecture: any
+Depends: ${misc:Depends}, ${shlibs:Depends}
+Description: solver for pseudo_Boolean constraints
+ MinSat+ is a solver for Pseudo-Boolean Optimization (AKA 0-1
+ integer programming) that is based on the MiniSat SAT-solver. It
+ supports optimizing a linear objective function, subject to a set
+ of linear constraints. The variables of the objective function
+ and constraints are boolean, i.e. required to be 0 or
+ 1. Pseudo-Boolean optimization can be used to solve many kinds of
+ combinatorial optimization problems. This version of Minisat+ is
+ compiled with bignum support for constraint coefficients.
diff --git a/debian/copyright b/debian/copyright
new file mode 100644
index 0000000..7b39db4
--- /dev/null
+++ b/debian/copyright
@@ -0,0 +1,31 @@
+Upstream-Name: copyright
+Upstream-Contact: Niklas Sorensson <nik at chalmers.se>
+Source: http://minisat.se/downloads/minisatp-1.0.tar.gz
+Copyright: 2005-2010 Niklas Eén and Niklas Sörensson
+Licence: MIT 
+ Permission is hereby granted, free of charge, to any person obtaining
+ a copy of this software and associated documentation files (the
+ "Software"), to deal in the Software without restriction, including
+ without limitation the rights to use, copy, modify, merge, publish,
+ distribute, sublicense, and/or sell copies of the Software, and to
+ permit persons to whom the Software is furnished to do so, subject to
+ the following conditions:
+
+ The above copyright notice and this permission notice shall be included
+ in all copies or substantial portions of the Software.
+
+ THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+ EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+ MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+ NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS
+ BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN
+ ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+ CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+ SOFTWARE.
+
+Files: *
+Copyright:2005-2010  Niklas Eén and Niklas Sörensson
+Licence: MIT
+
+
+
diff --git a/debian/minisat+.1 b/debian/minisat+.1
new file mode 100644
index 0000000..05b9ac6
--- /dev/null
+++ b/debian/minisat+.1
@@ -0,0 +1,93 @@
+.TH "MINISAT+" 1
+.SH NAME
+minisat+ \- A Solver for Pseudo-Boolean Constraints
+
+.SH SYNOPSIS
+.B minisat+
+<input\-file> [<result\-file>] [<option> ...]
+
+.SH DESCRIPTION
+MiniSat+ is a solver for Pseudo-Boolean constraints, based on MiniSat.
+
+Pseudo-Boolean constraints can be used to describe certain kinds of
+combinatorial optimization problems. Variables are Boolean, that is
+can take as values only 0 or 1. (In-)equations used in hard
+constraints and objective functions, however, may use arbitrary
+integer coefficients.
+
+Minisat+ accepts problem specifications written in the OPB format.
+
+.SH OPTIONS
+.SS "Solver options:"
+.TP
+.BR \-M , \-minisat
+Use MiniSat v1.13 as backend (default)
+.TP
+\.BR \-S , \-satelite
+Use SatELite v1.0 as backend
+.TP
+.BR \-ca , \-adders
+Convert PB\-constrs to clauses through adders.
+.TP
+.BR -cs , -sorters
+Convert PB\-constrs to clauses through sorters.
+.TP
+.BR -cb , \-bdds
+Convert PB\-constrs to clauses through bdds.
+.TP
+.BR \-cm , \-mixed
+Convert PB\-constrs to clauses by a mix of the above. (default)
+.TP
+.BR -ga , -gs , -gb , -gm
+Override conversion for goal function (long name: \fB\-goal\-xxx\fR).
+.TP
+.BR \-w , \-weak\-off
+Clausify with equivalences instead of implications.
+.TP
+\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=\fIn\fR
+Set threshold for preferring sorters to \fIn\fR. Tried after BDDs (default: 20)
+.TP
+\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
+Don't minimize, just give first solution found
+.TP
+\fB\-A\fR, \fB\-all\fR
+Don't minimize, give all solutions
+.TP
+\fB\-goal=\fIn\fR
+Set initial goal limit to \fIn\fR.
+.TP
+\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
+Use old variant of OPB file format.
+
+.SS "Output options:"
+.TP
+\fB\-s\fR, \fB\-satlive\fR
+Turn off SAT competition output.
+.TP
+\fB\-a\fR, \fB\-ansi\fR
+Turn off ANSI codes in output.
+.TP
+\fB\-v\fIn\fR Set verbosity level to \fIn\fR. Possible values for
+\fIn\fR are 1,2,3 (default: 1).
+.TP
+\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.
diff --git a/debian/minisat+.examples b/debian/minisat+.examples
new file mode 100644
index 0000000..3693723
--- /dev/null
+++ b/debian/minisat+.examples
@@ -0,0 +1 @@
+Examples/*
diff --git a/debian/minisat+.install b/debian/minisat+.install
new file mode 100644
index 0000000..1237355
--- /dev/null
+++ b/debian/minisat+.install
@@ -0,0 +1 @@
+minisat+ usr/bin
diff --git a/debian/minisat+.manpages b/debian/minisat+.manpages
new file mode 100644
index 0000000..23189c7
--- /dev/null
+++ b/debian/minisat+.manpages
@@ -0,0 +1 @@
+debian/minisat+.1
diff --git a/debian/rules b/debian/rules
new file mode 100755
index 0000000..5c7237d
--- /dev/null
+++ b/debian/rules
@@ -0,0 +1,10 @@
+#!/usr/bin/make -f
+
+%:
+	dh $@
+
+override_dh_auto_make:
+	make rs
+
+override_dh_auto_clean:
+	make clean
diff --git a/debian/source/format b/debian/source/format
new file mode 100644
index 0000000..163aaf8
--- /dev/null
+++ b/debian/source/format
@@ -0,0 +1 @@
+3.0 (quilt)

-- 
minisat+ packaging



More information about the debian-science-commits mailing list