?. .. {1, +. 1}, ?. T. {1, R. Majumdar, T. Millstein et al., The pigeon hole planning task P P HP (i) is defined as follows For each hole h, there is a fact free(h) The initial state contains all i free facts but no assigned facts. The goal state contains all i+1 assigned facts. The only available actions (other than noops) are put(p, h), which puts pigeon p into a free hole h, after which h no longer remains free The plan length bound b(i) is set to 1. Consider any one of the four encoding methods (A)?(D), and let ?(i) be the encoding of P P HP (i) Restrict ?(i) by setting all noop variables to False; this has no real " restrictive " implication in terms of planning since the plan length bound is 1 and none of the goal facts are available at time step 0. For the action-only encodings (A) and (C), identifying the action variables put(p, h) with the PHP(i) variables x p,h immediately yields precisely the clauses of PHP(i): the goal clauses of ?(i) become the pigeon clauses of PHP(i) and the action mutex clauses become the hole clauses. For the action-fact encodings (B) and (D), fix all free fact variables at time step 0 as well as all assigned fact variables at time step 1 to True, and identify put(p, h) action variables as above with x p,h . This again yields precisely the clauses of PHP(i) It follows from the resolution hardness of PHP(i) and Proposition 2.1 that any resolution proof of the fact that the planning task P P HP (i) does not have a plan of length 1 must require size exponential in i. The claim now follows from a planning task P ? (i) which consists of a combination of two disconnected pigeon hole planning sub-tasks, P P HP (i) and P P HP (1), over two separate sets of pigeon and hole objects. The goal for P ? (i) is naturally defined as follows: put the first set of i + 1 pigeons into the first set of i holes and put the second set of two pigeons into the second set of holes (which consists of only a single hole) The overall CNF encoding ? ? (i) of P ? (i) is the logical conjunction of the encodings ?(i) and ?(1) (on disjoint sets of variables) of P P HP (i) and P P HP (1) Observe that ? ? (i) can be proved unsatisfiable by proving unsatisfiability of either of the two pigeon hole problems. In particular, there is a constant size resolution refutation of ? ? (i) which involves refuting the ?(1) component. On the other hand, we argue that all of the listed abstractions can make the one-hole component of P ? (i) trivially satisfiable, so that a resolution refutation of the abstracted task must resort to a proof of unsatisfiability of the i-hole component ?(i) of P ? (i), which we have shown requires exponential size. Hence the single example P ? (i) serves to show the claim for all combinations of abstraction method and CNF encoding. It is easily verified that P P HP (1) becomes solvable when ignoring the precondition free(1) of both put(1, 1) and put(2, 1): we can then put both pigeons into the single hole. The same happens when ignoring the delete effect free(1) of both put(1, 1) and put(2, 1)When ignoring the goal assigned Automatic predicate abstraction of C programs, or when inserting assigned (2) into the initial state, or when completely removing assigned) are persistently mutex in P P HP (1) because the only actions achieving them are put(1, 1) and put respectively. According to Definition 2.2, we can hence replace assigned the resulting planning task, we have the References Ball, PLDI'2001: Programming Language Design and Implementation, pp.203-213, 2001.

P. Beame, H. Kautz, and A. Sabharwal, Towards understanding and harnessing the potential of clause learning, Journal of Artificial Intelligence Research, vol.22, pp.319-351, 2004.

A. Blum and M. Furst, Fast planning through planning graph analysis, Artificial Intelligence, vol.90, issue.1-2, pp.279-298, 1997.
DOI : 10.1016/S0004-3702(96)00047-1

URL : http://doi.org/10.1016/s0004-3702(96)00047-1

A. L. Blum and M. L. Furst, Fast planning through planning graph analysis, Proceedings of the 14th International Joint Conference on Artificial Intelligence (IJCAI-95), pp.1636-1642, 1995.
DOI : 10.1016/S0004-3702(96)00047-1

B. Bonet and H. Geffner, Planning as heuristic search, Artificial Intelligence, vol.129, issue.1-2, pp.5-33, 2001.
DOI : 10.1016/S0004-3702(01)00108-4

URL : http://doi.org/10.1016/s0004-3702(01)00108-4

B. Bonet and H. Geffner, Heuristics for planning with penalties and rewards formulated in logic and computed through circuits, Artificial Intelligence, vol.172, issue.12-13, pp.12-13, 2008.
DOI : 10.1016/j.artint.2008.03.004

R. Brafman, On reachability, relevance, and resolution in the planning as satisfiability approach, Journal of Artificial Intelligence Research, vol.14, pp.1-28, 2001.

S. Chaki, E. Clarke, A. Groce, S. Jha, and H. Veith, Modular verification of software components in C, ICSE'2003: Int. Conf. on Software Engineering, pp.385-395, 2003.

Y. Chen, R. Huang, Z. Xing, and W. Zhang, Long-distance mutual exclusion for planning, Artificial Intelligence, vol.173, issue.2, pp.365-391, 2009.
DOI : 10.1016/j.artint.2008.11.004

URL : http://doi.org/10.1016/j.artint.2008.11.004

E. M. Clarke, A. Biere, R. Raimi, and Y. Zhu, Bounded model checking using satisfiability solving, Formal Methods in System Design, vol.19, issue.1, pp.7-34, 2001.
DOI : 10.1023/A:1011276507260

E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, Counterexample-guided abstraction refinement for symbolic model checking, Journal of the ACM, vol.50, issue.5, pp.50-752, 2003.
DOI : 10.1145/876638.876643

M. Davis, G. Logemann, and D. Loveland, A machine program for theorem-proving, Communications of the ACM, vol.5, issue.7, pp.394-397, 1962.
DOI : 10.1145/368273.368557

M. Davis and H. Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM, vol.7, issue.3, pp.201-215, 1960.
DOI : 10.1145/321033.321034

S. Edelkamp, Planning with pattern databases, Recent Advances in AI Planning. 6th European Conference on Planning (ECP'01), pp.13-24, 2001.

S. Edelkamp, Promela Planning, Proceedings of the 10th International SPIN Workshop on Model Checking of Software (SPIN-03), pp.197-212, 2003.
DOI : 10.1007/3-540-44829-2_13

S. Edelkamp and M. Helmert, Exhibiting Knowledge in Planning Problems to Minimize State Encoding Length, Recent Advances in AI Planning. 5th European Conference on Planning (ECP'99), pp.135-147, 1999.
DOI : 10.1007/10720246_11

M. Ernst, T. Millstein, and D. Weld, Automatic sat-compilation of planning problems, Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI-97), pp.1169-1176, 1997.

R. E. Fikes and N. J. Nilsson, Strips: A new approach to the application of theorem proving to problem solving, Artificial Intelligence, vol.2, issue.3-4, pp.3-4, 1971.
DOI : 10.1016/0004-3702(71)90010-5

A. Gerevini, A. Saetti, and I. Serina, Planning through stochastic local search and temporal action graphs, Journal of Artificial Intelligence Research, vol.20, pp.239-290, 2003.

S. Graf and H. Sa¨?disa¨?di, Construction of abstract state graphs with PVS, CAV'1997: Computer Aided Verification, pp.72-83, 1997.
DOI : 10.1007/3-540-63166-6_10

A. Gupta and O. Strichman, Abstraction Refinement for Bounded Model Checking, Proceedings of the 17th International Conference on Computer Aided Verification (CAV'05), Lecture Notes in Computer Science, pp.112-124, 2005.
DOI : 10.1007/11513988_11

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.91.239

A. Haken, The intractability of resolution, Theoretical Computer Science, vol.39, pp.297-308, 1985.
DOI : 10.1016/0304-3975(85)90144-6

P. Haslum and H. Geffner, Admissible heuristics for optimal planning, Proceedings of the 5th International Conference on Artificial Intelligence Planning Systems (AIPS-00), pp.140-149, 2000.

P. Haslum, A. Botea, M. Helmert, B. Bonet, and S. Koenig, Domain-independent construction of pattern database heuristics for cost-optimal planning, Proceedings of the Twenty-Second AAAI Conference on Artificial Intelligence (AAAI-2007), pp.1007-1012, 2007.

M. Helmert and R. Mattmüller, Accuracy of admissible heuristic functions in selected planning domains, Proceedings of the 23rd AAAI Conference on Artificial Intelligence, pp.938-943, 2008.

M. Helmert, P. Haslum, and J. Hoffmann, Flexible abstraction heuristics for optimal sequential planning, pp.176-183, 2007.

T. Henzinger, R. Jhala, R. Majumdar, and K. Mcmillan, Abstractions from proofs, POPL'2004: Principles of Programming Languages, pp.232-244, 2004.
DOI : 10.1145/964001.964021

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.1200

I. Hernadvölgyi and R. Holte, PSVN: A vector representation for production systems, 1999.

J. Hoffmann and S. Edelkamp, The deterministic part of IPC-4: An overview, Journal of Artificial Intelligence Research, vol.24, pp.519-579, 2005.

J. Hoffmann and B. Nebel, The FF planning system: Fast plan generation through heuristic search, Journal of Artificial Intelligence Research, vol.14, pp.253-302, 2001.

J. Hoffmann, Where 'ignoring delete lists' works: Local search topology in planning benchmarks, Journal of Artificial Intelligence Research, vol.24, pp.685-758, 2005.

J. Hoffmann, C. Gomes, and B. Selman, Structure and Problem Hardness: Goal Asymmetry and DPLL Proofs in SAT-Based Planning, Logical Methods in Computer Science, vol.3, issue.1, 2007.
DOI : 10.2168/LMCS-3(1:6)2007

J. Hoffmann, A. Sabharwal, and C. Domshlak, Friends or foes? an AI planning perspective on abstraction and search, pp.294-303, 2006.

M. Katz and C. Domshlak, Structural pattern heuristics via fork decomposition, pp.182-189, 2008.

H. Kautz and B. Selman, Unifying SAT-based and graph-based planning, Proceedings of the 16th International Joint Conference on Artificial Intelligence (IJCAI-99), pp.318-325, 1999.

H. Kautz, SATPLAN04: Planning as satisfiability, Proceedings of the 4th International Planning Competition, 2004.

H. Kautz, B. Selman, and J. Hoffmann, SATPLAN: Planning as satisfiability, Proceedings of the 5th International Planning Competition (IPC-06), 2006.

H. A. Kautz, D. Mcallester, and B. Selman, Encoding plans in propositional logic, Principles of Knowledge Representation and Reasoning: Proceedings of the 5th International Conference (KR-96), pp.374-384, 1996.

H. A. Kautz and B. Selman, Planning as satisfiability, Proceedings of the 10th European Conference on Artificial Intelligence (ECAI-92), pp.359-363, 1992.

H. A. Kautz and B. Selman, Pushing the envelope: Planning, propositional logic, and stochastic search, Proceedings of the 13th National Conference of the American Association for Artificial Intelligence (AAAI-96), pp.1194-1201, 1996.

C. A. Knoblock, Learning abstraction hierarchies for problem solving, Proceedings of the 8th National Conference of the American Association for Artificial Intelligence (AAAI-90), pp.923-928, 1990.

J. Koehler, B. Nebel, J. Hoffmann, and Y. Dimopoulos, Extending planning graphs to an ADL subset, pp.273-285, 1997.
DOI : 10.1007/3-540-63912-8_92

J. Koehler and J. Hoffmann, On reasonable and forced goal orderings and their use in an agenda-driven planning algorithm, Journal of Artificial Intelligence Research, vol.12, pp.338-386, 2000.

D. Long, H. A. Kautz, B. Selman, B. Bonet, H. Geffner et al., The aips-98 planning competition, pp.13-33, 2000.

D. Mcdermott, Using regression-match graphs to control search in planning, Artificial Intelligence, vol.109, issue.1-2, pp.111-159, 1999.
DOI : 10.1016/S0004-3702(99)00010-7

N. Meuleau, R. Brafman, and E. Benazera, Stochastic over-subscription planning using hierarchies of MDPs, pp.121-130, 2006.

B. Nebel, Y. Dimopoulos, and J. Koehler, Ignoring irrelevant facts and operators in plan generation, pp.338-350, 1997.
DOI : 10.1007/3-540-63912-8_97

C. Abstract, M. R. Prasad, A. Biere, and A. Gupta, A survey of recent advances in sat-based formal verification, Friends or Foes? On Planning as Satisfiability, pp.156-173, 2005.

K. Ray and M. L. Ginsberg, The complexity of optimal planning and a more efficient method for finding solutions, Beck et al, pp.280-287, 2008.

J. Rintanen, Evaluation strategies for planning as satisfiability, Proceedings of the 16th European Conference on Artificial Intelligence (ECAI-04), pp.682-687, 2004.

J. Rintanen, Planning graphs and propositional clause-learning, Principles of Knowledge Representation and Reasoning: Proceedings of the 11th International Conference (KR-08), pp.535-543, 2008.

J. Rintanen, K. Heljanko, and I. Niemelä, Planning as satisfiability: parallel plans and algorithms for plan search, artificial intelligence, Artificial Intelligence, vol.170, pp.12-13, 2006.
DOI : 10.1016/j.artint.2006.08.002

URL : http://doi.org/10.1016/j.artint.2006.08.002

J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM, vol.12, issue.1, pp.23-41, 1965.
DOI : 10.1145/321250.321253

N. Robinson, C. Gretton, D. Pham, A. Sattar, and . Beck, A compact and efficient sat encoding for planning, Beck et al, pp.296-303, 2008.

E. Sacerdoti, Planning in a hierarchy of abstraction spaces, Proceedings of the 3rd International Joint Conference on Artificial Intelligence (IJCAI-73), pp.412-422, 1973.
DOI : 10.1016/0004-3702(74)90026-5

R. Sanchez and S. Kambhampati, Planning graph heuristics for selecting objectives in over-subscription planning problems, Proceedings of the 15th International Conference on Automated Planning and Scheduling (ICAPS-05), pp.192-201, 2005.

S. Steel and R. Alami, Recent Advances in AI Planning, 4th European Conference on Planning (ECP'97), 1997.
DOI : 10.1007/3-540-63912-8

M. Streeter and . Smith, Using decision procedures efficiently for optimization, Boddy et, pp.312-319, 2007.