§ 4. Метод на насищане на нивото
Преди това беше въведен методът на разделяне и беше дадена теорема, потвърждаваща пълнотата на метода на разделяне. Нека имаме набор от клаузи S = < D 1 ,D 2 ,…,Dk >. Процедурата за получаване на двоични разделителни способности е двусмислена, защото може да се сравнят D 1 и D 2 , след това D 1 и D 3 или по друг начин. Помислете за метода на насищане на нивото. Състои се в изчисляване на всички резолвенти на всички двойки клаузи от S, добавяне на тези разделителни способности към множеството S, изчисляване на всички следващи разделителни способности и повтаряне на този процес, докато се намери празна клауза. Това означава, че генерираме S 0 ,S 1 ,S 2 ,S 3 ,…, където S 0 =S и
За да програмираме този метод на компютър, можем първо да напишем клаузите S 0 S 1 ... след това да изчислим резолюциите, като сравним всяка клауза D j (S 0 S 1 ... ) последователно с всяка клауза D k, която се намира след D j .
PQ, PQ, PQ>. S 0 : (1) P Q;
_____________________________ използвани клаузи
(10) P P от (2) и (3);
S 2 : (13) P Q от (1) и (7);
(14) P Q от (1) и (8);
(15) P Q от (1) и (9);
(16) P Q от (1) и (10);
(20) P Q от (2) и (7);
(21) P Q от (2) и (8);
(22) P Q от (2) и (9);
(23) P Q от (2) и (10);
(26) P Q от (3) и (7);
(27) P Q от (3) и (8);
(28) P Q от (3) и (9);
(29) P Q от (3) и (10);
(33) P Q от (4) и (7);
(34) P Q от (4) и (8);
(35) P Q от (4) и (9);
(36) P Q от (4) и (10);
Бяха генерирани много неуместни и излишни клаузи. Например (7), (8), (9) и (10) са тавтологии. Тъй като тавтологията винаги е вярна, тогава ако ниезачеркваме тавтологията от неудовлетворимия набор от клаузи, останалият набор все още трябва да е неудовлетворим. Следователно тавтологията е неуместна дизюнкция и не трябва да се генерира. Ако се генерира, тогава (с изключение на много малко случаи) трябва да се изтрие. Освен това, клаузи P, Q, P, Q се генерират многократно. Има и други повтарящи се клаузи, вижте (13) - (16), (20) - (23), (26) - (29) и (33) - (36). Всъщност,
за да получим доказателство за S, трябва да генерираме клаузи (5),
(12) и (39). За да намалите излишъка, помислете за стратегия за зачеркване.
Всяко ограничение е щастливо. А. Шопенхауер
§ 5. Стратегия за зачеркване
Клауза D се нарича подклауза на D * (или D абсорбира D * ), ако D е част от клаузата D *. Тук се извиква D*
superjunkt за D .
Пример. Нека D =P, D *=P Q. Ясно е, че D е подклауза на D * и D * е супер-клауза на D .
Стратегията за елиминиране зависи от това как се елиминират тавтологиите и супервръзките. Страйк аут стратегията ще бъде завършена, ако
използва се заедно с метода на насищане на ниво, както следва: първо клаузите (S 0 S 1 ... ) се изписват по ред; след това резолвентите се изчисляват чрез сравняване на всяка клауза D i (S 0 S 1 ... ) с клаузата D k, която идва след D i. Очевидно е, че същата клауза не се изписва отново. Приложете тази стратегия на изтриване към примера от § 4 и ще получим следния списък:
Имаме значително по-кратък списък.Следователно стратегията за зачеркване може да намали паметта, необходима за прилагане на метода за разрешаване.
Ясно е, че необходимите изчисления не намаляват, а се увеличават. За да използваме стратегията за елиминиране, трябва да можем да решим дали получената клауза е тавтология или дали една от клаузите е подчинена на друга.
Методът на разделяне, както вече беше посочено, прави възможно автоматизирането на доказателството на теоремите. Видяхме, че неограниченото приложение
резолюция може да породи много ненужни и ненужни клаузи заедно с полезни. Въпреки че е възможно да се използва стратегията на елиминатора, за да се отхвърлят някои от тези ненужни и безполезни клаузи, след като са били генерирани, времето вече е изгубено за генерирането им. Освен това, ако се генерират безполезни клаузи, тогава са необходими големи ресурси от компютърно време, за да се определи, че тези клаузи наистина са излишни и ненужни. Следователно, за да получим ефективни процедури за доказване на теореми, трябва да избягваме генерирането на голям брой безполезни клаузи. Съществуват различни подходи за намаляване на изчисленията, сред които: методът на семантична резолюция; линейна резолюция и други методи. Ще обмислим
Доброто е двойно добро, накратко. Балтисар Грасман
Идеята е по същество да се използват индекси за подреждане на знаците в клаузи от даден набор S от клаузи. С други думи, това включва въвеждане на индекси за всяко появяване на знак в S чрез някакво цяло число; могат да се индексират различни срещания на един и същ символ.След това само знаците с най-малък индекс във всяка от клаузите могат да бъдат изрязвани (изтривани). Буквите в резолвентите наследяват своите индекси от помещенията. Ако знак в резолвента може да наследи повече от един индекс, тогава той е настроен насъответстващ на най-ниския индекс.
Разгледайте следните две клаузи
Нека представим индексите, които ще напишем долу вляво на буквата:
Тъй като индекс 1 в 1 P е по-малък от индекс 2 в 2 Q, е позволено да се отреже 1 P. В 3 P 4 Q е позволено да се отреже 3 P , тъй като 3 4. По този начин, прилагайки разделителното правило към клаузи (1) и (2) върху 1 P и 3 P, получаваме следната клауза:
Буквата 2 Q и 4 Q е една и съща. Тъй като 2 4, тогава Q получава индекс 2, така че получаваме
Клаузата (4) е клаузата (1) и (2). Обърнете внимание, че ако знаците в клауза (2) са индексирани по различен начин, например по този начин:
тогава знакът в дизюнкта (2 * ), който е позволено да бъде отрязан, ще бъде 3 Q. Правилото за разделяне обаче не може да се прилага за 1 P и 3 Q. Следователно клаузи (1) и (2 * ) не съществуват. Под се разбира последователното получаване от даден набор от клаузи и новополучени клаузи.
Разгледайте набора S от клаузи, който беше разгледан в раздел 4: