1: \documentclass{LMCS}
2:
3: \usepackage{pstricks,pst-plot,pst-node}
4: \usepackage{enumerate,graphicx,hyperref}
5:
6:
7: \theoremstyle{plain}\newtheorem{hypothesis}{Hypothesis}
8: \theoremstyle{plain}\newtheorem{proposition}{Proposition}
9: \theoremstyle{plain}\newtheorem{lemma}{Lemma}
10:
11:
12: %\lmcsheading{?}{200?}{?-?}{200?-?}{200?-?}
13:
14:
15:
16: \newcommand{\widthfig}[4]{%% width, figure, caption, vspace
17: \begin{figure}[htb]
18: \begin{center}
19: \includegraphics[width=#1cm]{#2}
20: \end{center}
21: \vspace*{-0.3cm}
22: \caption{\label{#2}#3}
23: \vspace*{#4}
24: \end{figure}}
25:
26: \newcommand{\widthonlyfig}[2]{%% width, figure
27: \includegraphics[width=#1cm]{#2}
28: }
29:
30: \newcommand{\cost}{cost}
31: \newcommand{\ASratio}{AsymRatio}
32: \def\setstretch#1{\renewcommand{\baselinestretch}{#1}}
33:
34:
35: \newcommand{\chaff}{Chaff}
36: \newcommand{\minisat}{MiniSat}
37: \newcommand{\zchaff}{ZChaff}
38: \newcommand{\satz}{Satz}
39:
40:
41: \newcommand{\pp}{\mbox{\small ++}}
42:
43:
44: \newcommand{\domain}{{\mathcal D}}
45: \newcommand{\size}{{\mathcal S}}
46: \newcommand{\ppp}{{\mathcal P}}
47:
48:
49:
50:
51:
52:
53: %\newcommand{\ifTR}[1]{#1}
54: \newcommand{\ifTR}[1]{}
55: %\newcommand{\ifLMCS}[1]{}
56: \newcommand{\ifLMCS}[1]{#1}
57:
58: \def\doi{3 (1:6) 2007}
59: \lmcsheading%
60: {\doi}
61: {1--41}
62: {}
63: {}
64: {Mar.~13, 2006}
65: {Feb.~26, 2007}
66: {}
67:
68: \begin{document}
69:
70: \title[Goal Asymmetry and DPLL Proofs in Planning]{Structure and
71: Problem Hardness:\\ Goal Asymmetry and DPLL Proofs in SAT-Based
72: Planning}
73:
74: \author[J.~Hoffmann]{J\"org Hoffmann\rsuper a}
75: \address{{\lsuper a}Digital Enterprise Research Institute, Innsbruck, Austria}
76: \email{joerg.hoffmann@deri.org}
77:
78: \author[C.~Gomes]{Carla Gomes\rsuper b}
79: \address{{\lsuper{b,c}}Cornell University, Ithaca, NY, USA}
80: \email{\{gomes,selman\}@cs.cornell.edu}
81: \thanks{{\lsuper b}Research supported by the
82: Intelligent Information Systems Institute, Cornell University (AFOSR
83: grant F49620-01-1-0076).}
84:
85: \author[B.~Selman]{Bart Selman\rsuper c}
86: %\address{Cornell University, Ithaca, NY, USA}
87: %\email{selman@cs.cornell.edu}
88:
89: \keywords{planning, domain-independent planning, planning as SAT, DPLL, backdoors}
90: \subjclass{I.2.8, I.2.3}
91:
92: \begin{abstract}
93: In Verification and in (optimal) AI Planning, a successful method is
94: to formulate the application as boolean satisfiability (SAT), and
95: solve it with state-of-the-art DPLL-based procedures. There is a
96: lack of understanding of why this works so well. Focussing on the
97: Planning context, we identify a form of {\em problem structure}
98: concerned with the symmetrical or asymmetrical nature of the cost of
99: achieving the individual planning goals. We quantify this sort of
100: structure with a simple numeric parameter called $\ASratio$, ranging
101: between $0$ and $1$. We run experiments in 10 benchmark domains from
102: the International Planning Competitions since 2000; we show that
103: $\ASratio$ is a good indicator of SAT solver performance in 8 of
104: these domains. We then examine carefully crafted {\em synthetic
105: planning domains} that allow control of the amount of structure, and
106: that are clean enough for a rigorous analysis of the combinatorial
107: search space. The domains are parameterized by size, and by the
108: amount of structure. The CNFs we examine are unsatisfiable, encoding
109: one planning step less than the length of the optimal plan. We prove
110: upper and lower bounds on the size of the best possible DPLL
111: refutations, under different settings of the amount of structure, as
112: a function of size. We also identify the best possible sets of
113: branching variables (backdoors). With {\em minimum} $\ASratio$, we
114: prove exponential lower bounds, and identify minimal backdoors of
115: size linear in the number of variables. With {\em maximum}
116: $\ASratio$, we identify {\em logarithmic} DPLL refutations (and
117: backdoors), showing a doubly exponential gap between the two
118: structural extreme cases. The reasons for this behavior -- the proof
119: arguments -- illuminate the prototypical patterns of structure
120: causing the empirical behavior observed in the competition
121: benchmarks.
122: \end{abstract}
123:
124: \maketitle
125: \vfill\eject
126:
127: \input{introduction}
128: \input{related}
129: \input{prelim}
130: \input{real}
131: \input{sd}
132: \input{empirical}
133: \input{strawman}
134: \input{conclusion}
135:
136:
137:
138: %\bigskip
139:
140: \noindent {\bf Acknowledgements.} We thank Ashish Sabharwal for advice
141: on proving resolution lower bounds. We thank Rina Dechter for
142: discussions on the relation between backdoors and cutsets. We thank
143: Toby Walsh for discussions on the intuition behind $\ASratio$, and for
144: the suggestion to construct a red herring. We thank Jussi Rintanen for
145: providing the code of his random instance generator, and we thank
146: Martin G\"utlein for implementing the enumeration of CNF variable sets
147: under exploitation of problem symmetries. We finally thank the
148: anonymous reviewers for their comments, which contributed a lot to
149: improve the paper.
150:
151:
152:
153: %\bibliographystyle{plain}
154: %\bibliography{biblio}
155: \begin{thebibliography}{10}
156:
157: \bibitem{bundy:etal:ai-96}
158: R.~Sebastiani A.~Bundy, F.~Giunchiglia and T.~Walsh.
159: \newblock Calculating criticalities.
160: \newblock {\em Artificial Intelligence}, 88(1--2):39--67, 1996.
161:
162: \bibitem{baioletti:etal:aips-00}
163: M.~Baioletti, S.~Marcugini, and A.~Milani.
164: \newblock {D}{P}{P}lan: An algorithm for fast solution extraction from a
165: planning graph.
166: \newblock In {\em Proc. AIPS'00}, 2000.
167:
168: \bibitem{barrett:weld:ai-94}
169: A.~Barrett and D.~Weld.
170: \newblock Partial order planning: Evaluating possible efficiency gains.
171: \newblock {\em Artificial Intelligence}, 67:71--112, 1994.
172:
173: \bibitem{beame:etal:jair-04}
174: P.~Beame, H.~Kautz, and A.~Sabharwal.
175: \newblock Towards understanding and harnessing the potential of clause
176: learning.
177: \newblock {\em Journal of Artificial Intelligence Research}, 22:319--351, 2004.
178:
179: \bibitem{blum:furst:ai-97}
180: A.~Blum and M.~Furst.
181: \newblock Fast planning through planning graph analysis.
182: \newblock {\em Artificial Intelligence}, 90(1-2):279--298, 1997.
183:
184: \bibitem{bonet:geffner:ai-01}
185: B.~Bonet and H.~Geffner.
186: \newblock Planning as heuristic search.
187: \newblock {\em Artificial Intelligence}, 129(1--2):5--33, 2001.
188:
189: \bibitem{bonet:etal:siam-00}
190: M.~Bonet, J.~Esteban, N.~Galesi, and J.~Johansen.
191: \newblock On the relative complexity of resolution refinements and cutting
192: planes proof systems.
193: \newblock {\em SIAM Journal of Computing}, 30(5):1462--1484, 2001.
194:
195: \bibitem{buss:pitassi:csl-97}
196: S.~Buss and T.~Pitassi.
197: \newblock Resolution and the weak pigeon-hole principle.
198: \newblock In {\em Proc. CSL'97}, pages 149--156, 1997.
199:
200: \bibitem{bylander:ai-94}
201: Tom Bylander.
202: \newblock The computational complexity of propositional {STRIPS} planning.
203: \newblock {\em Artificial Intelligence}, 69(1--2):165--204, 1994.
204:
205: \bibitem{cheeseman:etal:ijcai-91}
206: P.~Cheeseman, B.~Kanefsky, and W.~Taylor.
207: \newblock Where the {\em really} hard problems are.
208: \newblock In {\em Proc. IJCAI'91}, pages 331--337, 1991.
209:
210: \bibitem{chen:dalmau:cp-05}
211: H.~Chen and V.~Dalmau.
212: \newblock Beyond hypertree width: Decomposition methods without decompositions.
213: \newblock In {\em Proc. CP'05}, 2005.
214:
215: \bibitem{Z02}
216: S.~Climer and W.~Zhang.
217: \newblock {Searching for backbones and fat: A limit-crossing approach with
218: applications}.
219: \newblock In {\em Proc. AAAI-02}, 2002.
220:
221: \bibitem{cook:reckhow:jsl-79}
222: S.~Cook and R.~Reckhow.
223: \newblock The relative efficiency of propositional proof systems.
224: \newblock {\em Journal of Symbolic Logic}, 44:26--50, 1979.
225:
226: \bibitem{dll62}
227: M.~Davis, G.~Logemann, and D.~Loveland.
228: \newblock A machine program for theorem-proving.
229: \newblock {\em Communications of the ACM}, 5:394--397, 1962.
230:
231: \bibitem{davis60}
232: M.~Davis and H.~Putnam.
233: \newblock A computing procedure for quantification theory.
234: \newblock {\em J. ACM}, 7(3):201--215, 1960.
235:
236: \bibitem{dechter:ai-90}
237: R.~Dechter.
238: \newblock Enhancement schemes for constraint processing: Backjumping, learning
239: and cutset decomposition.
240: \newblock {\em Artificial Intelligence}, 41(3):273--312, 1990.
241:
242: \bibitem{dechter03}
243: R.~Dechter.
244: \newblock {\em Constraint Processing}.
245: \newblock Morgan-Kauffmann, 2003.
246:
247: \bibitem{edelkamp:ecp-01}
248: S.~Edelkamp.
249: \newblock Planning with pattern databases.
250: \newblock In {\em Proc. ECP'01}, pages 13--24, 2001.
251:
252: \bibitem{een:biere:sat-05}
253: N.~Een and A.~Biere.
254: \newblock Effective preprocessing in {SAT} through variable and clause
255: elimination.
256: \newblock In {\em Proc. SAT-05}, 2005.
257:
258: \bibitem{een:soerensson:sat-03}
259: N.~Een and N.~S{\"o}rensson.
260: \newblock An extensible {SAT} solver.
261: \newblock In {\em Proc. SAT-03}, 2003.
262:
263: \bibitem{fikes:nilsson:ai-71}
264: R.~Fikes and N.~Nilsson.
265: \newblock {STRIPS}: A new approach to the application of theorem proving to
266: problem solving.
267: \newblock {\em Artificial Intelligence}, 2:189--208, 1971.
268:
269: \bibitem{frank:etal:jair-97}
270: J.~Frank, P.~Cheeseman, and J.~Stutz.
271: \newblock When gravity fails: Local search topology.
272: \newblock {\em Journal of Artificial Intelligence Research}, 7:249--281, 1997.
273:
274: \bibitem{gent:walsh:ecai-94}
275: I.~Gent and T.~Walsh.
276: \newblock The {SAT} phase transition.
277: \newblock In {\em Proc. ECAI'94}, pages 105--109, 1994.
278:
279: \bibitem{gerevini:etal:jair-03}
280: Alfonso Gerevini, Alessandro Saetti, and Ivan Serina.
281: \newblock Planning through stochastic local search and temporal action graphs.
282: \newblock {\em Journal of Artificial Intelligence Research}, 20:239--290, 2003.
283:
284: \bibitem{haken:tcs-85}
285: A.~Haken.
286: \newblock The intractability of resolution.
287: \newblock {\em Theoretical Computer Science}, 39:297--308, 1985.
288:
289: \bibitem{haslum:etal:aaai-05}
290: P.~Haslum, B.~Bonet, and H.~Geffner.
291: \newblock New admissible heuristics for domain-independent planning.
292: \newblock In {\em Proc. AAAI'05}, 2005.
293:
294: \bibitem{helmert:icaps-04}
295: Malte Helmert.
296: \newblock A planning heuristic based on causal graph analysis.
297: \newblock In {\em Proc. ICAPS'04}, pages 161--170, 2004.
298:
299: \bibitem{hoffmann:edelkamp:jair-05}
300: J.~Hoffmann and S.~Edelkamp.
301: \newblock The deterministic part of {IPC-4}: An overview.
302: \newblock {\em Journal of Artificial Intelligence Research}, 24:519--579, 2005.
303:
304: \bibitem{hoffmann:etal:jair-06}
305: J.~Hoffmann, S.~Edelkamp, S.~Thiebaux, R.~Englert, F.~Liporace, and S.~Tr\"ug.
306: \newblock Engineering benchmarks for planning: the domains used in the
307: deterministic part of {IPC-4}.
308: \newblock {\em Journal of Artificial Intelligence Research}, 2006.
309: \newblock Submitted.
310:
311: \bibitem{hoffmann:geffner:icaps-03}
312: J.~Hoffmann and H.~Geffner.
313: \newblock Branching matters: Alternative branching in graphplan.
314: \newblock In {\em Proc. ICAPS'03}, pages 22--31, 2003.
315:
316: \bibitem{hoffmann:etal:tr-lmcs06}
317: J.~Hoffmann, C.~Gomes, and B.~Selman.
318: \newblock Structure and problem hardness: Goal asymmetry and {DPLL} proofs in
319: {SAT}-based planning.
320: \newblock Technical Report, 2007.
321: \newblock Available at
322: http://members.deri.at/$\sim$joergh/papers/tr-lmcs07.ps.gz.
323:
324: \bibitem{hoffmann:nebel:jair-01}
325: J.~Hoffmann and B.~Nebel.
326: \newblock The {FF} planning system: Fast plan generation through heuristic
327: search.
328: \newblock {\em Journal of Artificial Intelligence Research}, 14:253--302, 2001.
329:
330: \bibitem{hoffmann:etal:jair-04}
331: J.~Hoffmann, J.~Porteous, and L.~Sebastia.
332: \newblock Ordered landmarks in planning.
333: \newblock {\em Journal of Artificial Intelligence Research}, 22:215--278, 2004.
334:
335: \bibitem{hoffmann:jair-05}
336: J{\"o}rg Hoffmann.
337: \newblock Where `ignoring delete lists' works: Local search topology in
338: planning benchmarks.
339: \newblock {\em Journal of Artificial Intelligence Research}, 24:685--758, 2005.
340:
341: \bibitem{Hogg96}
342: T.~Hogg, B.~Huberman, and C.~Williams.
343: \newblock {Phase Transitions and Complexity}.
344: \newblock {\em Artificial Intelligence}, 81, 1996.
345:
346: \bibitem{howe:dahlman:jair-02}
347: A.~Howe and E.~Dahlman.
348: \newblock A critical assessment of benchmark comparison in planning.
349: \newblock {\em Journal of Artificial Intelligence Research}, 17:1--33, 2002.
350:
351: \bibitem{Hulubei05}
352: T.~Hulubei and B.~Sullivan.
353: \newblock Optimal refutations for constraint satisfaction problems.
354: \newblock In {\em Proc. IJCAI05}, 2005.
355:
356: \bibitem{iwama:miyazaki:ac-99}
357: K.~Iwama and S.~Miyazaki.
358: \newblock Tree-like resolution is super-polynomially slower than {DAG}-like
359: resolution for the pigeonhole principle.
360: \newblock In {\em Proc. Algorithms and Computation}, pages 133--142, 1999.
361:
362: \bibitem{kautz:selman:ecai-92}
363: H.~Kautz and B.~Selman.
364: \newblock Planning as satisfiability.
365: \newblock In {\em Proc. ECAI'92}, pages 359--363, 1992.
366:
367: \bibitem{kautz:selman:aaai-96}
368: H.~Kautz and B.~Selman.
369: \newblock Pushing the envelope: Planning, propositional logic, and stochastic
370: search.
371: \newblock In {\em Proc. AAAI'96}, pages 1194--1201, 1996.
372:
373: \bibitem{kautz:selman:ijcai-99}
374: H.~Kautz and B.~Selman.
375: \newblock Unifying {SAT}-based and graph-based planning.
376: \newblock In {\em Proc. IJCAI'99}, pages 318--325, 1999.
377:
378: \bibitem{kirkpatrick:clark:ibm-66}
379: T.~Kirkpatrick and N.~Clark.
380: \newblock {PERT} as an aid to logic deaign.
381: \newblock {\em IBM Journal on Research Development}, 10(2):135--141, 1966.
382:
383: \bibitem{koehler:schuster:aips-00}
384: J.~Koehler and K.~Schuster.
385: \newblock Elevator control as a planning problem.
386: \newblock In {\em Proc. AIPS'00}, pages 331--338, 2000.
387:
388: \bibitem{long:fox:jair-03}
389: D.~Long and M.~Fox.
390: \newblock The 3rd international planning competition: Results and analysis.
391: \newblock {\em Journal of Artificial Intelligence Research}, 20:1--59, 2003.
392:
393: \bibitem{sadowska:xiao:dac-01}
394: M.~Marek-Sadowska and T.~Xiao.
395: \newblock Functional correlation analysis in crosstalk induced critical paths
396: identification.
397: \newblock In {\em Proc. DAC'01}, pages 653--656, 2001.
398:
399: \bibitem{moskewicz:etal:dac-01}
400: M.~Moskewicz, C.~Madigan, Y.~Zhao, L.~Zhang, and S.~Malik.
401: \newblock Chaff: Engineering an efficient {SAT} solver.
402: \newblock In {\em Proc. DAC'01}, pages 530--535, 2001.
403:
404: \bibitem{Nudelman04}
405: E.~Nudelman, K.~Leyton-Brown, H.~Hoos, A.~Devkar, and Y.~Shoham.
406: \newblock {Understanding random SAT: beyond the clauses-to-variable ratio}.
407: \newblock In {\em Proc. CP-04}, pages 438--452, 2004.
408:
409: \bibitem{razborov:jcss:04}
410: A.~Razborov.
411: \newblock Resolution lower bounds for perfect matching principles.
412: \newblock {\em J. Computer and Systems Sciences}, 69(1):3--27, 2004.
413:
414: \bibitem{rintanen:kr-98}
415: J.~Rintanen.
416: \newblock A planning algorithm not based on directional search.
417: \newblock In {\em Proceedings KR'98}, pages 617--624, 1998.
418:
419: \bibitem{rintanen:icaps-04}
420: J.~Rintanen.
421: \newblock Phase transitions in classical planning: An experimental study.
422: \newblock In {\em Proc. ICAPS'04}, pages 101--110, 2004.
423:
424: \bibitem{rish:dechter:jar-00}
425: I.~Rish and R.~Dechter.
426: \newblock Resolution versus search: Two strategies for {SAT}.
427: \newblock {\em Journal of Automated Rreasoning}, 24(1/2):225--275, 2000.
428:
429: \bibitem{sabharwal:aaai-05}
430: A.~Sabharwal.
431: \newblock Symchaff: A structure-aware satisfiability solver.
432: \newblock In {\em Proc. AAAI'05}, pages 467--474, 2005.
433:
434: \bibitem{slaney:thiebaux:ai-01}
435: J.~Slaney and S.~Thiebaux.
436: \newblock Blocks world revisited.
437: \newblock {\em Artificial Intelligence}, 125:119--153, 2001.
438:
439: \bibitem{SW01}
440: J.~Slaney and T.~Walsh.
441: \newblock Backbones in optimization and approximation.
442: \newblock In {\em Proc. IJCAI01}, 2001.
443:
444: \bibitem{streeter:smith:icaps-05}
445: M.~Streeter and S.~Smith.
446: \newblock Characterizing the distribution of low-makespan schedules in the job
447: shop scheduling problem.
448: \newblock In {\em Proc. ICAPS'05}, pages 61--70, 2005.
449:
450: \bibitem{veloso:blythe:aips-94}
451: M.~Veloso and J.~Blythe.
452: \newblock Linkability: Examining causal link commitments in partial order
453: planning.
454: \newblock In {\em Proc. AIPS'94}, pages 170--175, 1994.
455:
456: \bibitem{wah:chen:ijait-04}
457: Benjamin Wah and Yixin Chen.
458: \newblock Subgoal partitioning and global search for solving temporal planning
459: problems in mixed space.
460: \newblock {\em International Journal of Artificial Intelligence Tools},
461: 13(4):767--790, 2004.
462:
463: \bibitem{watson:etal:informs-02}
464: J.~Watson, L.~Barbulescu, L.~Whitley, and A.~Howe.
465: \newblock Contrasting structured and random permutation flow-shop scheduling
466: problems: Search space topology and algorithm performance.
467: \newblock {\em INFORMS Journal on Computing}, 14(2):98--123, 2002.
468:
469: \bibitem{watson:etal:ecp-01}
470: J.~Watson, J.~Beck, L.~Barbulescu, and L.~Whitley.
471: \newblock Toward a descriptive model of local search cost in job-shop
472: scheduling.
473: \newblock In {\em Proc. ECP'01}, 2001.
474:
475: \bibitem{watson:etal:ai-03}
476: J.~Watson, J.~Beck, A.~Howe, and D.~Whitley.
477: \newblock Problem difficulty for tabu search in job-shop scheduling.
478: \newblock {\em Artificial Intelligence}, 143(2):189--217, 2003.
479:
480: \bibitem{williams:etal:ijcai-03}
481: R.~Williams, C.~Gomes, and B.~Selman.
482: \newblock Backdoors to typical case complexity.
483: \newblock In {\em Proc. IJCAI'03}, 2003.
484:
485: \bibitem{yen:etal:dac-89}
486: S.~Yen, D.~du, and S.~Ghanta.
487: \newblock Efficient algorithms for extracting the k most critical paths in
488: timing analysis.
489: \newblock In {\em Proc. DAC'89}, pages 649-- 654, 1989.
490:
491: \end{thebibliography}
492:
493:
494: \ifTR{
495: \newpage
496: \appendix
497: \input{proofs}
498: \input{cutsets}
499: }
500:
501: \end{document}
502:
503:
504:
505: