В первом условии сказано, что самолет Р1 должен быть в аэропорту JFK, если он находился в нем во время 0 и не улетел из JFKb какой-то другой город, неважно, какой именно; во втором условии сказано, что он должен находиться в аэропорту JFK, если он прилетел туда из другого города, неважно, из какого именно. При использовании этих расщепленных символов мы можем удалить параметр, значение которого нас не интересует:

Обратите внимание на то, что в этой аксиоме аэропорты SFO и LAX больше не упоминаются. Вообще говоря, теперь расщепленные символы действий позволяют добиться того, чтобы размер каждой аксиомы состояния-преемника был независимым от количества аэропортов. Аналогичные сокращения допускаются в аксиомах предусловия и аксиомах исключения действий. Для описанного выше случая с 10 времен-ными этапами, 12 самолетами и 30 аэропортами полная аксиома исключения действий сокращается с 583 миллионов выражений до 9360 выражений.

Но остается непреодоленным еще один недостаток: представление с помощью расщепленных символов не допускает описания параллельных действий. Рассмотрим два параллельных действия,. Преобразовав их в расщепленные представления, получим следующее:

Теперь больше нет возможности определить с помощью этого выражения, что произошло! Мы знаем, что самолетывылетели, но не можем выяснить места их отправления и назначения. Это означает, что должна использоваться полная аксиома исключения действий со всеми указанными выше недостатками.

Планировщики, основанные на проверке выполнимости, способны обрабатывать крупные задачи планирования, например находить оптимальные тридцати-этапные решения для задач планирования в мире блоков с десятками блоков. Размер пропозиционального представления и стоимость решения в высшей степени зависят от задачи, но в большинстве случаев узким местом становится нехватка памяти, требуемой для хранения пропозициональных аксиом. Одним из интересных результатов этих исследований оказалось то, что алгоритмы поиска с возвратами, такие как DPLL, часто лучше решают задачи планирования по сравнению с алгоритмами локального поиска, подобными WalkSAT. Это связано с тем, что основная часть пропозициональных аксиом представляет собой хорновские выражения, которые эффективно обрабатываются с помощью метода распространения единичных выражений. Это наблюдение привело к разработке гибридных алгоритмов, в которых комбинируется некоторый метод случайного поиска с возвратами и метод распространения единичных выражений.