lemon-project-template-glpk
view deps/glpk/examples/pbn/pbn.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 %* pbn.tex *%
3 \documentclass[11pt,draft]{article}
4 \usepackage{amssymb}
6 \begin{document}
8 \title{Solving Paint-By-Numbers Puzzles with GLPK}
10 \author{Andrew Makhorin {\tt<mao@gnu.org>}}
12 \date{August 2011}
14 \maketitle
16 \section{Introduction$^1$}
18 \footnotetext[1]{This section is based on the material from [1].}
20 A {\it paint-by-numbers} puzzle consists of an $m\times n$ grid of
21 pixels (the {\it canvas}) together with $m+n$ {\it cluster-size
22 sequences}, one for each row and column. The goal is to paint the canvas
23 with a picture that satisfies the following constraints:
25 1. Each pixel must be blank or white.
27 2. If a row or column has cluster-size sequence $s_1$, $s_2$, \dots,
28 $s_k$, then it must contain $k$ clusters of black pixels---the first
29 with $s_1$ black pixels, the second with $s_2$ black pixels, and so on.
31 It should be noted that ``first'' means ``leftmost'' for rows and
32 ``topmost'' for columns, and that rows and columns need not begin or end
33 with black pixels.
35 \subsubsection*{Example}
37 \def\arraystretch{.8}
39 \begin{center}
40 \begin{tabular}{*{3}{@{$\;\;$}c}c*{10}{@{\ }c}@{}}
41 & & && & &1& &1& & & & & \\
42 & & && & &1& &1& & & & & \\
43 & & &&2&1&1&1&1&1&2&3& & \\
44 & & &&3&2&1&2&1&2&3&4&8&9\\
45 \\
46 &3&6&&$\blacksquare$&$\blacksquare$&$\blacksquare$&$\square$&
47 $\blacksquare$&$\blacksquare$&$\blacksquare$&$\blacksquare$&
48 $\blacksquare$&$\blacksquare$\\
49 &1&4&&$\blacksquare$&$\square$&$\square$&$\square$&$\square$&
50 $\square$&$\blacksquare$&$\blacksquare$&$\blacksquare$&$\blacksquare$\\
51 1&1&3&&$\square$&$\square$&$\blacksquare$&$\square$&$\blacksquare$&
52 $\square$&$\square$&$\blacksquare$&$\blacksquare$&$\blacksquare$\\
53 & &2&&$\square$&$\square$&$\square$&$\square$&$\square$&$\square$&
54 $\square$&$\square$&$\blacksquare$&$\blacksquare$\\
55 &3&3&&$\square$&$\square$&$\blacksquare$&$\blacksquare$&$\blacksquare$&
56 $\square$&$\square$&$\blacksquare$&$\blacksquare$&$\blacksquare$\\
57 &1&4&&$\blacksquare$&$\square$&$\square$&$\square$&$\square$&$\square$&
58 $\blacksquare$&$\blacksquare$&$\blacksquare$&$\blacksquare$\\
59 &2&5&&$\blacksquare$&$\blacksquare$&$\square$&$\square$&$\square$&
60 $\blacksquare$&$\blacksquare$&$\blacksquare$&$\blacksquare$&
61 $\blacksquare$\\
62 &2&5&&$\blacksquare$&$\blacksquare$&$\square$&$\square$&$\square$&
63 $\blacksquare$&$\blacksquare$&$\blacksquare$&$\blacksquare$&
64 $\blacksquare$\\
65 &1&1&&$\square$&$\square$&$\square$&$\blacksquare$&$\square$&$\square$&
66 $\square$&$\square$&$\square$&$\blacksquare$\\
67 & &3&&$\square$&$\square$&$\blacksquare$&$\blacksquare$&$\blacksquare$&
68 $\square$&$\square$&$\square$&$\square$&$\square$\\
69 \end{tabular}
70 \end{center}
72 \def\arraystretch{1}
74 \section{Solving a puzzle}
76 The Paint-By-Numbers puzzle can be formulated as a 0-1 integer
77 feasibility problem. The formulation used in GLPK was proposed in [1].
79 For solving puzzles there are used two components, which both are
80 coded in the GNU MathProg modeling language [2]: the model section and
81 the data section. The model section is common for all puzzles and
82 placed in file \verb|pbn.mod|. This file is included in the GLPK
83 distribution and can be found in subdirectory \verb|examples/pbn|.
85 To solve a particular puzzle the user only needs to prepare the data
86 section, which defines input data to the puzzle. The data section for
87 the example puzzle from the previous section may look like follows
88 (here \verb|m| is the number of rows, and \verb|n| is the number of
89 columns):
91 \begin{footnotesize}
92 \begin{verbatim}
93 data;
95 param m := 10;
97 param n := 10;
99 param row : 1 2 3 :=
100 1 3 6 .
101 2 1 4 .
102 3 1 1 3
103 4 2 . .
104 5 3 3 .
105 6 1 4 .
106 7 2 5 .
107 8 2 5 .
108 9 1 1 .
109 10 3 . .
110 ;
112 param col : 1 2 3 4 :=
113 1 2 3 . .
114 2 1 2 . .
115 3 1 1 1 1
116 4 1 2 . .
117 5 1 1 1 1
118 6 1 2 . .
119 7 2 3 . .
120 8 3 4 . .
121 9 8 . . .
122 10 9 . . .
123 ;
125 end;
126 \end{verbatim}
127 \end{footnotesize}
129 \newpage
131 Let the data section for a puzzle be placed in file \verb|foo.dat|.
132 Then to solve the puzzle the user should enter the following command:
134 \begin{verbatim}
135 glpsol --minisat -m pbn.mod -d foo.dat
136 \end{verbatim}
138 \noindent
139 This command invokes \verb|glpsol|, the GLPK LP/MIP stand-alone solver,
140 which reads the model section from file \verb|pbn.mod|, the data section
141 from file \verb|foo.dat|, translates them to an internal representation,
142 and solves the resulting 0-1 integer feasibility problem. The option
143 \verb|--minisat| tells \verb|glpsol| to translate the feasibility
144 problem to a CNF satisfiability problem and then use the MiniSat solver
145 [3] to solve it.
147 If a solution to the puzzle has been found, that is indicated by the
148 message \verb|SATISFIABLE|, \verb|glpsol| prints the solution to the
149 standard output (terminal), writes it to file \verb|solution.ps| in the
150 PostScript format, and also writes it to file \verb|solution.dat| in the
151 form of MathProg data section, which can be used later to check for
152 multiple solutions, if necessary (for details see the next section).
153 The message \verb|UNSATISFIABLE| means that the puzzle has no solution.
155 Usually the time taken to solve a puzzle of moderate size (up to 50 rows
156 and columns) varies from several seconds to several minutes. However,
157 hard or large puzzles may require much more time.
159 Data sections for some example puzzles included in the GLPK distribution
160 can be found in subdirectory \verb|examples/pbn|.
162 \section{Checking for multiple solutions}
164 Sometimes the user may be interested to know if the puzzle has exactly
165 one (unique) solution or it has multiple solutions. To check that the
166 user should solve the puzzle as explained above in the previous section
167 and then enter the following command:
169 \begin{verbatim}
170 glpsol --minisat -m pbn.mod -d foo.dat -d solution.dat
171 \end{verbatim}
173 \noindent
174 In this case \verb|glpsol| reads an additional data section from file
175 \verb|solution.dat|, which contains the previously found solution,
176 activates an additional constraint in the model section to forbid
177 finding the solution specified in the additional data section, and
178 attempts to find another solution. The message \verb|UNSATISFIABLE|
179 reported by \verb|glpsol| will mean that the puzzle has a unique
180 solution, while the message \verb|SATISFIABLE| will mean that the puzzle
181 has at least two different solutions.
183 \newpage
185 \section{Solution times}
187 The table on the next page shows solution times on a sample set of
188 the paint-by-numbers puzzles from the \verb|<webpbn.com>| website.
189 This sample set was used in the survey [4] to compare efficiency of
190 existing PBN solvers.
192 The authors of some puzzles from the sample set have given permission
193 for their puzzles to be freely redistributed as long as the original
194 attribution and copyright statement are retained. In the table these
195 puzzles are marked by an asterisk (*). The files containing the
196 MathProg data sections for these puzzles are included in the GLPK
197 distribution and can be found in subdirectory \verb|examples/pbn|.
199 All runs were performed on Intel Pentium 4 (CPU 3GHz, 2GB of RAM).
200 The C compiler used was GCC 3.4.4 with default optimization options.
202 The column `Sol.Time' shows the time, in seconds, taken by the
203 \verb|glpsol| solver to find a solution to corresponding puzzle. The
204 column `Chk.Time' shows the time, in seconds, taken by \verb|glpsol| to
205 check for multiple solutions, i.e. either to prove that the puzzle has
206 a unique solution or find another solution to the puzzle. Both these
207 times do not include the time used to translate the MathProg model and
208 data sections into an internal MIP representation, but include the time
209 used to translate the 0-1 feasibility problem to a CNF satisfiability
210 problem.
212 \begin{thebibliography}{10}
214 \bibitem{1}
215 Robert A. Bosch, ``Painting by Numbers'', 2000.\\
216 \verb|<http://www.oberlin.edu/~math/faculty/bosch/pbn-page.html>|.
218 \bibitem{2}
219 GLPK: Modeling Language GNU MathProg. Language Reference. (This
220 document is included in the GLPK distribution and can be found in
221 subdirectory \verb|doc|.)
223 \bibitem{3}
224 Niklas E\'en, Niklas S\"orensson, ``An Extensible SAT-solver'',
225 Chalmers University of Technology, Sweden. \verb|<http://minisat.se/>|.
227 \bibitem{4}
228 Jan Wolter, ``Survey of Paint-by-Number Puzzle Solvers''.\\
229 \verb|<http://webpbn.com/survey/>|.
231 \end{thebibliography}
233 \newpage
235 \begin{table}
236 \caption{Solution times on the sample set of puzzles from [4]}
237 \begin{center}
238 \begin{tabular}{@{}lllcrr@{}}
239 \hline
240 \multicolumn{2}{c}{Puzzle}&Size&Notes&Sol.Time, s&Chk.Time, s\\
241 \hline
242 \#1&Dancer* &$10\times 5$&L&$<1$&$<1$\\
243 \#6&Cat* &$20\times 20$&L&$<1$&$<1$\\
244 \#21&Skid* &$25\times 14$&L, B&$<1$&$<1$\\
245 \#27&Bucks* &$23\times 27$&B&$<1$&$<1$\\
246 \#23&Edge* &$11\times 10$&&$<1$&$<1$\\
247 \#2413&Smoke &$20\times 20$&&$<1$&$<1$\\
248 \#16&Knot* &$34\times 34$&L&1&1\\
249 \#529&Swing* &$45\times 45$&L&1&1\\
250 \#65&Mum* &$40\times 34$&&1&1\\
251 \#7604&DiCap &$55\times 55$&&10&10\\
252 \#1694&Tragic &$50\times 45$&&3&3\\
253 \#1611&Merka &$60\times 55$&B&4&4\\
254 \#436&Petro* &$35\times 40$&&1&1\\
255 \#4645&M\&M &$70\times 50$&B&5&6\\
256 \#3541&Signed &$50\times 60$&&7&7\\
257 \#803&Light* &$45\times 50$&B&1&1\\
258 \#6574&Forever*&$25\times 25$&&1&1\\
259 \#2040&Hot &$60\times 55$&&6&6\\
260 \#6739&Karate &$40\times 40$&M&2&2\\
261 \#8098&9-Dom* &$19\times 19$&&1&2\\
262 \#2556&Flag &$45\times 65$&M, B&2&2\\
263 \#2712&Lion &$47\times 47$&M&11&12\\
264 \#10088&Marley &$63\times 52$&M&135&226\\
265 \#9892&Nature &$40\times 50$&M&850&1053\\
266 \hline
267 \end{tabular}
269 \begin{tabular}{@{}lp{102mm}@{}}
270 *&Puzzle designer has given permission to redistribute the puzzle.\\
271 L&Puzzle is line solvable. That is, it can be solved one line at a
272 time.\\
273 B&Puzzle contains blank rows or columns.\\
274 M&Puzzle has multiple solutions.\\
275 \end{tabular}
276 \end{center}
277 \end{table}
279 \end{document}