simplex-glpk with modified glpk for fpgaHEADmaster

1 files changed, 413 insertions, 0 deletions

diff --git a/glpk-5.0/doc/cnfsat.tex b/glpk-5.0/doc/cnfsat.tex
new file mode 100644
index 0000000..4a2c3bb
--- /dev/null
+++ b/glpk-5.0/doc/cnfsat.tex
@@ -0,0 +1,413 @@
+%* cnfsat.tex *%
+
+\documentclass[11pt,draft]{article}
+\usepackage{amssymb}
+\usepackage{indentfirst}
+
+\setlength{\textwidth}{6.5in}
+\setlength{\textheight}{8.5in}
+\setlength{\oddsidemargin}{0in}
+\setlength{\topmargin}{0in}
+\setlength{\headheight}{0in}
+\setlength{\headsep}{0in}
+\setlength{\footskip}{0.5in}
+\setlength{\parindent}{16pt}
+\setlength{\parskip}{5pt}
+\setlength{\topsep}{0pt}
+\setlength{\partopsep}{0pt}
+\setlength{\itemsep}{\parskip}
+\setlength{\parsep}{0pt}
+\setlength{\leftmargini}{\parindent}
+\renewcommand{\labelitemi}{---}
+
+\def\para#1{\noindent{\bf#1}}
+\def\synopsis{\para{Synopsis}}
+\def\description{\para{Description}}
+\def\returns{\para{Returns}}
+
+\newenvironment{retlist}
+{  \def\arraystretch{1.5}
+   \noindent
+   \begin{tabular}{@{}p{1in}@{}p{5.5in}@{}}
+}
+{\end{tabular}}
+
+\begin{document}
+
+\title{\bf CNF Satisfiability Problem}
+
+\author{Andrew Makhorin {\tt<mao@gnu.org>}}
+
+\date{August 2011}
+
+\maketitle
+
+\section{Introduction}
+
+The {\it Satisfiability Problem (SAT)} is a classic combinatorial
+problem. Given a Boolean formula of $n$ variables
+$$f(x_1,x_2,\dots,x_n),\eqno(1.1)$$
+this problem is to find such values of the variables, on which the
+formula takes on the value {\it true}.
+
+The {\it CNF Satisfiability Problem (CNF-SAT)} is a version of the
+Satisfiability Problem, where the Boolean formula (1.1) is specified
+in the {\it Conjunctive Normal Form (CNF)}, that means that it is a
+conjunction of {\it clauses}, where a clause is a disjunction of
+{\it literals}, and a literal is a variable or its negation.
+For example:
+$$(x_1\vee x_2)\;\&\;(\neg x_2\vee x_3\vee\neg x_4)\;\&\;(\neg
+x_1\vee x_4).\eqno(1.2)$$
+Here $x_1$, $x_2$, $x_3$, $x_4$ are Boolean variables to be assigned,
+$\neg$ means
+negation (logical {\it not}), $\vee$ means disjunction (logical
+{\it or}), and $\&$ means conjunction (logical {\it and}). One may
+note that the formula (1.2) is {\it satisfiable}, because on
+$x_1$ = {\it true}, $x_2$ = {\it false}, $x_3$ = {\it false}, and
+$x_4$ = {\it true} it takes on the value {\it true}. If a formula
+is not satisfiable, it is called {\it unsatisfiable}, that means that
+it takes on the value {\it false} on any values of its variables.
+
+Any CNF-SAT problem can be easily translated to a 0-1 programming
+problem as follows.\linebreak A Boolean variable $x$ can be modeled by
+a binary variable in a natural way: $x=1$ means that $x$ takes on the
+value {\it true}, and $x=0$ means that $x$ takes on the value
+{\it false}. Then, if a literal is a negated variable, i.e. $t=\neg x$,
+it can be expressed as $t=1-x$. Since a formula in CNF is a conjunction
+of clauses, to provide its satisfiability we should require all its
+clauses to  take on the value {\it true}. A particular clause is
+a disjunction of literals:
+$$t\vee t'\vee t''\dots ,\eqno(1.3)$$
+so it takes on the value {\it true} iff at least one of its literals
+takes on the value {\it true}, that can be expressed as the following
+inequality constraint:
+$$t+t'+t''+\dots\geq 1.\eqno(1.4)$$
+Note that no objective function is used in this case, because only
+a feasible solution needs to be found.
+
+For example, the formula (1.2) can be translated to the following
+constraints:
+$$\begin{array}{c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c}
+x_1&+&x_2&&&&&\geq&1\\
+&&(1-x_2)&+&x_3&+&(1-x_4)&\geq&1\\
+(1-x_1)&&&&&+&x_4&\geq&1\\
+\end{array}$$
+$$x_1, x_2, x_3, x_4\in\{0,1\}$$
+Carrying out all constant terms to the right-hand side gives
+corresponding 0-1 programming problem in the standard format:
+$$\begin{array}{r@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }r}
+x_1&+&x_2&&&&&\geq&1\\
+&-&x_2&+&x_3&-&x_4&\geq&-1\\
+-x_1&&&&&+&x_4&\geq&0\\
+\end{array}$$
+$$x_1, x_2, x_3, x_4\in\{0,1\}$$
+
+In general case translation of a CNF-SAT problem results in the
+following 0-1 programming problem:
+$$\sum_{j\in J^+_i}x_j-\sum_{j\in J^-_i}x_j\geq 1-|J^-_i|,
+\ \ \ i=1,\dots,m\eqno(1.5)$$
+$$x_j\in\{0,1\},\ \ \ j=1,\dots,n\eqno(1.6)$$
+where $n$ is the number of variables, $m$ is the number of clauses
+(inequality constraints),\linebreak $J^+_i\subseteq\{1,\dots,n\}$ is
+a subset of variables, whose literals in $i$-th clause do not have
+negation, and $J^-_i\subseteq\{1,\dots,n\}$ is a subset of variables,
+whose literals in $i$-th clause are negations of that variables. It is
+assumed that $J^+_i\cap J^-_i=\varnothing$ for all $i$.
+
+\section{GLPK API Routines}
+
+\subsection{glp\_read\_cnfsat --- read CNF-SAT problem data in DIMACS
+format}
+
+\synopsis
+
+\begin{verbatim}
+   int glp_read_cnfsat(glp_prob *P, const char *fname);
+\end{verbatim}
+
+\description
+
+The routine \verb|glp_read_cnfsat| reads the CNF-SAT problem data from
+a text file in DIMACS format and automatically translates the data to
+corresponding 0-1 programming problem instance (1.5)--(1.6).
+
+The parameter \verb|P| specifies the problem object, to which the
+0-1 programming problem instance should be stored. Note that before
+reading data the current content of the problem object is completely
+erased with the routine \verb|glp_erase_prob|.
+
+The character string \verb|fname| specifies the name of a text file
+to be read in. (If the file name ends with the suffix `\verb|.gz|',
+the file is assumed to be compressed, in which case the routine
+decompresses it ``on the fly''.)
+
+\newpage
+
+\returns
+
+If the operation was successful, the routine returns zero. Otherwise,
+it prints an error message and returns non-zero.
+
+\para{DIMACS CNF-SAT problem format}\footnote{This material is based on
+the paper ``Satisfiability Suggested Format'', which is publicly
+available at {\tt http://dimacs.rutgers.edu/}.}
+
+The DIMACS input file is a plain ASCII text file. It contains lines of
+several types described below. A line is terminated with an end-of-line
+character. Fields in each line are separated by at least one blank
+space.
+
+\para{Comment lines.} Comment lines give human-readable information
+about the file and are ignored by programs. Comment lines can appear
+anywhere in the file. Each comment line begins with a lower-case
+character \verb|c|.
+
+\begin{verbatim}
+   c This is a comment line
+\end{verbatim}
+
+\para{Problem line.} There is one problem line per data file. The
+problem line must appear before any clause lines. It has the following
+format:
+
+\begin{verbatim}
+   p cnf VARIABLES CLAUSES
+\end{verbatim}
+
+\noindent
+The lower-case character \verb|p| signifies that this is a problem
+line. The three character problem designator \verb|cnf| identifies the
+file as containing specification information for the CNF-SAT problem.
+The \verb|VARIABLES| field contains an integer value specifying $n$,
+the number of variables in the instance. The \verb|CLAUSES| field
+contains an integer value specifying $m$, the number of clauses in the
+instance.
+
+\para{Clauses.} The clauses appear immediately after the problem
+line. The variables are assumed to be numbered from 1 up to $n$. It is
+not necessary that every variable appears in the instance. Each clause
+is represented by a sequence of numbers separated by either a space,
+tab, or new-line character. The non-negated version of a variable $j$
+is represented by $j$; the negated version is represented by $-j$. Each
+clause is terminated by the value 0. Unlike many formats that represent
+the end of a clause by a new-line character, this format allows clauses
+to be on multiple lines.
+
+\para{Example.} Below here is an example of the data file in DIMACS
+format corresponding to the CNF-SAT problem (1.2).
+
+\begin{footnotesize}
+\begin{verbatim}
+c sample.cnf
+c
+c This is an example of the CNF-SAT problem data
+c in DIMACS format.
+c
+p cnf 4 3
+1 2 0
+-4 3
+-2 0
+-1 4 0
+c
+c eof
+\end{verbatim}
+\end{footnotesize}
+
+\newpage
+
+\subsection{glp\_check\_cnfsat --- check for CNF-SAT problem instance}
+
+\synopsis
+
+\begin{verbatim}
+   int glp_check_cnfsat(glp\_prob *P);
+\end{verbatim}
+
+\description
+
+The routine \verb|glp_check_cnfsat| checks if the specified problem
+object \verb|P| contains a 0-1 programming problem instance in the
+format (1.5)--(1.6) and therefore encodes a CNF-SAT problem instance.
+
+\returns
+
+If the specified problem object has the format (1.5)--(1.6), the
+routine returns zero, otherwise non-zero.
+
+\subsection{glp\_write\_cnfsat --- write CNF-SAT problem data in DIMACS
+format}
+
+\synopsis
+
+\begin{verbatim}
+   int glp_write_cnfsat(glp_prob *P, const char *fname);
+\end{verbatim}
+
+\description
+
+The routine \verb|glp_write_cnfsat| automatically translates the
+specified 0-1 programming problem instance (1.5)--(1.6) to a CNF-SAT
+problem instance and writes the problem data to a text file in DIMACS
+format.
+
+The parameter \verb|P| is the problem object, which should specify
+a 0-1 programming problem instance in the format (1.5)--(1.6).
+
+The character string \verb|fname| specifies a name of the output text
+file to be written. (If the file name ends with suffix `\verb|.gz|',
+the file is assumed to be compressed, in which case the routine
+performs automatic compression on writing that file.)
+
+\returns
+
+If the operation was successful, the routine returns zero. Otherwise,
+it prints an error message and returns non-zero.
+
+\subsection{glp\_minisat1 --- solve CNF-SAT problem instance with
+MiniSat solver}
+
+\synopsis
+
+\begin{verbatim}
+   int glp_minisat1(glp_prob *P);
+\end{verbatim}
+
+\description
+
+The routine \verb|glp_minisat1| is a driver to MiniSat, a CNF-SAT
+solver developed by Niklas E\'en and Niklas S\"orensson, Chalmers
+University of Technology, Sweden.\footnote{The MiniSat software module
+is {\it not} part of GLPK, but is used with GLPK and included in the
+distribution.}
+
+\newpage
+
+It is assumed that the specified problem object \verb|P| contains
+a 0-1 programming problem instance in the format (1.5)--(1.6) and
+therefore encodes a CNF-SAT problem instance.
+
+If the problem instance has been successfully solved to the end, the
+routine \verb|glp_minisat1| returns 0. In this case the routine
+\verb|glp_mip_status| can be used to determine the solution status:
+
+\begin{itemize}
+\item {\tt GLP\_OPT} means that the solver found an integer feasible
+solution and therefore the corresponding CNF-SAT instance is
+satisfiable;
+
+\item {\tt GLP\_NOFEAS} means that no integer feasible solution exists
+and therefore the corresponding CNF-SAT instance is unsatisfiable.
+\end{itemize}
+
+If an integer feasible solution was found, corresponding values of
+binary variables can be retrieved with the routine
+\verb|glp_mip_col_val|.
+
+\returns
+
+\begin{retlist}
+0 & The MIP problem instance has been successfully solved. (This code
+does {\it not} necessarily mean that the solver has found feasible
+solution. It only means that the solution process was successful.)\\
+
+{\tt GLP\_EDATA} & The specified problem object contains a MIP
+instance which does {\it not} have the format (1.5)--(1.6).\\
+
+{\tt GLP\_EFAIL} & The solution process was unsuccessful because of
+the solver failure.\\
+\end{retlist}
+
+\subsection{glp\_intfeas1 --- solve integer feasibility problem}
+
+\synopsis
+
+\begin{verbatim}
+   int glp_intfeas1(glp_prob *P, int use_bound, int obj_bound);
+\end{verbatim}
+
+\description
+
+The routine \verb|glp_intfeas1| is a tentative implementation of
+an integer feasibility solver based on a CNF-SAT solver (currently
+it is MiniSat; see Subsection 2.4).
+
+If the parameter \verb|use_bound| is zero, the routine searches for
+{\it any} integer feasibile solution to the specified integer
+programming problem. Note that in this case the objective function is
+ignored.
+
+If the parameter \verb|use_bound| is non-zero, the routine searches for
+an integer feasible solution, which provides a value of the objective
+function not worse than \verb|obj_bound|. In other word, the parameter
+\verb|obj_bound| specifies an upper (in case of minimization) or lower
+(in case of maximization) bound to the objective function.
+
+If the specified problem has been successfully solved to the end, the
+routine \verb|glp_intfeas1| returns 0. In this case the routine
+\verb|glp_mip_status| can be used to determine the solution status:
+
+\begin{itemize}
+\item {\tt GLP\_FEAS} means that the solver found an integer feasible
+solution;
+
+\item {\tt GLP\_NOFEAS} means that the problem has no integer feasible
+solution (if {\tt use\_bound} is zero) or it has no integer feasible
+solution, which is not worse than {\tt obj\_bound} (if {\tt use\_bound}
+is non-zero).
+\end{itemize}
+
+\newpage
+
+If an integer feasible solution was found, corresponding values of
+variables (columns) can be retrieved with the routine
+\verb|glp_mip_col_val|.
+
+\para{Usage Notes}
+
+The integer programming problem specified by the parameter \verb|P|
+should satisfy to the following requirements:
+
+\begin{enumerate}
+\item All variables (columns) should be either binary ({\tt GLP\_BV})
+or fixed at integer values ({\tt GLP\_FX}).
+
+\item All constraint and objective coefficients should be integer
+numbers in the range\linebreak $[-2^{31},\ +2^{31}-1]$.
+\end{enumerate}
+
+Though there are no special requirements to the constraints,
+currently the routine \verb|glp_intfeas1| is efficient mainly for
+problems, where most constraints (rows) fall into the following three
+classes:
+
+\begin{enumerate}
+\item Covering inequalities
+$$\sum_{j}t_j\geq 1,$$
+where $t_j=x_j$ or $t_j=1-x_j$, $x_j$ is a binary variable.
+
+\item Packing inequalities
+$$\sum_{j}t_j\leq 1.$$
+
+\item Partitioning equalities (SOS1 constraints)
+$$\sum_{j}t_j=1.$$
+\end{enumerate}
+
+\returns
+
+\begin{retlist}
+0 & The problem has been successfully solved. (This code does
+{\it not} necessarily mean that the solver has found an integer
+feasible solution. It only means that the solution process was
+successful.) \\
+
+{\tt GLP\_EDATA} & The specified problem object does not satisfy
+to the requirements listed in Paragraph `Usage Notes'. \\
+
+{\tt GLP\_ERANGE} & An integer overflow occured on translating the
+specified problem to a CNF-SAT problem. \\
+
+{\tt GLP\_EFAIL} & The solution process was unsuccessful because of
+the solver failure. \\
+\end{retlist}
+
+\end{document}