Сокращение планирования до количественных булевых формул

Question

Почему бы нам не сократить проблему планирования в AI до TQBF версии SAT в практических решениях.вниз "или сводится к проблеме SAT, которая в свою очередь решается SAT Solvers.Проблема заключается в том, что, поскольку планирование выполняется в PSPACE Complete, а SAT - в NP Complete, может потребоваться экспоненциальное число литералов.

Почему же практические планировщики используют этот подход?Почему бы нам всем не решить TQBF SAT, а затем "скомпилировать" планирование до TQBF, что в любом случае должно занять только полиномиальное время?

Answer 1

Это уже было сделано.

Обычно TQBF используется для моделирования согласованного планирования, но существуют кодировки чисто логических задач планирования логики в (полиномиальных) формул TQBF.

Основным недостатком является то, что, хотя у нас гораздо меньшая формула, решить ее не всегда просто.Решение TQBF далеко не настолько зрелое, как исследование по решению SAT, а планирование как TQBF все еще отстает в производительности.

Вот одна публикация, подробно описывающая такое преобразование (мое):

http://users.cecs.anu.edu.au/~ssanner/ICAPS_2010_DC/Abstracts/cashmore.pdf

Answer 2

SAT решатели сегодня высоко оптимизированы и способны использовать структуру внутри проблем.Они очень быстро справляются с большинством задач (но они не могут быть быстрыми на всех, потому что SAT труден).

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

Возможно, при умном составлении задачи планирования и использовании структуры планирования на этом шаге выбыть в состоянии получить более простые экземпляры SAT.Но при этом можно было бы сказать, что вы снова пытаетесь решить проблему планирования, просто с помощью другой вычислительной модели (SAT-решатель вместо машины с произвольным доступом или, более того, LISP).

Так почему бы не TQBF?

Очевидно, потому что никто еще не пробовал (что я не могу подтвердить).Возможно, никто раньше не имел этой идеи, или, может быть, никто не думал, что современные TQBF-решатели достаточно умны, чтобы быстро решать скомпилированные задачи планирования - по крайней мере, быстрее, чем современные планировщики.

Я не очень хорошо осведомлен в сцене решателя TQBF.На самом деле, я никогда не слышал о чем-то вроде общего решения TQBF (за исключением логического программирования в целом).Я думаю, что это намного сложнее, чем SAT (что еще не доказано, предположительно, Деолаликар неправ).

Итак, попробуйте и попробуйте.Вы можете опубликовать ссылку на вашу публикацию здесь, если вам это удастся.