You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

413 lines
14 KiB

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