Введение   Главы  1  2  3  4  5  6  7  8  9  10  11  12  13  14  15  16  17  18  19  20  21  22  23

 24   Приложения  1  2  

Комбинаторный взрыв






Исследованием вычислительной обозримости (или необозримости) проблем занимается теория сложности. Для начала нам потребуется только знать, что существуют классы проблем, решение которых требует ресурсов, экспоненциально возрастающих при линейном увеличении размерности задачи. Например, время, необходимое для отыскания пути в лабиринте, экспоненциально увеличивается при увеличении количества разветвлений в лабиринте. Аналогично, время, необходимое для поиска доказательства теоремы исчислением утверждений, растет экспоненциально по отношению к количеству переменных. Такие проблемы являются в общем случае необозримыми и называются NP-hard. Читателей, которые ими заинтересуются, мы отсылаем к специальной литературе, в частности книге Хопкрофта и Ульмана [Hopcroft and Ullman, 1979].

Проблемы, время решения которых связано с размерностью задачи полиномиальной функции, считаются обозримыми. Например, проверка заданного маршрута в лабиринте или проверка правильности доказательства некоторой теоремы — обозримые проблемы. Но можно показать, что, к сожалению, большинство проблем, которые интересуют нас в области искусственного интеллекта, относятся к классу NP-hard. Поэтому такое важное значение придается использованию эвристических методов при их решении.

Прекрасное изложение теории вычислительной сложности, рассчитанное на читателя, несклонного к излишнему теоретизированию, можно найти в работе Паунд-стоуна [Poundstone, 1988, Chapter 9].

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

"Если компьютер может ошибаться, он ошибется" и

"Мой компьютер может ошибаться".

Тогда, используя механизм исчислений только правил влияния, мы можем показать, что справедлива теорема.

"Мой компьютер ошибется".

Это утверждение логически следует из заданных аксиом в том смысле, что оно не может быть ложным, если истинны исходные утверждения (аксиомы). Корректности такого следствия легко доказываются компьютером — все, что от него требуется, так это обработать выражения в форме логической зависимости:

(любой Х)(F(X))

F(a) / [G(a){X/a}]

которое читается следующим образом:

"Все элементы F являются элементами G, а входит в F, следовательно, F есть G".

Как и в случае с головоломками, некоторые концепции и методы, разработанные в области машинного доказательства теорем (иногда эту область исследований называют automated reasoning — машинным поиском логического вывода), весьма помогут студентам при решении практических проблем. Итак, знания, касающиеся решения некоторой проблемы, можно представить как набор аксиом, т.е. теорию, а процесс поиска решения проблемы можно рассматривать как попытку доказать теорему, каковой является искомое решение (подробнее об этом — в главе 8). Другими словами, поиск решения среди сформулированных теорем аналогичен поиску пути на графе в пространстве состояний и для его анализа можно использовать тот же аппарат.

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



Содержание раздела