Искусный просмотр больших древовидных структур - часть 2
Проблема выполнимости для булевского выражения может трактоваться по этой схеме следующим образом. Пусть п есть число идентификаторов в выражении. Представим их конкретизацию в виде последовательности длины п логических значений - так, что i-й элемент последовательности является значением i-го идентификатора. Предположим, что булевское выражение задано в форме вычислительного предписания а, которое для конкретизации х с помощью вызова а(х) вычисляет значение выражения для этой конкретизации.
fct baum = ( seq bool х ) set seq bool:
if length(x) ³ n then {x}
else baum(<trie> о x) È baum(<false> о x)
fi
fct suchemin = ( set seq bool s ) scq bool:
if ÷sç = I then some seq bool x: x Î s
else scq bool x = some seq bool z: z Î s;
scq bool у == suchemin(s\{x});
if a(x) Ü a(y) then x
else у
fi
По вызову baum(e) порождаются все возможные различные последовательности длины п логических значений. По вызову suchemin из множества всех этих последовательностей выбирается та минимальная по времени построения последовательность, для которой a(x) дает значение «истина»; если не существует ни одной такой последовательности, то в качестве результата выдается просто самая первая из построенных последовательностей. Таким образом, через (suchemin(baum(e)) решается проблема выполнимости для булевского выражения.
Рекурсивная структура функции baum дает возможность улучшить эффективность алгоритма, если применить:
· умелое отсечение трасс, которые не обещают успеха (см. далее а/р-отсечение, бэктрекинг);
· умелый выбор порядка просмотра (см.