Cтраница 2
Пусть Ck-дизъюнкт, выбранный на & - м шаге. TPU пытается породить какой-либо единичный дизъюнкт из Ck, Sx и S2 с множеством Wck поддержки для Ck. Если не было порождено ни одного единичного дизъюнкта, то TPU выбирает в Sa другой дизъюнкт и повторяет процесс. Если порождены какие-то единичные дизъюнкты, то TPU применяет критерий поглощения и, если возможно, критерий функциональной глубины. TPU сохраняет только те дизъюнкты, которые выдерживают эти критерии. Если найдено противоречие, программа останавливается; в противном случае она выбирает другой дизъюнкт из S3 и повторяет процесс. На каждом шаге процесса метод выбора дизъюнкта из S3 может оказаться критическим для эффективности программы. В TPU дизъюнкты из S3 выбираются последовательно. Когда S3 исчерпано, дизъюнкты выбираются снова в том же самом порядке. В программу включена стратегия поддержки. Каждый дизъюнкт из S3 имеет свое собственное множество поддержки. Различные дизъюнкты могут иметь различные множества поддержки. Они обновляются на каждом шаге. [16]