1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/deps/glpk/doc/cnfsat.tex	Sun Nov 06 20:59:10 2011 +0100
     1.3 @@ -0,0 +1,380 @@
     1.4 +%* cnfsat.tex *%
     1.5 +
     1.6 +\documentclass[11pt,draft]{article}
     1.7 +
     1.8 +\begin{document}
     1.9 +
    1.10 +\title{CNF Satisfiability Problem}
    1.11 +
    1.12 +\author{Andrew Makhorin {\tt<mao@gnu.org>}}
    1.13 +
    1.14 +\date{August 2011}
    1.15 +
    1.16 +\maketitle
    1.17 +
    1.18 +\section{Introduction}
    1.19 +
    1.20 +The {\it Satisfiability Problem (SAT)} is a classic combinatorial
    1.21 +problem. Given a Boolean formula of $n$ variables
    1.22 +$$f(x_1,x_2,\dots,x_n),\eqno(1.1)$$
    1.23 +this problem is to find such values of the variables, on which the
    1.24 +formula takes on the value {\it true}.
    1.25 +
    1.26 +The {\it CNF Satisfiability Problem (CNF-SAT)} is a version of the
    1.27 +Satisfiability Problem, where the Boolean formula (1.1) is specified
    1.28 +in the {\it Conjunctive Normal Form (CNF)}, that means that it is a
    1.29 +conjunction of {\it clauses}, where a clause is a disjunction of
    1.30 +{\it literals}, and a literal is a variable or its negation.
    1.31 +For example:
    1.32 +$$(x_1\vee x_2)\;\&\;(\neg x_2\vee x_3\vee\neg x_4)\;\&\;(\neg
    1.33 +x_1\vee x_4).\eqno(1.2)$$
    1.34 +Here $x_1$, $x_2$, $x_3$, $x_4$ are Boolean variables to be assigned,
    1.35 +$\neg$ means
    1.36 +negation (logical {\it not}), $\vee$ means disjunction (logical
    1.37 +{\it or}), and $\&$ means conjunction (logical {\it and}). One may
    1.38 +note that the formula (1.2) is {\it satisfiable}, because on
    1.39 +$x_1$ = {\it true}, $x_2$ = {\it false}, $x_3$ = {\it false}, and
    1.40 +$x_4$ = {\it true} it takes on the value {\it true}. If a formula
    1.41 +is not satisfiable, it is called {\it unsatisfiable}, that means that
    1.42 +it takes on the value {\it false} on any values of its variables.
    1.43 +
    1.44 +Any CNF-SAT problem can be easily translated to a 0-1 programming
    1.45 +problem as follows. A Boolean variable $x$ can be modeled by a binary
    1.46 +variable in a natural way: $x=1$ means that $x$ takes on the value
    1.47 +{\it true}, and $x=0$ means that $x$ takes on the value {\it false}.
    1.48 +Then, if a literal is a negated variable, i.e. $t=\neg x$, it can
    1.49 +be expressed as $t=1-x$. Since a formula in CNF is a conjunction of
    1.50 +clauses, to provide its satisfiability we should require all its
    1.51 +clauses to  take on the value {\it true}. A particular clause is
    1.52 +a disjunction of literals:
    1.53 +$$t\vee t'\vee t''\dots ,\eqno(1.3)$$
    1.54 +so it takes on the value {\it true} iff at least one of its literals
    1.55 +takes on the value {\it true}, that can be expressed as the following
    1.56 +inequality constraint:
    1.57 +$$t+t'+t''+\dots\geq 1.\eqno(1.4)$$
    1.58 +Note that no objective function is used in this case, because only
    1.59 +a feasible solution needs to be found.
    1.60 +
    1.61 +For example, the formula (1.2) can be translated to the following
    1.62 +constraints:
    1.63 +$$\begin{array}{c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c}
    1.64 +x_1&+&x_2&&&&&\geq&1\\
    1.65 +&&(1-x_2)&+&x_3&+&(1-x_4)&\geq&1\\
    1.66 +(1-x_1)&&&&&+&x_4&\geq&1\\
    1.67 +\end{array}$$
    1.68 +$$x_1, x_2, x_3, x_4\in\{0,1\}$$
    1.69 +Carrying out all constant terms to the right-hand side gives
    1.70 +corresponding 0-1 programming problem in the standard format:
    1.71 +$$\begin{array}{r@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }r}
    1.72 +x_1&+&x_2&&&&&\geq&1\\
    1.73 +&-&x_2&+&x_3&-&x_4&\geq&-1\\
    1.74 +-x_1&&&&&+&x_4&\geq&0\\
    1.75 +\end{array}$$
    1.76 +$$x_1, x_2, x_3, x_4\in\{0,1\}$$
    1.77 +
    1.78 +In general case translation of a CNF-SAT problem results in the
    1.79 +following 0-1 programming problem:
    1.80 +$$\sum_{j\in J^+_i}x_j-\sum_{j\in J^-_i}x_j\geq 1-|J^-_i|,
    1.81 +\ \ \ i=1,\dots,m\eqno(1.5)$$
    1.82 +$$x_j\in\{0,1\},\ \ \ j=1,\dots,n\eqno(1.6)$$
    1.83 +where $n$ is the number of variables, $m$ is the number of clauses
    1.84 +(inequality constraints), $J^+_i\subseteq\{1,\dots,n\}$ is a subset
    1.85 +of variables, whose literals in $i$-th clause do not have negation,
    1.86 +and $J^-_i\subseteq\{1,\dots,n\}$ is a subset of variables, whose
    1.87 +literals in $i$-th clause are negations of that variables. It is
    1.88 +assumed that $J^+_i\cap J^-_i=\emptyset$ for all $i$.
    1.89 +
    1.90 +\newpage
    1.91 +
    1.92 +\section{GLPK API Routines}
    1.93 +
    1.94 +\subsection{glp\_read\_cnfsat---read CNF-SAT problem data in\\DIMACS
    1.95 +format}
    1.96 +
    1.97 +\subsubsection*{Synopsis}
    1.98 +
    1.99 +\begin{verbatim}
   1.100 +int glp_read_cnfsat(glp_prob *P, const char *fname);
   1.101 +\end{verbatim}
   1.102 +
   1.103 +\subsubsection*{Description}
   1.104 +
   1.105 +The routine \verb|glp_read_cnfsat| reads the CNF-SAT problem data from
   1.106 +a text file in DIMACS format and automatically translates the data to
   1.107 +corresponding 0-1 programming problem instance (1.5)--(1.6).
   1.108 +
   1.109 +The parameter \verb|P| specifies the problem object, to which the
   1.110 +0-1 programming problem instance should be stored. Note that before
   1.111 +reading data the current content of the problem object is completely
   1.112 +erased with the routine \verb|glp_erase_prob|.
   1.113 +
   1.114 +The character string \verb|fname| specifies the name of a text file
   1.115 +to be read in. (If the file name ends with the suffix `\verb|.gz|',
   1.116 +the file is assumed to be compressed, in which case the routine
   1.117 +decompresses it ``on the fly''.)
   1.118 +
   1.119 +\subsubsection*{Returns}
   1.120 +
   1.121 +If the operation was successful, the routine returns zero. Otherwise,
   1.122 +it prints an error message and returns non-zero.
   1.123 +
   1.124 +\subsubsection*{DIMACS CNF-SAT problem format\footnote{This material
   1.125 +is based on the paper ``Satisfiability Suggested Format'', which is
   1.126 +publicly available at {\tt http://dimacs.rutgers.edu/}.}}
   1.127 +
   1.128 +The DIMACS input file is a plain ASCII text file. It contains lines of
   1.129 +several types described below. A line is terminated with an end-of-line
   1.130 +character. Fields in each line are separated by at least one blank
   1.131 +space.
   1.132 +
   1.133 +\paragraph{Comment lines.} Comment lines give human-readable
   1.134 +information about the file and are ignored by programs. Comment lines
   1.135 +can appear anywhere in the file. Each comment line begins with a
   1.136 +lower-case character \verb|c|.
   1.137 +
   1.138 +\begin{verbatim}
   1.139 +   c This is a comment line
   1.140 +\end{verbatim}
   1.141 +
   1.142 +\newpage
   1.143 +
   1.144 +\paragraph{Problem line.} There is one problem line per data file. The
   1.145 +problem line must appear before any clause lines. It has the following
   1.146 +format:
   1.147 +
   1.148 +\begin{verbatim}
   1.149 +   p cnf VARIABLES CLAUSES
   1.150 +\end{verbatim}
   1.151 +
   1.152 +\noindent
   1.153 +The lower-case character \verb|p| signifies that this is a problem
   1.154 +line. The three character problem designator \verb|cnf| identifies the
   1.155 +file as containing specification information for the CNF-SAT problem.
   1.156 +The \verb|VARIABLES| field contains an integer value specifying $n$,
   1.157 +the number of variables in the instance. The \verb|CLAUSES| field
   1.158 +contains an integer value specifying $m$, the number of clauses in the
   1.159 +instance.
   1.160 +
   1.161 +\paragraph{Clauses.} The clauses appear immediately after the problem
   1.162 +line. The variables are assumed to be numbered from 1 up to $n$. It is
   1.163 +not necessary that every variable appears in the instance. Each clause
   1.164 +is represented by a sequence of numbers separated by either a space,
   1.165 +tab, or new-line character. The non-negated version of a variable $j$
   1.166 +is represented by $j$; the negated version is represented by $-j$. Each
   1.167 +clause is terminated by the value 0. Unlike many formats that represent
   1.168 +the end of a clause by a new-line character, this format allows clauses
   1.169 +to be on multiple lines.
   1.170 +
   1.171 +\paragraph{Example.} Below here is an example of the data file in
   1.172 +DIMACS format corresponding to the CNF-SAT problem (1.2).
   1.173 +
   1.174 +\begin{footnotesize}
   1.175 +\begin{verbatim}
   1.176 +c sample.cnf
   1.177 +c
   1.178 +c This is an example of the CNF-SAT problem data
   1.179 +c in DIMACS format.
   1.180 +c
   1.181 +p cnf 4 3
   1.182 +1 2 0
   1.183 +-4 3
   1.184 +-2 0
   1.185 +-1 4 0
   1.186 +c
   1.187 +c eof
   1.188 +\end{verbatim}
   1.189 +\end{footnotesize}
   1.190 +
   1.191 +\newpage
   1.192 +
   1.193 +\subsection{glp\_check\_cnfsat---check for CNF-SAT problem instance}
   1.194 +
   1.195 +\subsubsection*{Synopsis}
   1.196 +
   1.197 +\begin{verbatim}
   1.198 +int glp_check_cnfsat(glp_prob *P);
   1.199 +\end{verbatim}
   1.200 +
   1.201 +\subsubsection*{Description}
   1.202 +
   1.203 +The routine \verb|glp_check_cnfsat| checks if the specified problem
   1.204 +object \verb|P| contains a 0-1 programming problem instance in the
   1.205 +format (1.5)--(1.6) and therefore encodes a CNF-SAT problem instance.
   1.206 +
   1.207 +\subsubsection*{Returns}
   1.208 +
   1.209 +If the specified problem object has the format (1.5)--(1.6), the
   1.210 +routine returns zero, otherwise non-zero.
   1.211 +
   1.212 +\subsection{glp\_write\_cnfsat---write CNF-SAT problem data in\\DIMACS
   1.213 +format}
   1.214 +
   1.215 +\subsubsection*{Synopsis}
   1.216 +
   1.217 +\begin{verbatim}
   1.218 +int glp_write_cnfsat(glp_prob *P, const char *fname);
   1.219 +\end{verbatim}
   1.220 +
   1.221 +\subsubsection*{Description}
   1.222 +
   1.223 +The routine \verb|glp_write_cnfsat| automatically translates the
   1.224 +specified 0-1 programming problem instance (1.5)--(1.6) to a CNF-SAT
   1.225 +problem instance and writes the problem data to a text file in DIMACS
   1.226 +format.
   1.227 +
   1.228 +The parameter \verb|P| is the problem object, which should specify
   1.229 +a 0-1 programming problem instance in the format (1.5)--(1.6).
   1.230 +
   1.231 +The character string \verb|fname| specifies a name of the output text
   1.232 +file to be written. (If the file name ends with suffix `\verb|.gz|',
   1.233 +the file is assumed to be compressed, in which case the routine
   1.234 +performs automatic compression on writing that file.)
   1.235 +
   1.236 +\subsubsection*{Returns}
   1.237 +
   1.238 +If the operation was successful, the routine returns zero. Otherwise,
   1.239 +it prints an error message and returns non-zero.
   1.240 +
   1.241 +\newpage
   1.242 +
   1.243 +\subsection{glp\_minisat1---solve CNF-SAT problem instance with\\
   1.244 +MiniSat solver}
   1.245 +
   1.246 +\subsubsection*{Synopsis}
   1.247 +
   1.248 +\begin{verbatim}
   1.249 +int glp_minisat1(glp_prob *P);
   1.250 +\end{verbatim}
   1.251 +
   1.252 +\subsubsection*{Description}
   1.253 +
   1.254 +The routine \verb|glp_minisat1| is a driver to MiniSat, a CNF-SAT
   1.255 +solver developed by Niklas E\'en and Niklas S\"orensson, Chalmers
   1.256 +University of Technology, Sweden.\footnote{The MiniSat software module
   1.257 +is {\it not} part of GLPK, but is used with GLPK and included in the
   1.258 +distribution.}
   1.259 +
   1.260 +It is assumed that the specified problem object \verb|P| contains
   1.261 +a 0-1 programming problem instance in the format (1.5)--(1.6) and
   1.262 +therefore encodes a CNF-SAT problem instance.
   1.263 +
   1.264 +If the problem instance has been successfully solved to the end, the
   1.265 +routine \verb|glp_minisat1| returns 0. In this case the routine
   1.266 +\verb|glp_mip_status| can be used to determine the solution status:
   1.267 +
   1.268 +\verb|GLP_OPT| means that the solver found an integer feasible
   1.269 +solution and therefore the corresponding CNF-SAT instance is
   1.270 +satisfiable;
   1.271 +
   1.272 +\verb|GLP_NOFEAS| means that no integer feasible solution exists and
   1.273 +therefore the corresponding CNF-SAT instance is unsatisfiable.
   1.274 +
   1.275 +If an integer feasible solution was found, corresponding values of
   1.276 +binary variables can be retrieved with the routine
   1.277 +\verb|glp_mip_col_val|.
   1.278 +
   1.279 +\subsubsection*{Returns}
   1.280 +
   1.281 +\begin{tabular}{@{}p{25mm}p{97.3mm}@{}}
   1.282 +0 & The MIP problem instance has been successfully solved. (This code
   1.283 +does {\it not} necessarily mean that the solver has found feasible
   1.284 +solution. It only means that the solution process was successful.)\\
   1.285 +\verb|GLP_EDATA| & The specified problem object contains a MIP instance
   1.286 +which does {\it not} have the format (1.5)--(1.6).\\
   1.287 +\verb|GLP_EFAIL| & The solution process was unsuccessful because of the
   1.288 +solver failure.\\
   1.289 +\end{tabular}
   1.290 +
   1.291 +\newpage
   1.292 +
   1.293 +\subsection{glp\_intfeas1---solve integer feasibility problem}
   1.294 +
   1.295 +\subsubsection*{Synopsis}
   1.296 +
   1.297 +\begin{verbatim}
   1.298 +int glp_intfeas1(glp_prob *P, int use_bound, int obj_bound);
   1.299 +\end{verbatim}
   1.300 +
   1.301 +\subsubsection*{Description}
   1.302 +
   1.303 +The routine \verb|glp_intfeas1| is a tentative implementation of
   1.304 +an integer feasibility solver based on a CNF-SAT solver (currently
   1.305 +it is MiniSat; see Subsection 2.4).
   1.306 +
   1.307 +If the parameter \verb|use_bound| is zero, the routine searches for
   1.308 +{\it any} integer feasibile solution to the specified integer
   1.309 +programming problem. Note that in this case the objective function is
   1.310 +ignored.
   1.311 +
   1.312 +If the parameter \verb|use_bound| is non-zero, the routine searches for
   1.313 +an integer feasible solution, which provides a value of the objective
   1.314 +function not worse than \verb|obj_bound|. In other word, the parameter
   1.315 +\verb|obj_bound| specifies an upper (in case of minimization) or lower
   1.316 +(in case of maximization) bound to the objective function.
   1.317 +
   1.318 +If the specified problem has been successfully solved to the end, the
   1.319 +routine \verb|glp_intfeas1| returns 0. In this case the routine
   1.320 +\verb|glp_mip_status| can be used to determine the solution status:
   1.321 +
   1.322 +\begin{itemize}
   1.323 +\item {\tt GLP\_FEAS} means that the solver found an integer feasible
   1.324 +solution;
   1.325 +
   1.326 +\item {\tt GLP\_NOFEAS} means that the problem has no integer feasible
   1.327 +solution (if {\tt use\_bound} is zero) or it has no integer feasible
   1.328 +solution, which is not worse than {\tt obj\_bound} (if {\tt use\_bound}
   1.329 +is non-zero).
   1.330 +\end{itemize}
   1.331 +
   1.332 +If an integer feasible solution was found, corresponding values of
   1.333 +variables (columns) can be retrieved with the routine
   1.334 +\verb|glp_mip_col_val|.
   1.335 +
   1.336 +\subsubsection*{Usage Notes}
   1.337 +
   1.338 +The integer programming problem specified by the parameter \verb|P|
   1.339 +should satisfy to the following requirements:
   1.340 +
   1.341 +\begin{enumerate}
   1.342 +\item All variables (columns) should be either binary ({\tt GLP\_BV})
   1.343 +or fixed at integer values ({\tt GLP\_FX}).
   1.344 +
   1.345 +\item All constraint and objective coefficients should be integer
   1.346 +numbers in the range $[-2^{31},\ +2^{31}-1]$.
   1.347 +\end{enumerate}
   1.348 +
   1.349 +Though there are no special requirements to the constraints,
   1.350 +currently the routine \verb|glp_intfeas1| is efficient mainly for
   1.351 +problems, where most constraints (rows) fall into the following three
   1.352 +classes:
   1.353 +
   1.354 +\begin{enumerate}
   1.355 +\item Covering inequalities
   1.356 +$$\sum_{j}t_j\geq 1,$$
   1.357 +where $t_j=x_j$ or $t_j=1-x_j$, $x_j$ is a binary variable.
   1.358 +
   1.359 +\item Packing inequalities
   1.360 +$$\sum_{j}t_j\leq 1.$$
   1.361 +
   1.362 +\item Partitioning equalities (SOS1 constraints)
   1.363 +$$\sum_{j}t_j=1.$$
   1.364 +\end{enumerate}
   1.365 +
   1.366 +\subsubsection*{Returns}
   1.367 +
   1.368 +\begin{tabular}{@{}p{25mm}p{97.3mm}@{}}
   1.369 +0 & The problem has been successfully solved. (This code does {\it not}
   1.370 +necessarily mean that the solver has found an integer feasible solution.
   1.371 +It only means that the solution process was successful.)\\
   1.372 +
   1.373 +\verb|GLP_EDATA| & The specified problem object does not satisfy to the
   1.374 +requirements listed in Paragraph `Usage Notes'.\\
   1.375 +
   1.376 +\verb|GLP_ERANGE| & An integer overflow occured on translating the
   1.377 +specified problem to a CNF-SAT problem.\\
   1.378 +
   1.379 +\verb|GLP_EFAIL| & The solution process was unsuccessful because of the
   1.380 +solver failure.\\
   1.381 +\end{tabular}
   1.382 +
   1.383 +\end{document}