lemon-project-template-glpk
comparison 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 |
comparison
equal
deleted
inserted
replaced
-1:000000000000 | 0:d304e457c133 |
---|---|
1 %* cnfsat.tex *% | |
2 | |
3 \documentclass[11pt,draft]{article} | |
4 | |
5 \begin{document} | |
6 | |
7 \title{CNF Satisfiability Problem} | |
8 | |
9 \author{Andrew Makhorin {\tt<mao@gnu.org>}} | |
10 | |
11 \date{August 2011} | |
12 | |
13 \maketitle | |
14 | |
15 \section{Introduction} | |
16 | |
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}. | |
22 | |
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. | |
40 | |
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. | |
57 | |
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\}$$ | |
74 | |
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$. | |
86 | |
87 \newpage | |
88 | |
89 \section{GLPK API Routines} | |
90 | |
91 \subsection{glp\_read\_cnfsat---read CNF-SAT problem data in\\DIMACS | |
92 format} | |
93 | |
94 \subsubsection*{Synopsis} | |
95 | |
96 \begin{verbatim} | |
97 int glp_read_cnfsat(glp_prob *P, const char *fname); | |
98 \end{verbatim} | |
99 | |
100 \subsubsection*{Description} | |
101 | |
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). | |
105 | |
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|. | |
110 | |
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''.) | |
115 | |
116 \subsubsection*{Returns} | |
117 | |
118 If the operation was successful, the routine returns zero. Otherwise, | |
119 it prints an error message and returns non-zero. | |
120 | |
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/}.}} | |
124 | |
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. | |
129 | |
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|. | |
134 | |
135 \begin{verbatim} | |
136 c This is a comment line | |
137 \end{verbatim} | |
138 | |
139 \newpage | |
140 | |
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: | |
144 | |
145 \begin{verbatim} | |
146 p cnf VARIABLES CLAUSES | |
147 \end{verbatim} | |
148 | |
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. | |
157 | |
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. | |
167 | |
168 \paragraph{Example.} Below here is an example of the data file in | |
169 DIMACS format corresponding to the CNF-SAT problem (1.2). | |
170 | |
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} | |
187 | |
188 \newpage | |
189 | |
190 \subsection{glp\_check\_cnfsat---check for CNF-SAT problem instance} | |
191 | |
192 \subsubsection*{Synopsis} | |
193 | |
194 \begin{verbatim} | |
195 int glp_check_cnfsat(glp_prob *P); | |
196 \end{verbatim} | |
197 | |
198 \subsubsection*{Description} | |
199 | |
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. | |
203 | |
204 \subsubsection*{Returns} | |
205 | |
206 If the specified problem object has the format (1.5)--(1.6), the | |
207 routine returns zero, otherwise non-zero. | |
208 | |
209 \subsection{glp\_write\_cnfsat---write CNF-SAT problem data in\\DIMACS | |
210 format} | |
211 | |
212 \subsubsection*{Synopsis} | |
213 | |
214 \begin{verbatim} | |
215 int glp_write_cnfsat(glp_prob *P, const char *fname); | |
216 \end{verbatim} | |
217 | |
218 \subsubsection*{Description} | |
219 | |
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. | |
224 | |
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). | |
227 | |
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.) | |
232 | |
233 \subsubsection*{Returns} | |
234 | |
235 If the operation was successful, the routine returns zero. Otherwise, | |
236 it prints an error message and returns non-zero. | |
237 | |
238 \newpage | |
239 | |
240 \subsection{glp\_minisat1---solve CNF-SAT problem instance with\\ | |
241 MiniSat solver} | |
242 | |
243 \subsubsection*{Synopsis} | |
244 | |
245 \begin{verbatim} | |
246 int glp_minisat1(glp_prob *P); | |
247 \end{verbatim} | |
248 | |
249 \subsubsection*{Description} | |
250 | |
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.} | |
256 | |
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. | |
260 | |
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: | |
264 | |
265 \verb|GLP_OPT| means that the solver found an integer feasible | |
266 solution and therefore the corresponding CNF-SAT instance is | |
267 satisfiable; | |
268 | |
269 \verb|GLP_NOFEAS| means that no integer feasible solution exists and | |
270 therefore the corresponding CNF-SAT instance is unsatisfiable. | |
271 | |
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|. | |
275 | |
276 \subsubsection*{Returns} | |
277 | |
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} | |
287 | |
288 \newpage | |
289 | |
290 \subsection{glp\_intfeas1---solve integer feasibility problem} | |
291 | |
292 \subsubsection*{Synopsis} | |
293 | |
294 \begin{verbatim} | |
295 int glp_intfeas1(glp_prob *P, int use_bound, int obj_bound); | |
296 \end{verbatim} | |
297 | |
298 \subsubsection*{Description} | |
299 | |
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). | |
303 | |
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. | |
308 | |
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. | |
314 | |
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: | |
318 | |
319 \begin{itemize} | |
320 \item {\tt GLP\_FEAS} means that the solver found an integer feasible | |
321 solution; | |
322 | |
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} | |
328 | |
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|. | |
332 | |
333 \subsubsection*{Usage Notes} | |
334 | |
335 The integer programming problem specified by the parameter \verb|P| | |
336 should satisfy to the following requirements: | |
337 | |
338 \begin{enumerate} | |
339 \item All variables (columns) should be either binary ({\tt GLP\_BV}) | |
340 or fixed at integer values ({\tt GLP\_FX}). | |
341 | |
342 \item All constraint and objective coefficients should be integer | |
343 numbers in the range $[-2^{31},\ +2^{31}-1]$. | |
344 \end{enumerate} | |
345 | |
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: | |
350 | |
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. | |
355 | |
356 \item Packing inequalities | |
357 $$\sum_{j}t_j\leq 1.$$ | |
358 | |
359 \item Partitioning equalities (SOS1 constraints) | |
360 $$\sum_{j}t_j=1.$$ | |
361 \end{enumerate} | |
362 | |
363 \subsubsection*{Returns} | |
364 | |
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.)\\ | |
369 | |
370 \verb|GLP_EDATA| & The specified problem object does not satisfy to the | |
371 requirements listed in Paragraph `Usage Notes'.\\ | |
372 | |
373 \verb|GLP_ERANGE| & An integer overflow occured on translating the | |
374 specified problem to a CNF-SAT problem.\\ | |
375 | |
376 \verb|GLP_EFAIL| & The solution process was unsuccessful because of the | |
377 solver failure.\\ | |
378 \end{tabular} | |
379 | |
380 \end{document} |