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