lemon-project-template-glpk

annotate deps/glpk/doc/cnfsat.tex @ 11:4fc6ad2fb8a6

find changesets by author, revision, files, or words in the commit message
Test GLPK in src/main.cc
author Alpar Juttner <alpar@cs.elte.hu>
date Sun, 06 Nov 2011 21:43:29 +0100
parents
children
rev   line source
alpar@9 1 %* cnfsat.tex *%
alpar@9 2
alpar@9 3 \documentclass[11pt,draft]{article}
alpar@9 4
alpar@9 5 \begin{document}
alpar@9 6
alpar@9 7 \title{CNF Satisfiability Problem}
alpar@9 8
alpar@9 9 \author{Andrew Makhorin {\tt<mao@gnu.org>}}
alpar@9 10
alpar@9 11 \date{August 2011}
alpar@9 12
alpar@9 13 \maketitle
alpar@9 14
alpar@9 15 \section{Introduction}
alpar@9 16
alpar@9 17 The {\it Satisfiability Problem (SAT)} is a classic combinatorial
alpar@9 18 problem. Given a Boolean formula of $n$ variables
alpar@9 19 $$f(x_1,x_2,\dots,x_n),\eqno(1.1)$$
alpar@9 20 this problem is to find such values of the variables, on which the
alpar@9 21 formula takes on the value {\it true}.
alpar@9 22
alpar@9 23 The {\it CNF Satisfiability Problem (CNF-SAT)} is a version of the
alpar@9 24 Satisfiability Problem, where the Boolean formula (1.1) is specified
alpar@9 25 in the {\it Conjunctive Normal Form (CNF)}, that means that it is a
alpar@9 26 conjunction of {\it clauses}, where a clause is a disjunction of
alpar@9 27 {\it literals}, and a literal is a variable or its negation.
alpar@9 28 For example:
alpar@9 29 $$(x_1\vee x_2)\;\&\;(\neg x_2\vee x_3\vee\neg x_4)\;\&\;(\neg
alpar@9 30 x_1\vee x_4).\eqno(1.2)$$
alpar@9 31 Here $x_1$, $x_2$, $x_3$, $x_4$ are Boolean variables to be assigned,
alpar@9 32 $\neg$ means
alpar@9 33 negation (logical {\it not}), $\vee$ means disjunction (logical
alpar@9 34 {\it or}), and $\&$ means conjunction (logical {\it and}). One may
alpar@9 35 note that the formula (1.2) is {\it satisfiable}, because on
alpar@9 36 $x_1$ = {\it true}, $x_2$ = {\it false}, $x_3$ = {\it false}, and
alpar@9 37 $x_4$ = {\it true} it takes on the value {\it true}. If a formula
alpar@9 38 is not satisfiable, it is called {\it unsatisfiable}, that means that
alpar@9 39 it takes on the value {\it false} on any values of its variables.
alpar@9 40
alpar@9 41 Any CNF-SAT problem can be easily translated to a 0-1 programming
alpar@9 42 problem as follows. A Boolean variable $x$ can be modeled by a binary
alpar@9 43 variable in a natural way: $x=1$ means that $x$ takes on the value
alpar@9 44 {\it true}, and $x=0$ means that $x$ takes on the value {\it false}.
alpar@9 45 Then, if a literal is a negated variable, i.e. $t=\neg x$, it can
alpar@9 46 be expressed as $t=1-x$. Since a formula in CNF is a conjunction of
alpar@9 47 clauses, to provide its satisfiability we should require all its
alpar@9 48 clauses to take on the value {\it true}. A particular clause is
alpar@9 49 a disjunction of literals:
alpar@9 50 $$t\vee t'\vee t''\dots ,\eqno(1.3)$$
alpar@9 51 so it takes on the value {\it true} iff at least one of its literals
alpar@9 52 takes on the value {\it true}, that can be expressed as the following
alpar@9 53 inequality constraint:
alpar@9 54 $$t+t'+t''+\dots\geq 1.\eqno(1.4)$$
alpar@9 55 Note that no objective function is used in this case, because only
alpar@9 56 a feasible solution needs to be found.
alpar@9 57
alpar@9 58 For example, the formula (1.2) can be translated to the following
alpar@9 59 constraints:
alpar@9 60 $$\begin{array}{c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c}
alpar@9 61 x_1&+&x_2&&&&&\geq&1\\
alpar@9 62 &&(1-x_2)&+&x_3&+&(1-x_4)&\geq&1\\
alpar@9 63 (1-x_1)&&&&&+&x_4&\geq&1\\
alpar@9 64 \end{array}$$
alpar@9 65 $$x_1, x_2, x_3, x_4\in\{0,1\}$$
alpar@9 66 Carrying out all constant terms to the right-hand side gives
alpar@9 67 corresponding 0-1 programming problem in the standard format:
alpar@9 68 $$\begin{array}{r@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }r}
alpar@9 69 x_1&+&x_2&&&&&\geq&1\\
alpar@9 70 &-&x_2&+&x_3&-&x_4&\geq&-1\\
alpar@9 71 -x_1&&&&&+&x_4&\geq&0\\
alpar@9 72 \end{array}$$
alpar@9 73 $$x_1, x_2, x_3, x_4\in\{0,1\}$$
alpar@9 74
alpar@9 75 In general case translation of a CNF-SAT problem results in the
alpar@9 76 following 0-1 programming problem:
alpar@9 77 $$\sum_{j\in J^+_i}x_j-\sum_{j\in J^-_i}x_j\geq 1-|J^-_i|,
alpar@9 78 \ \ \ i=1,\dots,m\eqno(1.5)$$
alpar@9 79 $$x_j\in\{0,1\},\ \ \ j=1,\dots,n\eqno(1.6)$$
alpar@9 80 where $n$ is the number of variables, $m$ is the number of clauses
alpar@9 81 (inequality constraints), $J^+_i\subseteq\{1,\dots,n\}$ is a subset
alpar@9 82 of variables, whose literals in $i$-th clause do not have negation,
alpar@9 83 and $J^-_i\subseteq\{1,\dots,n\}$ is a subset of variables, whose
alpar@9 84 literals in $i$-th clause are negations of that variables. It is
alpar@9 85 assumed that $J^+_i\cap J^-_i=\emptyset$ for all $i$.
alpar@9 86
alpar@9 87 \newpage
alpar@9 88
alpar@9 89 \section{GLPK API Routines}
alpar@9 90
alpar@9 91 \subsection{glp\_read\_cnfsat---read CNF-SAT problem data in\\DIMACS
alpar@9 92 format}
alpar@9 93
alpar@9 94 \subsubsection*{Synopsis}
alpar@9 95
alpar@9 96 \begin{verbatim}
alpar@9 97 int glp_read_cnfsat(glp_prob *P, const char *fname);
alpar@9 98 \end{verbatim}
alpar@9 99
alpar@9 100 \subsubsection*{Description}
alpar@9 101
alpar@9 102 The routine \verb|glp_read_cnfsat| reads the CNF-SAT problem data from
alpar@9 103 a text file in DIMACS format and automatically translates the data to
alpar@9 104 corresponding 0-1 programming problem instance (1.5)--(1.6).
alpar@9 105
alpar@9 106 The parameter \verb|P| specifies the problem object, to which the
alpar@9 107 0-1 programming problem instance should be stored. Note that before
alpar@9 108 reading data the current content of the problem object is completely
alpar@9 109 erased with the routine \verb|glp_erase_prob|.
alpar@9 110
alpar@9 111 The character string \verb|fname| specifies the name of a text file
alpar@9 112 to be read in. (If the file name ends with the suffix `\verb|.gz|',
alpar@9 113 the file is assumed to be compressed, in which case the routine
alpar@9 114 decompresses it ``on the fly''.)
alpar@9 115
alpar@9 116 \subsubsection*{Returns}
alpar@9 117
alpar@9 118 If the operation was successful, the routine returns zero. Otherwise,
alpar@9 119 it prints an error message and returns non-zero.
alpar@9 120
alpar@9 121 \subsubsection*{DIMACS CNF-SAT problem format\footnote{This material
alpar@9 122 is based on the paper ``Satisfiability Suggested Format'', which is
alpar@9 123 publicly available at {\tt http://dimacs.rutgers.edu/}.}}
alpar@9 124
alpar@9 125 The DIMACS input file is a plain ASCII text file. It contains lines of
alpar@9 126 several types described below. A line is terminated with an end-of-line
alpar@9 127 character. Fields in each line are separated by at least one blank
alpar@9 128 space.
alpar@9 129
alpar@9 130 \paragraph{Comment lines.} Comment lines give human-readable
alpar@9 131 information about the file and are ignored by programs. Comment lines
alpar@9 132 can appear anywhere in the file. Each comment line begins with a
alpar@9 133 lower-case character \verb|c|.
alpar@9 134
alpar@9 135 \begin{verbatim}
alpar@9 136 c This is a comment line
alpar@9 137 \end{verbatim}
alpar@9 138
alpar@9 139 \newpage
alpar@9 140
alpar@9 141 \paragraph{Problem line.} There is one problem line per data file. The
alpar@9 142 problem line must appear before any clause lines. It has the following
alpar@9 143 format:
alpar@9 144
alpar@9 145 \begin{verbatim}
alpar@9 146 p cnf VARIABLES CLAUSES
alpar@9 147 \end{verbatim}
alpar@9 148
alpar@9 149 \noindent
alpar@9 150 The lower-case character \verb|p| signifies that this is a problem
alpar@9 151 line. The three character problem designator \verb|cnf| identifies the
alpar@9 152 file as containing specification information for the CNF-SAT problem.
alpar@9 153 The \verb|VARIABLES| field contains an integer value specifying $n$,
alpar@9 154 the number of variables in the instance. The \verb|CLAUSES| field
alpar@9 155 contains an integer value specifying $m$, the number of clauses in the
alpar@9 156 instance.
alpar@9 157
alpar@9 158 \paragraph{Clauses.} The clauses appear immediately after the problem
alpar@9 159 line. The variables are assumed to be numbered from 1 up to $n$. It is
alpar@9 160 not necessary that every variable appears in the instance. Each clause
alpar@9 161 is represented by a sequence of numbers separated by either a space,
alpar@9 162 tab, or new-line character. The non-negated version of a variable $j$
alpar@9 163 is represented by $j$; the negated version is represented by $-j$. Each
alpar@9 164 clause is terminated by the value 0. Unlike many formats that represent
alpar@9 165 the end of a clause by a new-line character, this format allows clauses
alpar@9 166 to be on multiple lines.
alpar@9 167
alpar@9 168 \paragraph{Example.} Below here is an example of the data file in
alpar@9 169 DIMACS format corresponding to the CNF-SAT problem (1.2).
alpar@9 170
alpar@9 171 \begin{footnotesize}
alpar@9 172 \begin{verbatim}
alpar@9 173 c sample.cnf
alpar@9 174 c
alpar@9 175 c This is an example of the CNF-SAT problem data
alpar@9 176 c in DIMACS format.
alpar@9 177 c
alpar@9 178 p cnf 4 3
alpar@9 179 1 2 0
alpar@9 180 -4 3
alpar@9 181 -2 0
alpar@9 182 -1 4 0
alpar@9 183 c
alpar@9 184 c eof
alpar@9 185 \end{verbatim}
alpar@9 186 \end{footnotesize}
alpar@9 187
alpar@9 188 \newpage
alpar@9 189
alpar@9 190 \subsection{glp\_check\_cnfsat---check for CNF-SAT problem instance}
alpar@9 191
alpar@9 192 \subsubsection*{Synopsis}
alpar@9 193
alpar@9 194 \begin{verbatim}
alpar@9 195 int glp_check_cnfsat(glp_prob *P);
alpar@9 196 \end{verbatim}
alpar@9 197
alpar@9 198 \subsubsection*{Description}
alpar@9 199
alpar@9 200 The routine \verb|glp_check_cnfsat| checks if the specified problem
alpar@9 201 object \verb|P| contains a 0-1 programming problem instance in the
alpar@9 202 format (1.5)--(1.6) and therefore encodes a CNF-SAT problem instance.
alpar@9 203
alpar@9 204 \subsubsection*{Returns}
alpar@9 205
alpar@9 206 If the specified problem object has the format (1.5)--(1.6), the
alpar@9 207 routine returns zero, otherwise non-zero.
alpar@9 208
alpar@9 209 \subsection{glp\_write\_cnfsat---write CNF-SAT problem data in\\DIMACS
alpar@9 210 format}
alpar@9 211
alpar@9 212 \subsubsection*{Synopsis}
alpar@9 213
alpar@9 214 \begin{verbatim}
alpar@9 215 int glp_write_cnfsat(glp_prob *P, const char *fname);
alpar@9 216 \end{verbatim}
alpar@9 217
alpar@9 218 \subsubsection*{Description}
alpar@9 219
alpar@9 220 The routine \verb|glp_write_cnfsat| automatically translates the
alpar@9 221 specified 0-1 programming problem instance (1.5)--(1.6) to a CNF-SAT
alpar@9 222 problem instance and writes the problem data to a text file in DIMACS
alpar@9 223 format.
alpar@9 224
alpar@9 225 The parameter \verb|P| is the problem object, which should specify
alpar@9 226 a 0-1 programming problem instance in the format (1.5)--(1.6).
alpar@9 227
alpar@9 228 The character string \verb|fname| specifies a name of the output text
alpar@9 229 file to be written. (If the file name ends with suffix `\verb|.gz|',
alpar@9 230 the file is assumed to be compressed, in which case the routine
alpar@9 231 performs automatic compression on writing that file.)
alpar@9 232
alpar@9 233 \subsubsection*{Returns}
alpar@9 234
alpar@9 235 If the operation was successful, the routine returns zero. Otherwise,
alpar@9 236 it prints an error message and returns non-zero.
alpar@9 237
alpar@9 238 \newpage
alpar@9 239
alpar@9 240 \subsection{glp\_minisat1---solve CNF-SAT problem instance with\\
alpar@9 241 MiniSat solver}
alpar@9 242
alpar@9 243 \subsubsection*{Synopsis}
alpar@9 244
alpar@9 245 \begin{verbatim}
alpar@9 246 int glp_minisat1(glp_prob *P);
alpar@9 247 \end{verbatim}
alpar@9 248
alpar@9 249 \subsubsection*{Description}
alpar@9 250
alpar@9 251 The routine \verb|glp_minisat1| is a driver to MiniSat, a CNF-SAT
alpar@9 252 solver developed by Niklas E\'en and Niklas S\"orensson, Chalmers
alpar@9 253 University of Technology, Sweden.\footnote{The MiniSat software module
alpar@9 254 is {\it not} part of GLPK, but is used with GLPK and included in the
alpar@9 255 distribution.}
alpar@9 256
alpar@9 257 It is assumed that the specified problem object \verb|P| contains
alpar@9 258 a 0-1 programming problem instance in the format (1.5)--(1.6) and
alpar@9 259 therefore encodes a CNF-SAT problem instance.
alpar@9 260
alpar@9 261 If the problem instance has been successfully solved to the end, the
alpar@9 262 routine \verb|glp_minisat1| returns 0. In this case the routine
alpar@9 263 \verb|glp_mip_status| can be used to determine the solution status:
alpar@9 264
alpar@9 265 \verb|GLP_OPT| means that the solver found an integer feasible
alpar@9 266 solution and therefore the corresponding CNF-SAT instance is
alpar@9 267 satisfiable;
alpar@9 268
alpar@9 269 \verb|GLP_NOFEAS| means that no integer feasible solution exists and
alpar@9 270 therefore the corresponding CNF-SAT instance is unsatisfiable.
alpar@9 271
alpar@9 272 If an integer feasible solution was found, corresponding values of
alpar@9 273 binary variables can be retrieved with the routine
alpar@9 274 \verb|glp_mip_col_val|.
alpar@9 275
alpar@9 276 \subsubsection*{Returns}
alpar@9 277
alpar@9 278 \begin{tabular}{@{}p{25mm}p{97.3mm}@{}}
alpar@9 279 0 & The MIP problem instance has been successfully solved. (This code
alpar@9 280 does {\it not} necessarily mean that the solver has found feasible
alpar@9 281 solution. It only means that the solution process was successful.)\\
alpar@9 282 \verb|GLP_EDATA| & The specified problem object contains a MIP instance
alpar@9 283 which does {\it not} have the format (1.5)--(1.6).\\
alpar@9 284 \verb|GLP_EFAIL| & The solution process was unsuccessful because of the
alpar@9 285 solver failure.\\
alpar@9 286 \end{tabular}
alpar@9 287
alpar@9 288 \newpage
alpar@9 289
alpar@9 290 \subsection{glp\_intfeas1---solve integer feasibility problem}
alpar@9 291
alpar@9 292 \subsubsection*{Synopsis}
alpar@9 293
alpar@9 294 \begin{verbatim}
alpar@9 295 int glp_intfeas1(glp_prob *P, int use_bound, int obj_bound);
alpar@9 296 \end{verbatim}
alpar@9 297
alpar@9 298 \subsubsection*{Description}
alpar@9 299
alpar@9 300 The routine \verb|glp_intfeas1| is a tentative implementation of
alpar@9 301 an integer feasibility solver based on a CNF-SAT solver (currently
alpar@9 302 it is MiniSat; see Subsection 2.4).
alpar@9 303
alpar@9 304 If the parameter \verb|use_bound| is zero, the routine searches for
alpar@9 305 {\it any} integer feasibile solution to the specified integer
alpar@9 306 programming problem. Note that in this case the objective function is
alpar@9 307 ignored.
alpar@9 308
alpar@9 309 If the parameter \verb|use_bound| is non-zero, the routine searches for
alpar@9 310 an integer feasible solution, which provides a value of the objective
alpar@9 311 function not worse than \verb|obj_bound|. In other word, the parameter
alpar@9 312 \verb|obj_bound| specifies an upper (in case of minimization) or lower
alpar@9 313 (in case of maximization) bound to the objective function.
alpar@9 314
alpar@9 315 If the specified problem has been successfully solved to the end, the
alpar@9 316 routine \verb|glp_intfeas1| returns 0. In this case the routine
alpar@9 317 \verb|glp_mip_status| can be used to determine the solution status:
alpar@9 318
alpar@9 319 \begin{itemize}
alpar@9 320 \item {\tt GLP\_FEAS} means that the solver found an integer feasible
alpar@9 321 solution;
alpar@9 322
alpar@9 323 \item {\tt GLP\_NOFEAS} means that the problem has no integer feasible
alpar@9 324 solution (if {\tt use\_bound} is zero) or it has no integer feasible
alpar@9 325 solution, which is not worse than {\tt obj\_bound} (if {\tt use\_bound}
alpar@9 326 is non-zero).
alpar@9 327 \end{itemize}
alpar@9 328
alpar@9 329 If an integer feasible solution was found, corresponding values of
alpar@9 330 variables (columns) can be retrieved with the routine
alpar@9 331 \verb|glp_mip_col_val|.
alpar@9 332
alpar@9 333 \subsubsection*{Usage Notes}
alpar@9 334
alpar@9 335 The integer programming problem specified by the parameter \verb|P|
alpar@9 336 should satisfy to the following requirements:
alpar@9 337
alpar@9 338 \begin{enumerate}
alpar@9 339 \item All variables (columns) should be either binary ({\tt GLP\_BV})
alpar@9 340 or fixed at integer values ({\tt GLP\_FX}).
alpar@9 341
alpar@9 342 \item All constraint and objective coefficients should be integer
alpar@9 343 numbers in the range $[-2^{31},\ +2^{31}-1]$.
alpar@9 344 \end{enumerate}
alpar@9 345
alpar@9 346 Though there are no special requirements to the constraints,
alpar@9 347 currently the routine \verb|glp_intfeas1| is efficient mainly for
alpar@9 348 problems, where most constraints (rows) fall into the following three
alpar@9 349 classes:
alpar@9 350
alpar@9 351 \begin{enumerate}
alpar@9 352 \item Covering inequalities
alpar@9 353 $$\sum_{j}t_j\geq 1,$$
alpar@9 354 where $t_j=x_j$ or $t_j=1-x_j$, $x_j$ is a binary variable.
alpar@9 355
alpar@9 356 \item Packing inequalities
alpar@9 357 $$\sum_{j}t_j\leq 1.$$
alpar@9 358
alpar@9 359 \item Partitioning equalities (SOS1 constraints)
alpar@9 360 $$\sum_{j}t_j=1.$$
alpar@9 361 \end{enumerate}
alpar@9 362
alpar@9 363 \subsubsection*{Returns}
alpar@9 364
alpar@9 365 \begin{tabular}{@{}p{25mm}p{97.3mm}@{}}
alpar@9 366 0 & The problem has been successfully solved. (This code does {\it not}
alpar@9 367 necessarily mean that the solver has found an integer feasible solution.
alpar@9 368 It only means that the solution process was successful.)\\
alpar@9 369
alpar@9 370 \verb|GLP_EDATA| & The specified problem object does not satisfy to the
alpar@9 371 requirements listed in Paragraph `Usage Notes'.\\
alpar@9 372
alpar@9 373 \verb|GLP_ERANGE| & An integer overflow occured on translating the
alpar@9 374 specified problem to a CNF-SAT problem.\\
alpar@9 375
alpar@9 376 \verb|GLP_EFAIL| & The solution process was unsuccessful because of the
alpar@9 377 solver failure.\\
alpar@9 378 \end{tabular}
alpar@9 379
alpar@9 380 \end{document}