Planning as satisfiability: heuristics. (English) Zbl 1270.68276

Rintanen, Jussi

Artif. Intell. 193, 45-86 (2012).

Summary: Reduction to SAT is a very successful approach to solving hard combinatorial problems in artificial intelligence and computer science in general. Most commonly, problem instances reduced to SAT are solved with a general-purpose SAT solver. Although there is the obvious possibility of improving the SAT solving process with application-specific heuristics, this has rarely been done successfully.
In this work we propose a planning-specific variable selection strategy for SAT solving. The strategy is based on generic principles about properties of plans, and its performance with standard planning benchmarks often substantially improves on generic variable selection heuristics, such as VSIDS, and often lifts it to the same level with other search methods such as explicit state-space search with heuristic search algorithms.

© Elsevier B.V.

MSC:

68T20

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)

Software:

Walksat; Siege; MathSAT; Graphplan; Chaff

References:

[1]	Kautz, H.; Selman, B., Planning as satisfiability, 359-363
[2]	S.A. Cook, The complexity of theorem proving procedures, in: Proceedings of the Third Annual ACM Symposium on Theory of Computing, pp. 151–158. · Zbl 0253.68020
[3]	Kautz, H.; Selman, B., Pushing the envelope: planning, propositional logic, and stochastic search, 1194-1201
[4]	Biere, A.; Cimatti, A.; Clarke, E. M.; Zhu, Y., Symbolic model checking without BDDs, 193-207
[5]	Marques-Silva, J. P.; Sakallah, K. A., GRASP: a search algorithm for propositional satisfiability, IEEE Transactions on Computers, 48, 506-521, 1999 · Zbl 1392.68388
[6]	R.J. Bayardo Jr., R.C. Schrag, Using CSP look-back techniques to solve real-world SAT instances, in: Proceedings of the 14th National Conference on Artificial Intelligence (AAAI-97) and 9th Innovative Applications of Artificial Intelligence Conference (IAAI-97), pp. 203–208.
[7]	Moskewicz, M. W.; Madigan, C. F.; Zhao, Y.; Zhang, L.; Malik, S., Chaff: engineering an efficient SAT solver, 530-535
[8]	Bonet, B.; Geffner, H., Planning as heuristic search, Artificial Intelligence, 129, 5-33, 2001 · Zbl 0971.68146
[9]	Grastien, A.; Anbulagan; Rintanen, J.; Kelareva, E., Diagnosis of discrete-event systems using satisfiability algorithms, 305-310
[10]	A. Porco, A. Machado, B. Bonet, Automatic polytime reductions of NP problems into a fragment of STRIPS, in: ICAPS 2011. Proceedings of the Twenty-First International Conference on Automated Planning and Scheduling, pp. 178–185.
[11]	Rintanen, J., Phase transitions in classical planning: an experimental study, 710-719
[12]	Rintanen, J.; Heljanko, K.; Niemelä, I., Planning as satisfiability: parallel plans and algorithms for plan search, Artificial Intelligence, 170, 1031-1080, 2006 · Zbl 1131.68099
[13]	Blum, A. L.; Furst, M. L., Fast planning through planning graph analysis, Artificial Intelligence, 90, 281-300, 1997 · Zbl 1017.68533
[14]	Selman, B.; Kautz, H. A.; Cohen, B., Noise strategies for improving local search, 337-343
[15]	B. Selman, H.A. Kautz, B. Cohen, Local search strategies for satisfiability testing, in: DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 25, 1996, pp. 521–531. · Zbl 0864.90093
[16]	Crawford, J. M.; Auton, L. D., Experimental results on the crossover point in random 3-SAT, Artificial Intelligence, 81, 31-57, 1996 · Zbl 1508.68324
[17]	Bonet, B.; Loerincs, G.; Geffner, H., A robust and fast action selection mechanism for planning, 714-719
[18]	Rintanen, J., Evaluation strategies for planning as satisfiability, 682-687
[19]	Rintanen, J.; Heljanko, K.; Niemelä, I., Parallel encodings of classical planning as satisfiability, 307-319 · Zbl 1111.68660
[20]	Li, C. M.; Anbulagan, Heuristics based on unit propagation for satisfiability problems, 366-371
[21]	Rintanen, J., A planning algorithm not based on directional search, 617-624
[22]	Davis, M.; Logemann, G.; Loveland, D., A machine program for theorem proving, Communications of the ACM, 5, 394-397, 1962 · Zbl 0217.54002
[23]	Rintanen, J., Heuristics for planning with SAT, 414-428
[24]	Wehrle, M.; Rintanen, J., Planning as satisfiability with relaxed ∃-step plans, 244-253
[25]	Ogata, S.; Tsuchiya, T.; Kikuno, T., SAT-based verification of safe Petri nets, 79-92 · Zbl 1108.68082
[26]	Gerevini, A.; Schubert, L., Inferring state constraints for domain-independent planning, 905-912
[27]	Beame, P.; Kautz, H.; Sabharwal, A., Towards understanding and harnessing the potential of clause learning, Journal of Artificial Intelligence Research, 22, 319-351, 2004 · Zbl 1080.68651
[28]	Mitchell, D. G., A SAT solver primer, EATCS Bulletin, 85, 112-133, 2005 · Zbl 1169.68444
[29]	Gomes, C. P.; Selman, B.; Crato, N.; Kautz, H., Heavy-tailed phenomena in satisfiability and constraint satisfaction problems, Journal of Automated Reasoning, 24, 67-100, 2000 · Zbl 0967.68145
[30]	Gomes, C. P.; Selman, B.; Kautz, H., Boosting combinatorial search through randomization, 431-437
[31]	Rintanen, J., Regression for classical and nondeterministic planning, 568-571
[32]	Rintanen, J., Engineering efficient planners with SAT, 684-689
[33]	Pipatsrisawat, K.; Darwiche, A., A lightweight component caching scheme for satisfiability solvers, 294-299
[34]	Zarpas, E., Simple yet efficient improvements of SAT based bounded model checking, 174-185 · Zbl 1117.68439
[35]	M. Streeter, S.F. Smith, Using decision procedures efficiently for optimization, in: M. Boddy, M. Fox, S. Thiébaux (Eds.), ICAPS 2007. Proceedings of the Seventeenth International Conference on Automated Planning and Scheduling, pp. 312–319.
[36]	D. McDermott, The planning domain definition language, Technical Report CVC TR-98-003/DCS TR-1165, Yale Center for Computational Vision and Control, Yale University, 1998.
[37]	Rintanen, J., Heuristics for planning with SAT and expressive action definitions, 210-217
[38]	Gerevini, A.; Serina, I., Planning as propositional CSP: from Walksat to local search techniques for action graphs, Constraints Journal, 8, 389-413, 2003 · Zbl 1074.68612
[39]	Kautz, H.; Selman, B., Unifying SAT-based and graph-based planning, 318-325
[40]	Richter, S.; Westphal, M., The LAMA planner: guiding cost-based anytime planning with landmarks, Journal of Artificial Intelligence Research, 39, 127-177, 2010 · Zbl 1205.68383
[41]	ICAPS, http://www.icaps-conference.org/, 2010.
[42]	Bylander, T., A probabilistic analysis of propositional STRIPS planning, Artificial Intelligence, 81, 241-271, 1996 · Zbl 1508.68323
[43]	J. Rintanen, Generation of hard solvable planning problems, Technical Report TR-CS-12-03, Research School of Computer Science, The Australian National University, 2012.
[44]	Huberman, B. A.; Lukose, R. M.; Hogg, T., An economics approach to hard computational problems, Science, 275, 51-54, 1997
[45]	Gomes, C. P.; Selman, B., Algorithm portfolio design: theory vs. practice, 190-197
[46]	Gomes, C. P.; Selman, B., Algorithm portfolios, Journal of Artificial Intelligence Research, 126, 43-62, 2001 · Zbl 0969.68047
[47]	Hoffmann, J.; Nebel, B., The FF planning system: fast plan generation through heuristic search, Journal of Artificial Intelligence Research, 14, 253-302, 2001 · Zbl 0970.68044
[48]	Vidal, V., A lookahead strategy for heuristic search planning, 150-160
[49]	Cheeseman, P.; Kanefsky, B.; Taylor, W. M., Where the really hard problems are, 331-337 · Zbl 0747.68064
[50]	Mitchell, D.; Selman, B.; Levesque, H., Hard and easy distributions of SAT problems, 459-465
[51]	Bollobás, B., Random Graphs, 1985, Academic Press · Zbl 0567.05042
[52]	L. Ryan, Efficient algorithms for clause-learning SAT solvers, Masterʼs thesis, Simon Fraser University, 2003.
[53]	Sideris, A.; Dimopoulos, Y., Constraint propagation in propositional planning, 153-160
[54]	Robinson, N.; Gretton, C.; Pham, D.-N.; Sattar, A., SAT-based parallel planning using a split representation of actions, 281-288
[55]	K. Ray, M.L. Ginsberg, The complexity of optimal planning and a more efficient method for finding solutions, in: J. Rintanen, B. Nebel, J.C. Beck, E. Hansen (Eds.), ICAPS 2008. Proceedings of the Eighteenth International Conference on Automated Planning and Scheduling, pp. 280–287.
[56]	R. Huang, Y. Chen, W. Zhang, A novel transition based encoding scheme for planning as satisfiability, in: Proceedings of the 24th AAAI Conference on Artificial Intelligence (AAAI-10), pp. 89–94.
[57]	Rintanen, J., Planning and SAT, 483-504
[58]	Cimatti, A.; Giunchiglia, E.; Giunchiglia, F.; Traverso, P., Planning via model checking: a decision procedure for \(\mathcal{AR}\), 130-142
[59]	Vidal, V.; Geffner, H., Branching and pruning: an optimal temporal POCL planner based on constraint programming, Artificial Intelligence, 170, 298-335, 2006 · Zbl 1131.68528
[60]	McAllester, D. A.; Rosenblitt, D., Systematic nonlinear planning, 634-639
[61]	Pearl, J., Heuristics: Intelligent Search Strategies for Computer Problem Solving, 1984, Addison-Wesley Publishing Company
[62]	N. Lipovetzky, H. Geffner, Inference and decomposition in planning using causal consistent chains, in: A. Gerevini, A. Howe, A. Cesta, I. Refanidis (Eds.), ICAPS 2009. Proceedings of the Nineteenth International Conference on Automated Planning and Scheduling, pp. 217–224.
[63]	Haken, A., The intractability of resolution, Theoretical Computer Science, 39, 297-308, 1985 · Zbl 0586.03010
[64]	Järvisalo, M.; Junttila, T., Limitations of restricted branching in clause learning, Constraints Journal, 14, 325-356, 2009 · Zbl 1192.68643
[65]	Bozzano, M.; Bruttomesso, R.; Cimatti, A.; Junttila, T.; van Rossum, P.; Schulz, S.; Sebastiani, R., The MathSAT 3 system, 315-321
[66]	Audemard, G.; Cimatti, A.; Kornilowicz, A.; Sebastiani, R., Bounded model checking for timed systems, 243-259 · Zbl 1037.68549
[67]	Giorgetti, N.; Pappas, G. J.; Bemporad, A., Bounded model checking of hybrid dynamical systems, 672-677
[68]	Audemard, G.; Bozzano, M.; Cimatti, A.; Sebastiani, R., Verifying industrial hybrid systems with MathSAT, Electronic Notes in Theoretical Computer Science, 119, 17-32, 2005 · Zbl 1272.68220
[69]	Rintanen, J., Constructing conditional plans by a theorem-prover, Journal of Artificial Intelligence Research, 10, 323-352, 1999 · Zbl 0916.68139
[70]	Rintanen, J., Asymptotically optimal encodings of conformant planning in QBF, 1045-1050
[71]	Majercik, S. M.; Littman, M. L., Contingent planning under uncertainty via stochastic satisfiability, Artificial Intelligence, 147, 119-162, 2003 · Zbl 1082.68807