Cтраница 1
Определение 2.2. Множеством DCDP-связей называется множество связей, которые соединяют пары различных дизъюнктов, если дизъюнкты каждой пары не являются смежными со всеми дизъюнктами остальных пар. [1]
Сложность оптимального выбора DCDP-связей эквивалентна проблеме оптимальной раскраски графа. [2]
Рассмотрим проблему выбора DCDP-связей. Пусть все связи имеют метки. [3]
Рассмотрим модификацию процедуры нахождения множества DCDP-связей. [4]
Так как нахождение всех возможных множеств DCDP-связей, резольвирование по этим связям и определение наиболее подходящего варианта резольвирования является вычислительно неэффективным, необходимо использование эвристик для определения потенциально лучших кандидатов на резольвирование. [5]
Рассмотрим модификацию алгоритма DCDP-параллельного вывода. Недетерминизм определения множества DCDP-связей, в принципе, может оказывать влияние на эффективность работы алгоритма. Необходимо напомнить, что при определении множества DCDP-связей необходимо определить дизъюнкты, параллельное резольви-рование которых позволяет максимально упростить граф связей. [6]
Необходимо отметить зависимость работы алгоритмов от структуры графа связей. В графах связей с большой удельной связностью, для которых мощность множества DCDP-связей мала, наилучшие результаты показываются при использовании алгоритма OR-параллельной резолюции. В случае низкой связности графа связей наилучшие результаты дает использование DCDP-параллельного вывода. AND-параллельный вывод показывает наилучшие результаты, когда имеется множество однолитеральных дизъюнктов и SUN-дизъюнкт с большим количеством литер. [7]
Рассмотрим модификацию алгоритма DCDP-параллельного вывода. Недетерминизм определения множества DCDP-связей, в принципе, может оказывать влияние на эффективность работы алгоритма. Необходимо напомнить, что при определении множества DCDP-связей необходимо определить дизъюнкты, параллельное резольви-рование которых позволяет максимально упростить граф связей. [8]
Доказано, что DCDP-параллельная резолюция корректна. Считаем, что исходное множество дизъюнктов не имеет чистых литер и тавтологий. Предварительно построим исходный граф связей. Если граф связей содержит пустой дизъюнкт, то он невыполним и, следовательно, алгоритм достиг конечного состояния. Алгоритм DCDP-параллельной резолюции отличается от алгоритма OR-параллельной резолюции 1 - м шагом, на котором, в случае DCDP-параллельной резолюции, происходит выбор множества DCDP-связей и проводится параллельное резольвирование по всем связям из выбранного множества. [9]