Параллельный поиск вывода в логическом исчислении на основе системы алгебраического программирования
Описано програмні засоби паралельного пошуку логічного виводу у пропозиційному численні та подано результати експериментів з ними. Програмні засоби розроблено на базі системи алгебричного програмування АПС та кластерного комплексу СКІТ-1. Software for parallel inference search in propositional calcu...
Saved in:
| Published in: | Кибернетика и системный анализ |
|---|---|
| Date: | 2010 |
| Main Authors: | , , , |
| Format: | Article |
| Language: | Russian |
| Published: |
Інститут кібернетики ім. В.М. Глушкова НАН України
2010
|
| Subjects: | |
| Online Access: | https://nasplib.isofts.kiev.ua/handle/123456789/45253 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Journal Title: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Cite this: | Параллельный поиск вывода в логическом исчислении на основе системы алгебраического программирования / A.А. Летичевский, В.Н. Герман, М.К. Мороховец, Н.Н. Щеголева // Кибернетика и системный анализ. — 2010. — № 4. — С. 169-180. — Бібліогр.: 10 назв. — рос. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1860248925189963776 |
|---|---|
| author | Летичевский, А.А. Герман, В.Н. Мороховец, М.К. Щеголева, Н.Н. |
| author_facet | Летичевский, А.А. Герман, В.Н. Мороховец, М.К. Щеголева, Н.Н. |
| citation_txt | Параллельный поиск вывода в логическом исчислении на основе системы алгебраического программирования / A.А. Летичевский, В.Н. Герман, М.К. Мороховец, Н.Н. Щеголева // Кибернетика и системный анализ. — 2010. — № 4. — С. 169-180. — Бібліогр.: 10 назв. — рос. |
| collection | DSpace DC |
| container_title | Кибернетика и системный анализ |
| description | Описано програмні засоби паралельного пошуку логічного виводу у пропозиційному численні та подано результати експериментів з ними. Програмні засоби розроблено на базі системи алгебричного програмування АПС та кластерного комплексу СКІТ-1.
Software for parallel inference search in propositional calculus is described and used to obtain experimental results. The software is based on the Algebraic Programming System APS and the cluster complex SCIT-1.
|
| first_indexed | 2025-12-07T18:40:35Z |
| format | Article |
| fulltext |
ÓÄÊ 510.66:004.272.2
À.À. ËÅÒÈ×ÅÂÑÊÈÉ, Â.Í. ÃÅÐÌÀÍ, Ì.Ê. ÌÎÐÎÕÎÂÅÖ, Í.Í. ÙÅÃÎËÅÂÀ
ÏÀÐÀËËÅËÜÍÛÉ ÏÎÈÑÊ ÂÛÂÎÄÀ  ËÎÃÈ×ÅÑÊÎÌ ÈÑ×ÈÑËÅÍÈÈ
ÍÀ ÎÑÍÎÂÅ ÑÈÑÒÅÌÛ ÀËÃÅÁÐÀÈ×ÅÑÊÎÃÎ ÏÐÎÃÐÀÌÌÈÐÎÂÀÍÈß
Êëþ÷åâûå ñëîâà: ñèñòåìà àëãåáðàè÷åñêîãî ïðîãðàììèðîâàíèÿ, ïðàâèëà ïåðåïè-
ñûâàíèÿ, àëãîðèòì î÷åâèäíîñòè, ïîèñê ëîãè÷åñêîãî âûâîäà, ïàðàëëåëüíûå âû÷èñ-
ëåíèÿ, êëàñòåð.
ÂÂÅÄÅÍÈÅ
Ïîÿâëåíèå âñå áîëåå ìîùíûõ ñîâðåìåííûõ ýëåêòðîííûõ ñðåäñòâ âû÷èñëåíèé,
â ÷àñòíîñòè òàêèõ, êàê ïàðàëëåëüíûå âû÷èñëèòåëüíûå ìàøèíû, îêàçûâàåò âëèÿ-
íèå íà ðàçâèòèå ìàòåìàòè÷åñêîãî îáåñïå÷åíèÿ ðåøåíèÿ ðàçëè÷íûõ çàäà÷, â òîì
÷èñëå òåõ, êîòîðûå òðàäèöèîííî îòíîñÿòñÿ ê îáëàñòè èñêóññòâåííîãî èíòåëëåêòà.
Îäíèì èç íàïðàâëåíèé ýòîé îáëàñòè ÿâëÿåòñÿ àâòîìàòèçàöèÿ ïîèñêà äîêàçà-
òåëüñòâ òåîðåì (ÀÄÒ). Ïîñêîëüêó îíî âîçíèêëî ðàíüøå, ÷åì ïîÿâèëèñü ïàðàë-
ëåëüíûå ÝÂÌ, êî âðåìåíè âíåäðåíèÿ ñðåäñòâ ïàðàëëåëüíûõ âû÷èñëåíèé áûëè
ñîçäàíû ïðîãðàììíûå ñèñòåìû àâòîìàòèçèðîâàííîãî äîêàçàòåëüñòâà òåîðåì,
ôóíêöèîíèðîâàâøèå íà ïîñëåäîâàòåëüíûõ ÝÂÌ. Ïåðåä ðàçðàáîò÷èêàìè ÀÄÒ
âñòàëà çàäà÷à ñîçäàíèÿ òàêèõ ïðîãðàììíûõ ñèñòåì, êîòîðûå áû ýôôåêòèâíî ðà-
áîòàëè íà ïàðàëëåëüíûõ ìàøèíàõ.
 ðàìêàõ äâóõ áàçîâûõ ñòðàòåãèé ðàñïàðàëëåëèâàíèÿ ïîèñêà ðåøåíèÿ çàäà÷ —
È-ïàðàëëåëèçìà è ÈËÈ-ïàðàëëåëèçìà — èññëåäîâàòåëÿìè â îáëàñòè ÀÄÒ ðàññìàò-
ðèâàëèñü ðàçíûå ñõåìû ïàðàëëåëüíûõ âû÷èñëåíèé.  íàñòîÿùåå âðåìÿ ðàçëè÷àåòñÿ
ðàñïàðàëëåëèâàíèå âû÷èñëåíèé ïðè ïîèñêå äîêàçàòåëüñòâà òåîðåì íà óðîâíå: îáðà-
áîòêè òåðìîâ, îáðàáîòêè ïðåäëîæåíèé, îðãàíèçàöèè ïîèñêà â öåëîì. Îäíèì èç âè-
äîâ ðàñïàðàëëåëèâàíèÿ âû÷èñëåíèé íà óðîâíå îáðàáîòêè òåðìîâ ÿâëÿåòñÿ ïàðàë-
ëåëüíîå âûïîëíåíèå óíèôèêàöèè (íàïðèìåð, [1, 2]) îáðàáîòêè ïðåäëîæåíèé —
ïðèìåíåíèå îäíîâðåìåííî íåñêîëüêèõ ïðàâèë âûâîäà èñ÷èñëåíèÿ ïðè ïîèñêå ëîãè-
÷åñêîãî âûâîäà èëè îäíîãî ïðàâèëà âûâîäà ê íåñêîëüêèì ñîâîêóïíîñòÿì ôîð-
ìóë-ïîñûëîê (íàïðèìåð, [3]) îðãàíèçàöèè ïîèñêà — îäíîâðåìåííîå èñïîëüçîâàíèå
äëÿ ðåøåíèÿ îäíîé çàäà÷è íåñêîëüêèõ ñòðàòåãèé ïîèñêà äîêàçàòåëüñòâà òåîðåì
(îäèíàêîâûõ èëè ðàçëè÷íûõ) â ðåæèìå ñîòðóäíè÷åñòâà èëè ðåæèìå ñîïåðíè÷åñòâà
(íàïðèìåð, [4]). Îïûò ðàçðàáîòêè è èñïîëüçîâàíèÿ ïàðàëëåëüíûõ ñèñòåì ÀÄÒ ïîêà-
çàë, ÷òî íà äàííîì ýòàïå ðàçâèòèÿ âû÷èñëèòåëüíûõ ñðåäñòâ íàèáîëåå ïåðñïåêòèâ-
íûì ÿâëÿåòñÿ ðàñïàðàëëåëèâàíèå íà óðîâíå îðãàíèçàöèè ïîèñêà [5].
 íàñòîÿùåé ñòàòüå îïèñàíû ñðåäñòâà ïàðàëëåëüíîãî ïîèñêà äîêàçàòåëüñòâ òå-
îðåì, ðàçðàáîòàííûå íà áàçå ñèñòåìû àëãåáðàè÷åñêîãî ïðîãðàììèðîâàíèÿ (ÀÏÑ).
Îíè ñîçäàâàëèñü ñ ó÷åòîì îñîáåííîñòåé äîñòóïíîãî òåõíè÷åñêîãî îáåñïå÷åíèÿ ïà-
ðàëëåëüíûõ âû÷èñëåíèé — êëàñòåðíîãî êîìïëåêñà ÑÊÈÒ-1. Èññëåäîâàíèÿ èìåëè
öåëüþ, ñ îäíîé ñòîðîíû, ñîçäàòü ïàðàëëåëüíóþ âåðñèþ äîêàçûâàòåëÿ òåîðåì (äëÿ
ôîðìóë ëîãèêè âûñêàçûâàíèé), ðàçðàáîòàííîãî ðàíåå íà áàçå ÀÏÑ, ñ äðóãîé —
íàéòè êëàññ çàäà÷, ñõåìà ðåøåíèÿ êîòîðûõ ïóòåì ïàðàëëåëüíûõ âû÷èñëåíèé õîðî-
øî ñî÷åòàëàñü áû ñ àðõèòåêòóðîé âû÷èñëèòåëüíîãî êîìïëåêñà ÑÊÈÒ-1, è, êðîìå
òîãî, èçó÷èòü ýêñïåðèìåíòàëüíî çàâèñèìîñòü âðåìåíè ðåøåíèÿ çàäà÷ ðàññìàòðèâàå-
ìîãî êëàññà îò ÷èñëà èñïîëüçóåìûõ ïðîöåññîðîâ.  ðàáîòå àíàëèçèðóþòñÿ ðåçóëü-
òàòû ýêñïåðèìåíòîâ ñ ïðîãðàììîé ïàðàëëåëüíîãî ïîèñêà äîêàçàòåëüñòâ òåîðåì.
Äàëüíåéøåå èçëîæåíèå îðãàíèçîâàíî ñëåäóþùèì îáðàçîì. Ïðèâåäåíû êðàòêèå
ñâåäåíèÿ îá ÀÏÑ, îïèñàíî áàçîâîå èñ÷èñëåíèå, èñïîëüçîâàííîå äëÿ ïîñòðîåíèÿ
ñèñòåìû ÀÄÒ, äàíû êðàòêèå ñâåäåíèÿ î êëàñòåðíîì êîìïëåêñå ÑÊÈÒ-1, íà áàçå êî-
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4 169
� À.À. Ëåòè÷åâñêèé, Â.Í. Ãåðìàí, Ì.Ê. Ìîðîõîâåö, Í.Í. Ùåãîëåâà, 2010
òîðîãî ïðîâîäèëèñü ýêñïåðèìåíòû, ïðåäñòàâëåíî îáîñíîâàíèå âûáîðà êëàññà çàäà÷
äëÿ ïðîâåäåíèÿ ýêñïåðèìåíòîâ, îïèñàíà îðãàíèçàöèÿ ïàðàëëåëüíîãî äîêàçàòåëüñòâà
òåîðåì, ïðèâåäåíû ðåçóëüòàòû ýêñïåðèìåíòîâ è èõ àíàëèç.
ÑÈÑÒÅÌÀ ÀËÃÅÁÐÀÈ×ÅÑÊÎÃÎ ÏÐÎÃÐÀÌÌÈÐÎÂÀÍÈß
Ñèñòåìà àëãåáðàè÷åñêîãî ïðîãðàììèðîâàíèÿ [6] ñëóæèò ñðåäîé äëÿ ðàçðàáîòêè
ïðîòîòèïîâ ïðèêëàäíûõ ïðîãðàììíûõ ñèñòåì. Îíà íàèáîëåå ïðèñïîñîáëåíà äëÿ
ïðåäìåòíûõ îáëàñòåé, ïðåäñòàâëåííûõ àëãåáðî-ëîãè÷åñêèìè ìîäåëÿìè. Òåõíèêà
ïðîãðàììèðîâàíèÿ â ÀÏÑ áàçèðóåòñÿ íà ïåðåïèñûâàíèè òåðìîâ.  îòëè÷èå îò
òðàäèöèîííîãî ïîäõîäà, îðèåíòèðîâàííîãî íà èñïîëüçîâàíèå êàíîíè÷åñêèõ ñèñ-
òåì ïðàâèë ïåðåïèñûâàíèÿ ñ «î÷åâèäíîé» ñòðàòåãèåé èõ ïðèìåíåíèÿ, â ÀÏÑ
âîçìîæíî ñî÷åòàíèå ëþáûõ ñèñòåì ïðàâèë ïåðåïèñûâàíèÿ è ðàçíîîáðàçíûõ
ñòðàòåãèé ïåðåïèñûâàíèÿ. Òàêîé ïîäõîä çíà÷èòåëüíî ðàñøèðÿåò âîçìîæíîñòè
òåõíèê ïåðåïèñûâàíèÿ, ïîñêîëüêó âîçðàñòàåò èõ ãèáêîñòü è âûðàçèòåëüíîñòü.
 ñòðóêòóðå ÀÏÑ ìîæíî âûäåëèòü òðè ñïîñîáà ñòðóêòóðèçàöèè èñïîëüçóåìûõ
îáúåêòîâ:
� îñíîâíûå òèïû ñèñòåìíûõ îáúåêòîâ;
� áàçîâûå âû÷èñëèòåëüíûå ìåõàíèçìû;
� äîïóñòèìûå ÿçûêîâûå êîíñòðóêöèè, îáúåäèíåííûå â ñåìåéñòâî ÿçûêîâ
ÀÏËÀÍ.
Îñíîâíûì òèïîì äàííûõ â ñèñòåìå ÿâëÿåòñÿ òåðì (ïðåäñòàâëåííûé â âèäå äå-
ðåâà) â àëãåáðå T Z� ( ) , ïîðîæäåííîé ìíîæåñòâîì ïåðâè÷íûõ îáúåêòîâ Z è îïåðàöè-
ÿìè ñèãíàòóðû �. Ýòà àëãåáðà ðàññìàòðèâàåòñÿ êàê àáñîëþòíî ñâîáîäíàÿ. Â ñèñòå-
ìå òðè îñíîâíûõ òèïà îáúåêòîâ: àëãåáðàè÷åñêèå ïðîãðàììû (àï-ìîäóëè), àëãåáðàè-
÷åñêèå ìîäóëè (à-ìîäóëè) è èíòåðïðåòàòîðû. Àëãåáðàè÷åñêèå ïðîãðàììû — ýòî
òåêñòû â ÿçûêå ÀÏËÀÍ. Êàæäàÿ ïðîãðàììà ñîäåðæèò îïèñàíèå ñèãíàòóðû � ñ ñèí-
òàêñèñîì äëÿ ïîñòðîåíèÿ àëãåáðàè÷åñêèõ âûðàæåíèé.  íåé îïðåäåëÿþòñÿ ìíîæåñ-
òâà èìåí X è àòîìîâ A. Àëãåáðàè÷åñêàÿ ïðîãðàììà îïðåäåëÿåò òàêæå íà÷àëüíûå
çíà÷åíèÿ èìåí.
Àëãåáðàè÷åñêèå ìîäóëè ñîäåðæàò âíóòðåííèå ïðåäñòàâëåíèÿ ñòðóêòóð äàííûõ,
îïðåäåëåííûõ â àï-ìîäóëÿõ. Ïîíÿòèå àëãåáðàè÷åñêîãî ìîäóëÿ èìååò äèíàìè÷åñêèé
õàðàêòåð: ìîäóëü íàõîäèòñÿ â ñîñòîÿíèè, êîòîðîå ñî âðåìåíåì ìîæåò ìåíÿòüñÿ; èç-
ìåíåíèå ñîñòîÿíèÿ à-ìîäóëÿ ïðîèñõîäèò â òîì ñëó÷àå, êîãäà ïðè èíòåðïðåòàöèè
âûïîëíÿåòñÿ êàêàÿ-ëèáî åãî ïðîöåäóðà.
Èíòåðïðåòàòîðû èñïîëüçóþòñÿ äëÿ èíòåðïðåòàöèè ïðîöåäóðíîãî ïîäìíîæåñòâà
ÿçûêà ÀÏËÀÍ.
Òåõíèêà ïðîãðàììèðîâàíèÿ â ÀÏÑ áàçèðóåòñÿ íà ïåðåïèñûâàíèè òåðìîâ.
 ÀÏÑ ðåàëèçîâàíî íåñêîëüêî ñòðàòåãèé ïåðåïèñûâàíèÿ, êðîìå òîãî, àðñåíàë
ñòðàòåãèé ìîæíî ïîïîëíÿòü.
Ñèñòåìà àëãåáðàè÷åñêîãî ïðîãðàììèðîâàíèÿ îðãàíèçîâàíà òàêèì îáðàçîì, ÷òî
ïîëüçîâàòåëü èìååò îäíîâðåìåííûé äîñòóï êî âñåì óðîâíÿì ïðîãðàììèðîâàíèÿ,
íà÷èíàÿ ñ ÿçûêà êîíêðåòíîé ïðåäìåòíîé îáëàñòè è çàêàí÷èâàÿ óðîâíåì ðàñøèðå-
íèÿ ÿçûêà ñè, êîòîðîå íàçûâàåòñÿ L2C. Òàêèì ïóòåì äîñòèãàåòñÿ ýôôåêòèâíîå ðàñ-
ïðåäåëåíèå ñëîæíîñòè ðàçðàáàòûâàåìîé ïðîãðàììíîé ñèñòåìû ïî ðàçëè÷íûì óðîâ-
íÿì. Ïîääåðæèâàåòñÿ ýâîëþöèîííîñòü ïðîöåññà ïðîãðàììèðîâàíèÿ, íà÷èíàÿ ñ âû-
ïîëíÿåìîé àëãåáðàè÷åñêîé ñïåöèôèêàöèè ÷åðåç îïòèìèçèðóþùèå ïðåîáðàçîâàíèÿ
äî ýôôåêòèâíîé ïðîãðàììû íà ÿçûêå ñè. Ñàìûé âåðõíèé è ñïåöèàëèçèðîâàííûé
óðîâåíü îáðàçóþò êîíñòðóêöèè, ñâÿçàííûå ñ íåêîòîðîé êîíêðåòíîé ïðåäìåòíîé îá-
ëàñòüþ. Îíè èìåþò ëîêàëüíûé õàðàêòåð, íî òàêæå àêòèâíî èñïîëüçóþòñÿ â äðóãèõ
ïðåäìåòíûõ îáëàñòÿõ. Ýòî ñâÿçàíî ñ òåì, ÷òî â áàçîâîì ÀÏËÀÍå íåò òèïîâ äàí-
íûõ. Ñòðîãî ãîâîðÿ, ñóùåñòâóåò åäèíñòâåííûé òèï äàííûõ — àëãåáðàè÷åñêèé òåðì.
 òî æå âðåìÿ èìåþòñÿ âîçìîæíîñòè äëÿ èñïîëüçîâàíèÿ ñòðîãîãî òèïèçèðîâàíèÿ,
íàïðèìåð ïðè ïðîãðàììèðîâàíèè â îáúåêòíî-îðèåíòèðîâàííîì ðàñøèðåíèè
ÀÏËÀÍà.
170 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4
 êà÷åñòâå ïðèìåðà èñïîëüçîâàíèÿ òåõíèêè ïåðåïèñûâàíèÿ äëÿ ðåøåíèÿ çàäà÷,
à òàêæå ÿçûêîâûõ êîíñòðóêöèé ÿçûêà ÀÏËÀÍ ðàññìîòðèì ïðîñòóþ çàäà÷ó ôóíêöè-
îíàëüíîãî ïðîãðàììèðîâàíèÿ — âû÷èñëåíèå ÷èñåë Ôèáîíà÷÷è. Èçâåñòíîå ðåêóð-
ñèâíîå îïðåäåëåíèå n-ãî ÷èñëà Ôèáîíà÷÷è çàäàåòñÿ ñëåäóþùåé ñèñòåìîé
ñîîòíîøåíèé:
F ( )0 1� , F ( )1 1� , F n F n F n( ) ( ) ( )� � � �1 2 .
Äàííóþ ñèñòåìó ìîæíî ðàññìàòðèâàòü êàê (ðåêóðñèâíîå) îïðåäåëåíèå ôóíê-
öèè F èëè ñèñòåìó ïðàâèë ïåðåïèñûâàíèÿ, êîòîðóþ ìîæíî èñïîëüçîâàòü äëÿ âû-
÷èñëåíèÿ F n( ). ×òîáû çàïèñàòü åå íà ÿçûêå ÀÏËÀÍ, ñëåäóåò èìïîðòèðîâàòü ìî-
äóëü std.ap:
INCLUDE <std.ap>.
Ýòà êîìàíäà äàåò âîçìîæíîñòü âêëþ÷èòü íåêîòîðûå ñòàíäàðòíûå îïðåäåëåíèÿ,
â ÷àñòíîñòè, îáåñïå÷èâàåò èñïîëüçîâàíèå àðèôìåòè÷åñêèõ îïåðàöèé «�», «�», îò-
íîøåíèÿ «�», à òàêæå íåêîòîðûõ äðóãèõ ñèíòàêñè÷åñêèõ ïîíÿòèé, îïðåäåëåííûõ
â ìîäóëå std.ap. Çàòåì ñëåäóåò îïðåäåëèòü èìÿ ñèñòåìû (ñ ïîìîùüþ ïðåäëîæå-
íèÿ NAME R;) è ïðèñâîèòü íà÷àëüíûå çíà÷åíèÿ:
R:=rs(n)(
F(0) = 1,
F(1) = 1,
F(n) = F(n – 1) + F(n – 2)
);
Ïåðâàÿ ñòðîêà ïðèñâàèâàíèÿ óêàçûâàåò, ÷òî çíà÷åíèåì èìåíè R ÿâëÿåòñÿ ñèñ-
òåìà ïðàâèë ïåðåïèñûâàíèÿ (rs), à n — åäèíñòâåííàÿ ïåðåìåííàÿ, èñïîëüçóåìàÿ
ñèñòåìîé.
Ñèñòåìó R ìîæíî ïðèìåíèòü, íàïðèìåð, ê âûðàæåíèþ T F� ( )10 è ïðåîáðàçî-
âàòü åãî òàêèì îáðàçîì:
F F F F F( ) ( ) ( ) ( ) ( )10 10 1 10 2 9 8� � � � � � .
 ÀÏÑ äàííîå ïðåîáðàçîâàíèå âûïîëíÿåòñÿ çà îäèí øàã, òàê êàê àðèôìåòè÷åñ-
êèå îïåðàöèè ÿâëÿþòñÿ èíòåðïðåòèðóåìûìè è âûïîëíÿþòñÿ ïî ìåðå âîçìîæíîñòè
íà êàæäîì øàãå ïåðåïèñûâàíèÿ. Ñëåäóþùèé øàã ïåðåïèñûâàíèÿ ìîæåò áûòü âû-
ïîëíåí îäíèì èç äâóõ ñïîñîáîâ, â çàâèñèìîñòè îò òîãî, ê êîòîðîìó èç âõîæäåíèé
âûðàæåíèÿ F n( ) ïðèìåíÿåòñÿ òðåòüå ïðàâèëî ñèñòåìû. Ðàññìîòðèì ñëó÷àé, êîãäà
âûáèðàåòñÿ ïåðâîå âõîæäåíèå, ò.å. F ( )9 . Òîãäà èìååì íîâîå âûðàæåíèå
T F F F� � �( ( ) ( )) ( )8 7 8 .
Ïðîäîëæàÿ ïîäîáíûì îáðàçîì, ò.å. âûáèðàÿ âñÿêèé ðàç ñàìîå ëåâîå (ñàìîå
âíóòðåííåå) âõîæäåíèå, ïîëó÷àåì
T F F F F� � � � �(( ( ) ( )) ( )) ( )7 6 7 8
� � � � � �((( ( ) ( )) ( )) ( )) ( )F F F F F6 5 6 7 8
.................................................................
� � � � �( (( ( ) ( )) ( )) ) ( )� �F F F F1 0 1 8 .
Òåïåðü ïðèìåíèìû êàê òðåòüå, òàê è âòîðîå ïðàâèëà. Áóäåì äåéñòâîâàòü ïî
ïðèíöèïó, êîòîðûé èñïîëüçóåòñÿ âî âñåõ îñíîâíûõ ñòðàòåãèÿõ ïåðåïèñûâàíèÿ â
ÀÏÑ. Îí ñîñòîèò â òîì, ÷òî ïðàâèëî, êîòîðîå ôàêòè÷åñêè ïðèìåíÿåòñÿ, ÿâëÿåòñÿ
ïåðâûì èç ïðàâèë, èñïîëüçóåìûõ íà òåêóùåì ýòàïå âû÷èñëåíèé. Òàêèì îáðàçîì,
ïîñëåäóþùèå äâà øàãà ïðåîáðàçîâàíèé ïðèâåäóò ê âûðàæåíèÿì
T F F F F F� � � � � � � � � �( (( ( )) ( )) ) ( ) ( (( ) ( )) ) ( )� � � �1 0 1 8 1 1 1 8 .
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4 171
 ñîîòâåòñòâèè ñ ëåâîñòîðîííåé ñòðàòåãèåé â ïåðâóþ î÷åðåäü ñëåäóåò âûïîë-
íèòü ñëîæåíèå. Â ðåçóëüòàòå ïîñëåäîâàòåëüíîñòè ïåðåïèñûâàíèé ñîãëàñíî ëåâîñòî-
ðîííåé ñòðàòåãèè ïîëó÷èì
T � � �55 34 89.
Äëÿ äàííîé ñèñòåìû òîò ôàêò, ÷òî ïðè ïåðåïèñûâàíèè âûáèðàåòñÿ ëèøü ñàìîå
ëåâîå âõîæäåíèå, íå ñóùåñòâåí. ×òîáû ïîëó÷èòü òðåáóåìûé ðåçóëüòàò ñ ïîìîùüþ
ñèñòåìû ïðàâèë R, äîñòàòî÷íî èñïîëüçîâàòü ëþáóþ ñòðàòåãèþ ïåðåïèñûâàíèÿ (àë-
ãîðèòì ïåðåïèñûâàíèÿ), óäîâëåòâîðÿþùóþ ñëåäóþùèì óñëîâèÿì.
1. Íà êàæäîì øàãå ïåðåïèñûâàíèÿ ïðèìåíÿåòñÿ îäíî èç ïðàâèë ñèñòåìû ëèáî
âûïîëíÿåòñÿ àðèôìåòè÷åñêàÿ îïåðàöèÿ.
2. Âûáîð ïðàâèëà îñóùåñòâëÿåòñÿ ñîãëàñíî ïîñëåäîâàòåëüíîñòè, â êîòîðîé çà-
ïèñàíû ïðàâèëà.
3. Ïåðåïèñûâàíèå ïðîäîëæàåòñÿ äî òåõ ïîð, ïîêà ýòî âîçìîæíî, ò.å. ïîêà ñó-
ùåñòâóþò âõîæäåíèÿ, ê êîòîðûì ïðèìåíèìû ïðàâèëà ñèñòåìû, ëèáî âîçìîæíû âû-
ïîëíåíèÿ àðèôìåòè÷åñêèõ îïåðàöèé íàä ÷èñëàìè.
Ñòðàòåãèÿ, óäîâëåòâîðÿþùàÿ ïðèâåäåííûì óñëîâèÿì, íàçûâàåòñÿ ôèíàëüíîé.
ÀÏÑ ïîçâîëÿåò èñïîëüçîâàòü âñòðîåííûå ñòðàòåãèè ïåðåïèñûâàíèÿ, à òàêæå ïèñàòü
ñîáñòâåííûå ñòðàòåãèè, êîòîðûå íàèáîëåå ïîäõîäÿò äëÿ ðåøàåìîé çàäà÷è. Âûçîâ
âñòðîåííîé ñòðàòåãèè ÿâëÿåòñÿ âûçîâîì âíóòðåííåé ïðîöåäóðû. Êàê ïðàâèëî, îí
èìååò âèä s T R( , ), ãäå s — èìÿ ñòðàòåãèè, T — èìÿ àëãåáðàè÷åñêîé ñòðóêòóðû äàí-
íûõ, ê êîòîðîé ïðèìåíÿåòñÿ ñèñòåìà, R — èìÿ ñèñòåìû ïðàâèë ïåðåïèñûâàíèÿ.
 ðàìêàõ ñèñòåìû ÀÏÑ ðàçðàáîòàí öåëûé ðÿä ïðèêëàäíûõ ïðîãðàìì: ñðåäñòâà
îáðàáîòêè ôîðìóë ëîãèêè âûñêàçûâàíèé (ïðèâåäåíèå ïðîïîçèöèîíàëüíûõ ôîðìóë
ê ÊÍÔ, ÄÍÔ, ïðîâåðêà òîæäåñòâåííîé èñòèííîñòè ôîðìóëû), ïðèâåäåíèå ïîëèíî-
ìîâ, ðåøàòåëü çàäà÷ îáùåãî íàçíà÷åíèÿ.
Ïåðâîíà÷àëüíî ÀÏÑ ðàçðàáàòûâàëàñü â ñðåäå MS DOS.  íàñòîÿùåå âðåìÿ ñó-
ùåñòâóþò âåðñèè ÀÏÑ, ïðåäíàçíà÷åííûå äëÿ ðàáîòû ïîä óïðàâëåíèåì ðàçëè÷íûõ
ñîâðåìåííûõ îïåðàöèîííûõ ñèñòåì — êàê Linux, Solaris, òàê è Windows.
ËÎÃÈ×ÅÑÊÎÅ ÈÑ×ÈÑËÅÍÈÅ
Ñðåäñòâà ïîèñêà äîêàçàòåëüñòâ òåîðåì â ÀÏÑ îñíîâàíû íà èñ÷èñëåíèè àëãîðèò-
ìà î÷åâèäíîñòè [7].  îñíîâó èñ÷èñëåíèÿ ïîëîæåíà èäåÿ Â.Ì. Ãëóøêîâà îá àë-
ãîðèòìå î÷åâèäíîñòè [8] êàê ôîðìàëèçàöèè ðàññóæäåíèé ïðàêòè÷åñêîãî ìàòåìà-
òèêà. Ïðè ðåàëèçàöèè ýòîãî èñ÷èñëåíèÿ èñïîëüçîâàíî ïðåäñòàâëåíèå, ïðåäëî-
æåííîå â [9]. Ýëåìåíòàðíûìè îáúåêòàìè èñ÷èñëåíèÿ ÿâëÿþòñÿ ïðîïîçèöèîíàëüíûå
ôîðìóëû è ïðîñòûå ñåêâåíöèè. Ïðîïîçèöèîíàëüíûå ôîðìóëû ðàññìàòðèâàþòñÿ
ñ òî÷íîñòüþ äî ýêâèâàëåíòíîñòè, êîòîðàÿ îïðåäåëÿåòñÿ ñ ïîìîùüþ âñåõ ñîîòíî-
øåíèé áóëåâîé àëãåáðû çà èñêëþ÷åíèåì äèñòðèáóòèâíîñòè (ïîñêîëüêó ïîñëåäíÿÿ
ÿâëÿåòñÿ èñòî÷íèêîì ýêñïîíåíöèàëüíîé ñëîæíîñòè).  ñèñòåìå ÀÏÑ ñóùåñòâóåò
ôóíêöèÿ Can, êîòîðàÿ èñïîëüçóåòñÿ äëÿ ïðèâåäåíèÿ ëîãè÷åñêèõ ôîðìóë ê íîð-
ìàëüíîé (íî íå êàíîíè÷åñêîé) ôîðìå, ÷òî ñîõðàíÿåò ýòó ýêâèâàëåíòíîñòü.
Àññîöèàòèâíîñòü, êîììóòàòèâíîñòü è èäåìïîòåíòíîñòü êîíúþíêöèè è äèçúþí-
êöèè, à òàêæå çàêîíû ïðîòèâîðå÷èÿ, èñêëþ÷åííîãî òðåòüåãî è çàêîíû äëÿ ïðîïî-
çèöèîíàëüíûõ êîíñòàíò ïðèìåíÿþòñÿ íåÿâíûì îáðàçîì, áóäó÷è âñòðîåííûìè
â ñòðàòåãèþ Can_ord. Äëÿ ïîñòðîåíèÿ ïðîñòûõ ñåêâåíöèé èñïîëüçóåòñÿ ñèíòàê-
ñèñ x y� , ãäå x è y — ïðîïîçèöèîíàëüíûå ôîðìóëû.
Èñ÷èñëåíèå àëãîðèòìà î÷åâèäíîñòè çàäàåòñÿ â âèäå êîìáèíàöèè äâóõ èñ÷èñëå-
íèé. Îäíèì èç íèõ ÿâëÿåòñÿ èñ÷èñëåíèå âñïîìîãàòåëüíûõ öåëåé (ÈÂÖ), äðóãèì —
èñ÷èñëåíèå óñëîâíûõ ñåêâåíöèé (ÈÓÑ). Âûâîä â èñ÷èñëåíèè âñïîìîãàòåëüíûõ öå-
ëåé èìååò ôèíèòíûé õàðàêòåð, îí âñåãäà çàâåðøàåòñÿ è èñïîëüçóåòñÿ êàê îäèí øàã
â èñ÷èñëåíèè óñëîâíûõ ñåêâåíöèé, êîòîðîå ÿâëÿåòñÿ îñíîâíûì. Çàìåòèì, ÷òî â íå-
êîòîðîì ñìûñëå èñ÷èñëåíèå àëãîðèòìà î÷åâèäíîñòè îáîáùàåò ïîèñê âûâîäà â ëî-
ãè÷åñêîì ïðîãðàììèðîâàíèè, êîòîðûé ìîæíî ðàññìàòðèâàòü êàê ïîèñê âàðèàíòîâ
ñâåäåíèÿ çàäà÷è ê ïîäçàäà÷àì (âñïîìîãàòåëüíûì öåëÿì). Îòëè÷èå ñîñòîèò ëèøü
â òîì, ÷òî âñïîìîãàòåëüíûå öåëè â ëîãè÷åñêîì ïðîãðàììèðîâàíèè èçâëåêàþòñÿ èç
172 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4
õîðíîâñêèõ äèçúþíêòîâ, à â èñ÷èñëåíèè àëãîðèòìà î÷åâèäíîñòè îíè ìîãóò èçâëå-
êàòüñÿ èç ïðîèçâîëüíûõ ôîðìóë.
Èñ÷èñëåíèå óñëîâíûõ ñåêâåíöèé. Óñëîâíàÿ ñåêâåíöèÿ — âûðàæåíèå âèäà
( , )w Q , ãäå w — êîíúþíêöèÿ ëèòåðàëîâ (äëÿ ïðîïîçèöèîíàëüíîãî èñ÷èñëåíèÿ ëèòå-
ðàë — ïðîïîçèöèîíàëüíàÿ ïåðåìåííàÿ ëèáî åå îòðèöàíèå), Q — êîíúþíêöèÿ ïðî-
ñòûõ ñåêâåíöèé.
Àêñèîìû èñ÷èñëåíèÿ:
( , ); ( , ); ( , ); ( , )w w u w P Q1 1 0 0� � .
Çäåñü P — êîíúþíêöèÿ ïðîñòûõ ñåêâåíöèé, åäèíèöà îçíà÷àåò ïóñòóþ êîíúþíêöèþ.
Ïðàâèëà âûâîäà:
(ÈÓÑ.1) ( , ) | ( , )w u w u� � � 0 1 ,
(ÈÓÑ.2) ( , ) | ( , ( ) ( ))w u x y w u x u y�
� �
� ,
(ÈÓÑ.3) ( , ) | ( , )w u x y w x u y� � �
� ,
(ÈÓÑ.4) ( , ) | ( , )w x y z w x y z
� �
� , ãäå x — ëèòåðàë,
(ÈÓÑ.5)
( , ) | ( , )
( , ) | ( , )
w F w F
w F H w H
� � �
�
, ãäå ( , )w F� � — àêñèîìà,
(ÈÓÑ.6)
aux aux( , , ) | ( , , )
( , ) | ( , )
1 1w u z v z y z P
w u z w z P
� �
�
� �
,
ãäå z — ëèòåðàë, P — êîíúþíêöèÿ ïðîñòûõ ñåêâåíöèé (ïðàâèëî âñïîìîãàòåëü-
íîé öåëè).
Èñ÷èñëåíèå âñïîìîãàòåëüíûõ öåëåé. Âñïîìîãàòåëüíîé öåëüþ íàçîâåì
âûðàæåíèå âèäà aux ( , , )v u z P� , ãäå z — ëèòåðàë, u v, — ïðîïîçèöèîíàëüíûå
ôîðìóëû, P — êîíúþíêöèÿ ïðîñòûõ ñåêâåíöèé (ïóñòàÿ êîíúþíêöèÿ ðàâíà 1).
Ïðàâèëà èñ÷èñëåíèÿ âñïîìîãàòåëüíûõ öåëåé:
(ÈÂÖ.1) aux aux( , , ) | ( , , )v x y z P v y x z P
� �
� ,
(ÈÂÖ.2) aux aux( , , ) | ( , , ( ) )v x y z P v x z v y P� � � � �
.
 ýòèõ ïðàâèëàõ êîíúþíêöèè è äèçúþíêöèè ðàññìàòðèâàþòñÿ ñ òî÷íîñòüþ äî
êîììóòàòèâíîñòè, ïîýòîìó íåò íåîáõîäèìîñòè ðàññìàòðèâàòü àëüòåðíàòèâíûå ïðà-
âèëà, êîòîðûå îáðàçóþòñÿ ïóòåì ïåðåñòàíîâîê x è y.
Ñâîéñòâî çàâåðøèìîñòè èñ÷èñëåíèÿ âñïîìîãàòåëüíûõ öåëåé ñëåäóåò èç óòâåð-
æäåíèÿ aux aux( , , ) | ( , , )v u z P v u z P� � � � � � , ãäå u� — ëèòåðàë.
Îñíîâíûì ñâîéñòâîì èñ÷èñëåíèÿ àëãîðèòìà î÷åâèäíîñòè ÿâëÿåòñÿ ñëåäóþùåå:
P — òàâòîëîãèÿ òîãäà è òîëüêî òîãäà, êîãäà ( , ) |1 1� �P Q, ãäå Q — àêñèîìà.
Ïðèìåð ïîñòðîåíèÿ âûâîäà â èñ÷èñëåíèè àëãîðèòìà î÷åâèäíîñòè. Ïóñòü
òðåáóåòñÿ äîêàçàòü, ÷òî â èñ÷èñëåíèè àëãîðèòìà î÷åâèäíîñòè âûâîäèìà ôîðìóëà
( ) ( )a a a a a a a2 1 2 1 1 1 1
�
�
� . (1)
Ñîãëàñíî îñíîâíîìó ñâîéñòâó ýòîãî èñ÷èñëåíèÿ äîñòàòî÷íî ïîêàçàòü, ÷òî
( , (1 1 2� a
�
�
� �a a a a a a Q1 2 1 1 1 1) ( )) | , ãäå Q — àêñèîìà. Çàïèøåì âû-
âîä, óêàçûâàÿ â ñêîáêàõ ñïðàâà îò ôîðìóëû íàçâàíèå ïðàâèëà, êîòîðîå ïðèìåíÿåòñÿ
äëÿ åå âûâîäà. Ïðè âûâîäå ó÷èòûâàåòñÿ, ÷òî ïðîïîçèöèîíàëüíûå ôîðìóëû ðàñ-
ñìàòðèâàþòñÿ ñ òî÷íîñòüþ äî íåêîòîðîé ýêâèâàëåíòíîñòè. Èòàê, èìååì
( , ( ) ( ))11 2 1 2 1 1 1 1�
�
�
� a a a a a a a (èñõîäíàÿ óñëîâíàÿ ñåêâåíöèÿ)
( , ( ( )) ( ( )))1 1 2 1 2 1 1 1 1 1�
�
�
� � a a a a a a a (ÈÓÑ.2)
Äàëåå ïðèìåíèìî ÈÓÑ.5, ò.å. åñëè áóäåò äîêàçàíî, ÷òî ( , (11 2�
a
�
� � � �a a a a w F1 2 1 1)) | ( , ) , ãäå ( , )w F� � — àêñèîìà, òî îñòàíåòñÿ ïðîâåðèòü
âûâîäèìîñòü óñëîâíîé ñåêâåíöèè
( , ( ))11 1 1� � a a (2)
( , ( ))11 2 1 2 1 1�
�
� a a a a a (ÈÓÑ.5, íà÷àëî)
( , ( ) )1 2 1 2 1 1
�
� a a a a a (ïðè x a a�
2 1, y a a a�
� 2 1 1 ÈÓÑ.3)
( , )1 2 1 2 1 1 � �
� a a a a a (çàìåíà
( )a a2 1 íà � a a2 1)
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4 173
( , ( ) ( ) )1 2 1 2 1 1 �
� � a a a a a (ÈÓÑ.3)
aux ( , ( ) ( ) , )1 2 1 2 1 11 �
� � a a a a a (ÈÓÑ.6, íà÷àëî)
aux (( ), , ) � � � a a a a a2 1 2 1 11 (ÈÂÖ.1)
aux (( ), , ) � � � � a a a a a a a2 1 1 1 2 1 2 (ÈÂÖ.2)
( , )a a a a1 2 1 2 � � (ÈÓÑ.6, êîíåö)
aux ( , ( ) , )1 1 2 1 21a a a a
� � (ÈÓÑ.6, íà÷àëî)
aux ( , , )a a a a1 2 1 21 � � (ÈÂÖ.1)
aux ( , , )a a a a a1 2 2 1 1 � � (ÈÂÖ.2)
( , )a a a a1 2 1 1
� (ÈÓÑ.6, êîíåö)
aux ( , , )1 1 2 1 11a a a a
� (ÈÓÑ.6, íà÷àëî)
aux ( , , )1 1 2 11a a a
� (çàìåíà a a a1 2 1
íà a a1 2
)
aux ( , , )a a a2 1 11� (ÈÂÖ.1)
( , )a a a1 2 11
(ÈÓÑ.6, êîíåö; àêñèîìà)
Ïîñëåäíÿÿ ñåêâåíöèÿ ÿâëÿåòñÿ àêñèîìîé. Îñòàëîñü ïðîâåðèòü âûâîäèìîñòü
óñëîâíîé ñåêâåíöèè ( , ( ))11 1 1� � a a . Èìååì:
( , ( ( )))1 1 1 1� � a a (óñëîâíàÿ ñåêâåíöèÿ (2))
( , )1 1 1a a� (ÈÓÑ.3)
aux ( , , )1 1 11a a� (ÈÓÑ.6, íà÷àëî)
( , ) a11 (ÈÓÑ.6, êîíåö; ÈÓÑ.5, êîíåö; àêñèîìà)
Òàêèì îáðàçîì, âûâîä ôîðìóëû (1) ïîñòðîåí.
ÒÅÕÍÈ×ÅÑÊÈÅ ÑÐÅÄÑÒÂÀ È ÎÏÅÐÀÖÈÎÍÍÀß ÑÐÅÄÀ ÏÐÎÃÐÀÌÌÛ
ÏÀÐÀËËÅËÜÍÎÃÎ ÏÎÈÑÊÀ ËÎÃÈ×ÅÑÊÎÃÎ ÂÛÂÎÄÀ
Áàçîé äëÿ ýêñïåðèìåíòîâ ñ ïðîãðàììîé ïîèñêà äîêàçàòåëüñòâ ïîñëóæèëà ìóëü-
òèïðîöåññîðíàÿ ñóïåðêîìïüþòåðíàÿ ñèñòåìà êëàñòåðíîãî òèïà ÑÊÈÒ (ñóïåðêîì-
ïüþòåð äëÿ èíôîðìàöèîííûõ òåõíîëîãèé) [10], ðàçðàáîòàííàÿ â Èíñòèòóòå êè-
áåðíåòèêè èìåíè Â.Ì. Ãëóøêîâà ÍÀÍÓ äëÿ ðåøåíèÿ çàäà÷, òðåáóþùèõ âû÷èñ-
ëåíèé áîëüøîãî îáúåìà è îáðàáîòêè ìàññèâîâ äàííûõ áîëüøèõ ðàçìåðîâ.
Êëàñòåðíàÿ âû÷èñëèòåëüíàÿ ñèñòåìà ïðåäñòàâëÿåò ñîáîé íàáîð ñòàíäàðòíûõ
ðàñïðåäåëåííûõ ïðîãðàììíî-àïïàðàòíûõ êîìïîíåíòîâ, îáúåäèíåííûõ äëÿ ðåøå-
íèÿ îáùèõ çàäà÷.  êëàñòåðå â êà÷åñòâå ïðîöåññîðíûõ ýëåìåíòîâ èñïîëüçóþòñÿ
ñòàíäàðòíûå êîìïüþòåðû, à äëÿ êîììóíèêàöèè — ñòàíäàðòíûå èíòåðôåéñû äëÿ
ñåòåé. Âû÷èñëèòåëüíàÿ ìîùíîñòü êëàñòåðíîé ñèñòåìû îïðåäåëÿåòñÿ áûñòðî-
äåéñòâèåì âû÷èñëèòåëüíûõ óçëîâ è ìåæóçëîâûõ êîììóíèêàöèé.
Ñèñòåìà ÑÊÈÒ îáåñïå÷èâàåò íàäåæíîå ôóíêöèîíèðîâàíèå àïïàðàòíî-ïðîãðàì-
ìíûõ ñðåäñòâ ðàçðàáîòêè èíòåëëåêòóàëüíûõ èíôîðìàöèîííûõ òåõíîëîãèé è ïðèêëàä-
íîãî ïðîãðàììíîãî îáåñïå÷åíèÿ è ïðåäíàçíà÷åíà äëÿ âûïîëíåíèÿ ñëîæíûõ çàäàíèé
â îáëàñòè ýêîíîìèêè, íàóêè, áåçîïàñíîñòè, îáîðîíû è äðóãèõ ñôåðàõ íàðîäíîãî õîçÿé-
ñòâà. Ôóíêöèîíàëüíûå êîìïîíåíòû ñóùåñòâóþùåãî âû÷èñëèòåëüíîãî êîìïëåêñà ïðåä-
íàçíà÷åíû äëÿ êðóãëîñóòî÷íîãî íåïðåðûâíîãî óäàëåííîãî óïðàâëåíèÿ ïîòîêîì çàäà-
íèé êàê â ðàìêàõ ëîêàëüíîé âû÷èñëèòåëüíîé ñåòè, òàê è ÷åðåç Èíòåðíåò.
Âû÷èñëèòåëüíûé êîìïëåêñ ñîñòîèò èç äâóõ êëàñòåðíûõ ñóïåðêîìïüþòåðîâ:
ÑÊÈÒ-1 è ÑÊÈÒ-2.
Ýêñïåðèìåíòû ïðîâîäèëèñü íà ñóïåðêîìïüþòåðíîé ñèñòåìå ÑÊÈÒ-1,
ÿâëÿþùåéñÿ 32-ïðîöåññîðíûì 16-óçëîâûì êëàñòåðîì íà ìèêðîïðîöåññîðàõ Intel
Xeon 2,67 ÃÃö (èìååò ðàçðÿäíîñòü 32 áèòà è âîçìîæíîñòü ïðîèçâîäèòü âû÷èñëåíèÿ
ñ 64- è 128-áèòîâûìè äàííûìè). Â êàæäûé êëàñòåð âõîäÿò: óïðàâëÿþùèé ñåðâåð,
ñåðâåð äîñòóïà, îáùèé êîììóòàòîð êëàñòåðíîãî êîìïëåêñà è ñèñòåìà õðàíåíèÿ
äàííûõ (ôàéëîâûé ñåðâåð).
Óïðàâëÿþùèé ñåðâåð èñïîëüçóåòñÿ äëÿ êîìïèëÿöèè çàäà÷, ïîñòàíîâêè çàäà÷
â î÷åðåäü, âûäåëåíèÿ ðåñóðñîâ çàäà÷å è çàïóñêà çàäà÷.
174 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4
 ñîñòàâå êëàñòåðà èìååòñÿ òðè ñåòè ïåðåäà÷è äàííûõ: ôàéëîâàÿ ñðåäà, ñåòü óïðàâëå-
íèÿ óçëàìè êëàñòåðà è ñåòü, êîòîðàÿ èñïîëüçóåòñÿ äëÿ îáìåíà ñîîáùåíèÿìè ìåæäó óçëàìè.
Óçëû êëàñòåðà íå èìåþò ñîáñòâåííûõ äèñêîâ, ïîýòîìó êàæäûé óçåë âî âðåìÿ
íà÷àëüíîé çàãðóçêè îáðàçóåò êîðíåâóþ ôàéëîâóþ ñèñòåìó ñåòè NFS (Network File
System). Çàòåì ñîçäàåòñÿ ðàçäåë ôàéëîâîé ñèñòåìû ñ ðàáî÷èìè äàííûìè çàäàíèé.
Ââîä-âûâîä ôàéëîâ îñóùåñòâëÿåòñÿ ïî ñåòè îáìåíà äàííûìè.
Èíäèâèäóàëüíûé ïîëüçîâàòåëüñêèé êàòàëîã (òàê íàçûâàåìûé äîìàøíèé êàòà-
ëîã ïîëüçîâàòåëÿ) ñîäåðæèò âñå ïîëüçîâàòåëüñêèå îáëàñòè ââîäà-âûâîäà, â êîòîðûõ
ìîãóò ðàçìåùàòüñÿ ïðîãðàììû çàäàíèé ïîëüçîâàòåëÿ.
Êàæäàÿ çàäà÷à èìååò ñâîé ïàñïîðò, â êîòîðîì óêàçàíà èíôîðìàöèÿ äëÿ ñèñòå-
ìû óïðàâëåíèÿ çàäà÷àìè, âåäóùåé î÷åðåäè çàäà÷ ïîëüçîâàòåëåé, íàçíà÷àþùåé ðå-
ñóðñû çàäà÷å, êîíòðîëèðóþùåé âûïîëíåíèå çàäà÷ è îñâîáîæäàþùåé èñïîëüçîâàí-
íûå ðåñóðñû ïîñëå çàâåðøåíèÿ çàäà÷è. Êëàñòåðíûé ðåñóðñ îïðåäåëÿåòñÿ êîëè÷åñ-
òâîì ïðîöåññîðîâ è âðåìåíåì ðåøåíèÿ çàäà÷è. Âûõîäíûå ôàéëû è ôàéëû
ñòàíäàðòíîãî âûâîäà ñîçäàþòñÿ â ðàáî÷åì êàòàëîãå çàäà÷è, åñëè íåò ñïåöèàëüíûõ
óêàçàíèé. Äëÿ ïîëüçîâàòåëåé îáåñïå÷èâàåòñÿ èíäèâèäóàëüíàÿ çàùèòà åãî äîìàøíå-
ãî êàòàëîãà îò äðóãèõ ïîëüçîâàòåëåé è çàùèòà ñàìîãî êîìïëåêñà îò
íåñàíêöèîíèðîâàííîãî äîñòóïà, â òîì ÷èñëå îò çàðåãèñòðèðîâàííûõ ïîëüçîâàòåëåé.
Ëîãè÷åñêàÿ ñèñòåìà ïàðàëëåëüíîãî ïðîãðàììèðîâàíèÿ îáåñïå÷èâàåò ñòàðò
ïðîãðàììû ïîëüçîâàòåëÿ íà ïåðâîì ïðîöåññîðå íà ïåðâîì óçëå èç ñïèñêà óçëîâ, âû-
äåëåííûõ äëÿ çàäàíèÿ, ñ ïîñëåäóþùèì äèíàìè÷íûì ñòàðòîì ïîðîæäàåìûõ ïîëüçî-
âàòåëüñêîé ïðîãðàììîé ïðîöåññîâ íà ñëåäóþùèõ ïðîöåññîðàõ ýòîãî ñïèñêà óçëîâ
êëàñòåðà. Ñâÿçü ïîðîæäåííûõ ïîëüçîâàòåëüñêèõ ïðîöåññîâ ìåæäó ñîáîé è ñ ïîðîæ-
äàþùèì ïðîöåññîì ïîääåðæèâàåòñÿ ÷åðåç êîììóíèêàöèîííûå áèáëèîòåêè ëîãè-
÷åñêîé ñèñòåìû, ôóíêöèîíàëüíî ñîîòâåòñòâóþùèå ðåàëèçîâàííîé â íåé âåðñèè èí-
òåðôåéñà MPI (Message Passing Interface). Âñå óçëû, âûäåëåííûå îäíîé çàäà÷å,
ìîãóò ñâÿçûâàòüñÿ ìåæäó ñîáîé ïî ñõåìå «êàæäûé ñ êàæäûì».
Çàïóñê çàäàíèÿ íà âûïîëíåíèå íà óçëàõ êëàñòåðà ìîæåò îñóùåñòâëÿòüñÿ ðàçíûìè
ñïîñîáàìè â çàâèñèìîñòè îò òîãî, ÿâëÿåòñÿ ëè çàäàíèå MPI-çàäà÷åé èëè îáû÷íîé íåïàðàë-
ëåëüíîé ïðîãðàììîé. Åñëè îäíà çàäà÷à ïîëó÷èëà â êà÷åñòâå ðåñóðñà ïðîöåññîð íåêîòîðîãî
óçëà, äðóãèå çàäà÷è íå ìîãóò ïîëüçîâàòüñÿ ïðîöåññîðàìè ýòîãî óçëà. Ïðåäïîëàãàåòñÿ, ÷òî
ñîáñòâåííî ðàáîòà ïîëüçîâàòåëÿ îñóùåñòâëÿåòñÿ ëèøü â ðàìêàõ åãî äîìàøíåãî êàòàëîãà
íà ñåðâåðå äîñòóïà, à äëÿ êîíòðîëÿ äîñòóïà ê âû÷èñëèòåëüíûì óçëàì äîñòàòî÷íî èñïîëü-
çîâàòü ìåõàíèçìû óïðàâëåíèÿ çàïóñêîì ïðîãðàìì ñ ïîìîùüþ ñïåöèàëüíîé êîìàíäû.
Âûáèðàÿ î÷åðåäíîå çàäàíèå èç î÷åðåäè, ïëàíèðîâùèê ðåñóðñîâ ÷èòàåò ïàñïîðò
çàäàíèÿ, îïðåäåëÿåò ñïèñîê âû÷èñëèòåëüíûõ ìîäóëåé, íà êîòîðûõ áóäåò âûïîëíÿòüñÿ
ïàðàëëåëüíîå çàäàíèå, îòêðûâàåò ê íèì äîñòóï äëÿ ïñåâäîïîëüçîâàòåëÿ — âëàäåëüöà
ëîãè÷åñêîé ñèñòåìû ïàðàëëåëüíîãî ïðîãðàììèðîâàíèÿ, â ðàìêàõ êîòîðîé áóäåò âû-
ïîëíÿòüñÿ çàäàíèå, çàïóñêàåò íà íèõ ýòó ëîãè÷åñêóþ ñèñòåìó, åñëè îíà íåàêòèâíà, è
âûïîëíÿåò êîìàíäíûé ôàéë ñòàðòà ïàðàëëåëüíîãî çàäàíèÿ. Êîìàíäíîìó ôàéëó ïåðåäà-
þòñÿ òàêèå ïàðàìåòðû, êàê êîëè÷åñòâî è èìåíà âûäåëåííûõ âû÷èñëèòåëüíûõ ìîäóëåé
(â êà÷åñòâå êîíôèãóðàöèîííûõ äàííûõ äëÿ áèáëèîòåêè îáìåíà ñîîáùåíèÿìè), è çàäà-
íèå çàïóñêàåòñÿ íà âû÷èñëåíèå, ïîñëå ÷åãî ïëàíèðîâùèê ðåñóðñîâ ïåðåõîäèò ê îáðà-
áîòêå ñëåäóþùåãî çàäàíèÿ, íàõîäÿùåãîñÿ â î÷åðåäè.
Ïðè ðàñ÷åòàõ ýôôåêòèâíîñòè ñëåäóåò ó÷èòûâàòü, ÷òî ìåæïðîöåññîðíûé îáìåí
äàííûìè ïðèâîäèò ê óðàâíèâàíèþ ýôôåêòèâíîñòè êàæäîãî ïðîöåññà ïî ñêîðîñòè ñ
ñàìûì ìåäëåííûì ïðîöåññîì.
Âçàèìîäåéñòâèå ïîëüçîâàòåëÿ ñ ñèñòåìîé ïîääåðæèâàåòñÿ ñðåäñòâàìè äèàëîãîâûõ
îêîí ñ òåðìèíàëà êëèåíòà. Ñåàíñ ðàáîòû íà÷èíàåòñÿ ñ ñîåäèíåíèÿ âû÷èñëèòåëüíîé ìà-
øèíû ïîëüçîâàòåëÿ ñ ñåðâåðîì äîñòóïà è çàïóñêà èíòåðàêòèâíîé ïðîãðàììû.
Çàäà÷à, òðåáóþùàÿ êîìïèëÿöèè, ñòàíîâèòñÿ â î÷åðåäü êîìïèëÿöèè. Êîìïèëÿ-
öèÿ èñïîëüçóåò Makefile, êîòîðûé ìîæåò áûòü ãîòîâûì èëè ãåíåðèðîâàòüñÿ ñèñ-
òåìîé óïðàâëåíèÿ çàäà÷àìè. Êðîìå òåêñòîâ ïðîãðàìì, ïîëüçîâàòåëü ìîæåò çàäàâàòü
ñâîè îïöèè äëÿ ôàéëîâ, êîòîðûå âêëþ÷àþòñÿ, è áèáëèîòåê.
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4 175
ÂÛÁÎÐ ÇÀÄÀ× ÄËß ÏÐÎÂÅÄÅÍÈß ÝÊÑÏÅÐÈÌÅÍÒÎÂ Ñ ÏÐÎÃÐÀÌÌÎÉ
ÏÀÐÀËËÅËÜÍÎÃÎ ÏÎÈÑÊÀ ÂÛÂÎÄÀ
Ñ ó÷åòîì îñîáåííîñòåé ñðåäû (ïðîãðàììíûõ ñðåäñòâ è îáîðóäîâàíèÿ) ôóíêöèî-
íèðîâàíèÿ ïðîãðàììû ïàðàëëåëüíîãî ïîèñêà âûâîäà ñèñòåìû ÀÏÑ äëÿ ýêñïåðè-
ìåíòèðîâàíèÿ ñ ýòîé ïðîãðàììîé áûëè âûáðàíû ñëåäóþùèå çàäà÷è.
1. ßâëÿåòñÿ ëè òàâòîëîãèåé ïðîïîçèöèîíàëüíàÿ ôîðìóëà âèäà
( )F F Fn1 2
� ?
2. ßâëÿåòñÿ ëè òàâòîëîãèåé ïðîïîçèöèîíàëüíàÿ ôîðìóëà âèäà F F Fn
1 � ?
Ðåøåíèå çàäà÷ ïåðâîãî òèïà íà êëàñòåðíîé ñèñòåìå ñâîäèòñÿ ê ðåøåíèþ n çà-
äà÷ âèäà «ÿâëÿåòñÿ ëè òàâòîëîãèåé ôîðìóëà Fi ?» (i n�{ }1,... , ), ïîñêîëüêó
( )F Fn1
� — òàâòîëîãèÿ òîãäà è òîëüêî òîãäà, êîãäà Fi — òàâòîëîãèÿ äëÿ êàæäî-
ãî i, i n�{ }1,... , .
Ðåøåíèå çàäà÷ âòîðîãî òèïà íà êëàñòåðíîé ñèñòåìå ñâîäèòñÿ ê ðåøåíèþ n çà-
äà÷ âèäà «ÿâëÿåòñÿ ëè òàâòîëîãèåé ôîðìóëà F Fi
?» (i n�{ }1,... , ), ïîñêîëüêó
F F Fn
1 � — òàâòîëîãèÿ òîãäà è òîëüêî òîãäà, êîãäà F Fi
— òàâòîëîãèÿ äëÿ
êàæäîãî i, i n�{ }1,... , .
Òàêèì îáðàçîì, êàæäûé äîñòóïíûé ïðîöåññîð ðàáîòàåò ñ áîëåå ïðîñòîé ôîð-
ìóëîé, ÷åì òà, ÷òî çàäàíà èçíà÷àëüíî.
ÎÐÃÀÍÈÇÀÖÈß ÏÀÐÀËËÅËÜÍÎÃÎ ÏÎÈÑÊÀ ÂÛÂÎÄÀ ÍÀ ÁÀÇÅ ÈÑ×ÈÑËÅÍÈß
ÀËÃÎÐÈÒÌÀ Î×ÅÂÈÄÍÎÑÒÈ
Ðåøåíèå çàäà÷è ïàðàëëåëüíîãî ïîèñêà âûâîäà íà áàçå àëãîðèòìà î÷åâèäíîñòè
â ñðåäå ÑÊÈÒ-1 îñóùåñòâëÿåòñÿ â ðåæèìå «õîçÿèí-ðàáîòíèê». Âõîäíûå äàí-
íûå — ýòî ôîðìóëà ëîãèêè âûñêàçûâàíèé âèäà F Fn1
� , êîëè÷åñòâî òðåáóå-
ìûõ ïðîöåññîðîâ k � 1 (k n� ), èç êîòîðûõ îäèí ïðîöåññîð âûïîëíÿåò ôóíêöèè
«ðóêîâîäèòåëÿ ðàáîò» («õîçÿèíà»), îñòàëüíûå — «èñïîëíèòåëè» («ðàáîòíèêè»).
Ïðîöåññîð-ðóêîâîäèòåëü ïîñûëàåò ñîîáùåíèÿ ïðîöåññîðàì-ðàáîòíèêàì è ïðèíè-
ìàåò îò íèõ ñîîáùåíèÿ. Êàæäûé äîñòóïíûé (ðàáî÷èé) ïðîöåññîð çàãðóæåí ïðî-
ãðàììîé ïîèñêà âûâîäà ôîðìóë ëîãèêè âûñêàçûâàíèé, îñíîâàííîé íà èñ÷èñëå-
íèè àëãîðèòìà î÷åâèäíîñòè, è i-é ïðîöåññîð-ðàáîòíèê íà÷èíàåò ðàáîòàòü ñ i-é
ôîðìóëîé (ò.å. ñ Fi ), i n�{ }1,... , , êîòîðàÿ óêàçûâàåòñÿ åìó ïðîöåññîðîì-ðóêîâîäè-
òåëåì â ñîîòâåòñòâóþùåì ñîîáùåíèè. Åñëè ôîðìóëà Fi ÿâëÿåòñÿ òàâòîëîãèåé, òî
i-é ïðîöåññîð-ðàáîòíèê ôîðìèðóåò îá ýòîì ñîîáùåíèå «Prover result_1» è, åñëè
åùå îñòàëèñü íåîáðàáîòàííûå ôîðìóëû F F Fm m n, , ,� �1 , ïðèíèìàåò ñîîáùåíèå,
ñîäåðæàùåå óêàçàíèå íà î÷åðåäíóþ ôîðìóëó Fm èç îñòàâøèõñÿ, êîòîðóþ ñëåäóåò
îáðàáàòûâàòü. Ïðîöåññ ïðîäîëæàåòñÿ äî òåõ ïîð, ïîêà èìåþòñÿ íåîáðàáîòàííûå
ôîðìóëû. Ôîðìóëà ÿâëÿåòñÿ òàâòîëîãèåé òîãäà è òîëüêî òîãäà, êîãäà âñå ïðîöåññî-
ðû ïðèñëàëè ñîîáùåíèå «Prover result_1». Òàêèì îáðàçîì, îòäåëüíûé ïðîöåññîð-ðà-
áîòíèê ìîæåò çà îäèí ñåàíñ ðàáîòû ïðîãðàììû ïàðàëëåëüíîãî ïîèñêà âûâîäà ðàáî-
òàòü ñ íåñêîëüêèìè ðàçíûìè ôîðìóëàìè ïåðå÷íÿ F Fn1 , ,� . Ïðîãðàììà, êîòîðàÿ
îñóùåñòâëÿåò óïðàâëåíèå ïîèñêîì — çàãðóçêó ðàáî÷èõ ïðîöåññîðîâ âõîäíûìè äàí-
íûìè (ïåðåñûëêó ñîîáùåíèé ïðîöåññîðàì) è àíàëèç ñîîáùåíèé, ïîñòóïàþùèõ îò
ðàáî÷èõ ïðîöåññîðîâ, èñïîëüçóåò MPI ôóíêöèè MPI_Send è MPI_Receive.
ÐÅÇÓËÜÒÀÒÛ ÝÊÑÏÅÐÈÌÅÍÒÎÂ
Ñ ïðîãðàììîé ïàðàëëåëüíîãî ïîèñêà âûâîäà ïðîâåäåíû äâå ñåðèè ýêñïåðèìåí-
òîâ. Äëÿ ïåðâîé ñåðèè âûáðàíû ñëåäóþùèå ôîðìóëû ëîãèêè âûñêàçûâàíèé
(ïðèâåäåíû íà ÿçûêå ÀÏËÀÍ).
Äëÿ ýêñïåðèìåíòà 1: Exp 1 = ( a_7 & a_6 & a_5 & a_4 & a_3 & a_2
& a_1 |/ ~(a_7) & a_6 & a_5 & a_4 & a_3 & a_2 & a_1 |/
~(a_6) & a_5 & a_4 & a_3 & a_2 & à_1 |/ ~(a_5) & a_4 & a_3 &
a_2 & à_1 |/ ~(a_4) & a_3 & a_2 & à_1 |/ ~(a_3) & a_2 & à_1
|/ ~(a_2) & à_1 |/ ~(à_1)) &
( a_6 & a_5 & a_4 & a_3 & a_2 & à_1 |/ ~(a_6) & a_5 &
a_4 & a_3 & a_2 & à_1 |/ ~(a_5) & a_4 & a_3 & a_2 & à_1 | /
~(a_4) & a_3 & a_2 & à_1 |/ ~(a_3) & a_2 & à_1 |/ ~(a_2) &
176 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4
à_1 |/ ~(à_1)) &
( a_5 & a_4 & a_3 & a_2 & à_1 |/ ~(a_5) & a_4 & a_3 &
a_2 & à_1 |/ ~(a_4) & a_3 & a_2 & à_1 |/ ~(a_3) & a_2 & à_1
|/ ~(a_2) & à_1 |/ ~(à_1)) &
( a_4 & a_3 & a_2 & à_1 |/ ~(a_4) & a_3 & a_2 & à_1 |/
~(a_3) & a_2 & à_1 |/ ~(a_2) & à_1 |/ ~(à_1)) &
( a_3 & a_2 & à_1 |/ ~(a_3) & a_2 & à_1 |/ ~(a_2) & à_1
|/ ~(à_1)) &
( a_2 & à_1 |/ ~(a_2) & à_1 |/ ~(à_1)) &
( à_1 |/ ~(à_1)).
Äëÿ ýêñïåðèìåíòà i � 1: Expi = (a_f(i) & a_(f(i)-1) & … & a_1 |/
~(a_f(i)) & a_(f(i)-1) & … & a_1 |/ … |/ ~(a_2) & a_1 |/
~(a_1)) & (a_(f(i)-1) & … & a_1 |/ ~(a_(f(i)-1)) &… & a_1 |/
… |/ ~(a_2) & a_1 |/ ~(a_1)) & Exp(i-1).
Çäåñü f i i( ) ( )� � �7 2 1 , ³ — öåëîå, 1 6� �i , f ( )7 18� .
Ôîðìóëà Åõð³.j ñîâïàäàåò ñ Åõð³ ñ òî÷íîñòüþ äî êîììóòàòèâíîñòè è àññîöèà-
òèâíîñòè. Êàê âèäíî èç ïðàâèë ïîñòðîåíèÿ ôîðìóë Åõð³, ñëîæíîñòü ïåðâûõ êîíúþíê-
òèâíûõ ÷ëåíîâ ôîðìóëû çíà÷èòåëüíî ïðåâîñõîäèò ñëîæíîñòü ïîñëåäíèõ åå êîíú-
þíêòèâíûõ ÷ëåíîâ, ïîýòîìó ïðè ïåðâîíà÷àëüíîì ðàñïðåäåëåíèè çàäàíèé ìåæäó
ïðîöåññîðàìè-ðàáîòíèêàìè íàãðóçêà íà íèõ íåðàâíîìåðíà. Ôîðìóëà Åõð³.j ñòðîèò-
ñÿ èç ôîðìóëû Åõð³ ïóòåì ïåðåñòàíîâêè êîíúþíêòèâíûõ ÷ëåíîâ è ðàññòàíîâêè ñêî-
áîê òàêèì îáðàçîì, ÷òîáû ñäåëàòü ïåðâîíà÷àëüíóþ íàãðóçêó ïðîöåññîðîâ-ðàáîòíè-
êîâ ïðèìåðíî îäèíàêîâîé. Ðåçóëüòàòû ýêñïåðèìåíòîâ ïðèâåäåíû â òàáë. 1 (âðåìÿ
âû÷èñëåíèé óêàçàíî â ñåêóíäàõ).
 òàáë. 2 ïîêàçàíî, ïðè êàêîì êîëè÷åñòâå ïðîöåññîðîâ äîñòèãíóòî ìàêñèìàëü-
íîå óñêîðåíèå â ýêñïåðèìåíòàõ ïåðâîé ñåðèè ïî îòíîøåíèþ ê äâóì ïðîöåññîðàì.
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4 177
×èñëî
ïðîöåñ
ñîðîâ
Ðåçóëüòàòû ýêñïåðèìåíòîâ äëÿ Expi
Exp1 Exp1.1 Exp2 Exp2.1 Exp3 Exp3.1 Exp4 Exp4.1 Exp5 Exp5.1 Exp6 Exp6.1 Exp6.2 Exp7
2 7 9 15 15 31 34 65 90 141 142 274 296 293 2091
3 7 6 11 10 15 9 34 51 68 78 136 166 137 1748
4 5 6 8 9 15 10 26 37 48 50 93 133 98 1733
5 7 7 10 10 15 14 24 40 43 62 82 113 86 1734
6 7 10 15 15 24 41 45 46 82 100 86 1716
7 10 12 17 18 25 41 45 66 66 95 92 1758
8 9 11 17 24 46 58 63 90 90 1711
9 10 12 19 25 45 63 63 88 92 1724
10 13 17 26 47 51 87 85 89 1748
11 19 28 51 71 86 89 96 1762
12 18 28 49 60 91 90 89 1755
13 19 28 51 91 89 89 1757
14 20 29 52 104 97 93 1736
15 22 31 53 90 95 93 1759
16 17 21 51 90 92 89 1772
17 141 96 97 98 1749
18 98 94 86 1765
19 99 98 98 1746
20 95 97 97 1754
21 101 100 100 1775
Ò à á ë è ö à 1
178 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4
Õàðàêòå
ðèñòèêè
Ïîêàçàòåëè óñêîðåíèÿ äëÿ Expi
Exp1 Exp1.v Exp2 Exp2.v Exp3 Exp3.v Exp4 Exp4.v Exp5 Exp5.v Exp6 Exp6.1 Exp6.2 Exp7
Âðåìÿ
íà äâóõ
ïðîöåññî
ðàõ
7 9 15 15 31 34 65 90 141 142 294 296 293 2091
Ìèíè-
ìàëüíîå
âðåìÿ
5 6 8 9 15 9 24 37 43 46 63 85 86 1711
×èñëî
ïðîöåñ-
ñîðîâ
4 3 4 4 3 3 5 4 5 6 8 10 5 8
Óñêîðå-
íèå 1,8 1,5 1,9 1,7 6,2 3,8 2,7 2,4 3,3 3 4,7 3,5 3,4 1,2
Ò à á ë è ö à 2
×èñëî
ïðîöåññîðîâ
Ðåçóëüòàòû ýêñïåðèìåíòîâ äëÿ Ti
T1 T2 T3 T4 T5 T6 T7 T8 T9 T10
2 15 22 52 125 237 440 652 1054 1343 2234
3 11 19 31 62 126 250 310 541 746 1261
4 9 14 23 49 90 155 220 366 532 814
5 10 16 23 35 66 110 173 261 409 587
6 8 14 18 27 54 88 152 232 331 481
7 9 13 21 33 51 80 128 221 287 424
8 9 19 22 30 50 67 116 163 244 377
9 11 16 24 27 45 64 94 155 254 334
10 11 17 25 25 43 57 97 143 209 300
11 19 27 45 58 82 129 174 292
12 19 27 44 58 78 123 162 241
13 23 32 36 61 81 102 160 228
14 20 30 37 49 80 100 164 224
15 22 30 37 51 72 100 132 211
16 25 37 48 64 99 188
17 27 38 49 65 97 188
18 26 41 50 60 94 186
19 27 39 54 63 82 171
20 28 43 55 65 77 174
21 42 51 63 89 179
22 35 55 65 82 169
23 38 54 67 83 161
24 35 54 69 93 153
25 38 54 67 80 135
26 42 70 93 144
27 48 63 95 132
28 45 68 80 133
29 52 67 133
30 46 65 142
31 47 63 134
32 55 63 136
33 52 61 154
34 61 145
Ò à á ë è ö à 3
Äëÿ âòîðîé ñåðèè ýêñïåðèìåíòîâ âûáðàíà çà-
äà÷à îïðåäåëåíèÿ ñóùåñòâîâàíèÿ ïóòåé ìåæäó çà-
äàííîé âåðøèíîé îðèåíòèðîâàííîãî ãðàôà è êàæ-
äîé èç îñòàëüíûõ åãî âåðøèí, êðîìå òåõ, êîòîðûå
ñìåæíû ñ çàäàííîé âåðøèíîé. Ðàññìîòðåíû äâà
âèäà îðãðàôîâ: îðèåíòèðîâàííûå äåðåâüÿ è îðãðà-
ôû ñ âûäåëåííîé âåðøèíîé.  ïåðâîì ñëó÷àå çà-
äàííîé âåðøèíîé ÿâëÿåòñÿ êîðåíü äåðåâà, âî âòî-
ðîì — âûäåëåííàÿ âåðøèíà.
Äåðåâî Ò1 îïèñûâàåòñÿ ôîðìóëîé ëîãèêè
âûñêàçûâàíèé ñëåäóþùåãî âèäà (íà ÿçûêå
ÀÏËÀÍ):
T1 = (~(a_0) |/ a_1) & (~(a_0) |/
a_2) & (~(a_0) |/ a_3) & (~(a_0) |/
a_4) & (~(a_0) |/ a_5) & (~(a_1) |/
a_6) & (~(a_2) |/ a_7) & (~(a_3) |/
a_8) & (~(a_4) |/ a_9) & (~(a_5) |/
a_10).
Ïóòü ìåæäó êîðíåì äåðåâà (âåðøèíîé
à_0) è âåðøèíîé à_9, íàïðèìåð, ñóùåñòâóåò,
åñëè ôîðìóëà Ò1
(à_0
à_9) ÿâëÿåòñÿ òàâ-
òîëîãèåé. Äåðåâî Ò³ (1 10� �³ ) èìååò 10 5 1� �( )³ âåðøèí. Îðãðàô Gri (1 4� �³ )
èìååò 10 5 1� �( )³ âåðøèí è îáðàçóåòñÿ èç äåðåâà Ò³ ïóòåì èçìåíåíèÿ íàïðàâëåíèÿ
äóãè (à_(5(³ –1)+1), à_(5³ +1)). Âûäåëåííîé ÿâëÿåòñÿ âåðøèíà à_0. Ðåçóëüòàòû
ýêñïåðèìåíòîâ ïðèâåäåíû â òàáë. 3, 4 (âðåìÿ âû÷èñëåíèé óêàçàíî â ñåêóíäàõ).
 òàáë. 5 ïîêàçàíî,
ïðè êàêîì êîëè÷åñòâå ïðî-
öåññîðîâ äîñòèãíóòî ìàê-
ñèìàëüíîå óñêîðåíèå äëÿ
îðèåíòèðîâàííûõ äåðåâü-
åâ, â òàáë. 6 — ïðè êàêîì
êîëè÷åñòâå ïðîöåññîðîâ
äîñòèãíóòî ìàêñèìàëüíîå
óñêîðåíèå äëÿ îðãðàôîâ
ñ âûäåëåííîé âåðøèíîé.
ÇÀÊËÞ×ÅÍÈÅ
Âðåìÿ ðåøåíèÿ çàäà÷ âî âñåõ ñëó÷àÿõ ñóùåñòâåííî óìåíüøàåòñÿ ïðè èñïîëüçîâàíèè
áîëåå ÷åì îäíîãî ðàáî÷åãî ïðîöåññîðà, à óñêîðåíèå âû÷èñëåíèé íåëèíåéíî çàâèñèò
îò êîëè÷åñòâà ðàáî÷èõ ïðîöåññîðîâ. Ðåçóëüòàòû ýêñïåðèìåíòîâ ñâèäåòåëüñòâóþò,
÷òî ëó÷øèå âðåìåííûå ïîêàçàòåëè ïðè èñïîëüçîâàíèè ïðîãðàììû ïàðàëëåëüíîãî
ïîèñêà âûâîäà, ôóíêöèîíèðóþùåé íà êëàñòåðíîé ñèñòåìå, äëÿ ôîðìóë âèäà
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4 179
Õàðàêòåðèñòèêè
Ïîêàçàòåëè óñêîðåíèÿ äëÿ Ti
T1 T2 T3 T4 T5 T6 T7 T8 T9 T10
Âðåìÿ íà äâóõ
ïðîöåññîðàõ
15 22 52 125 237 440 652 1054 1343 2234
Ìèíèìàëüíîå
âðåìÿ
8 13 18 36 42 60 77 132 132
×èñëî
ïðîöåññîðîâ
6 7 6 13 26 18 20 15 27
Óñêîðåíèå 1,9 1,7 2,9 6,7 10,5 10,9 13,9 10,2 16,9
Ò à á ë è ö à 5
×èñëî
ïðîöåññîðîâ
Ðåçóëüòàòû
ýêñïåðèìåíòîâ äëÿ Gri
Gr1 Gr2 Gr3 Gr4
2 19 28 64 146
3 13 21 43 93
4 12 16 29 75
5 19 21 38 72
6 25 31 50
7 42 33 45
8 17 29 51
9 28 29 42
10 24 30 52
11 32 28 44
12 37 47
13 37 44
14 34 43
15 37 45
16 36 53
17 41
Ò à á ë è ö à 4
Õàðàêòåðèñòèêè
Ïîêàçàòåëè óñêîðåíèÿ äëÿ Gri
Gr1 Gr2 Gr3 Gr4
Âðåìÿ íà äâóõ
ïðîöåññîðàõ
19 28 64 146
Ìèíèìàëüíîå
âðåìÿ
12 16 28 41
×èñëî
ïðîöåññîðîâ
4 4 11 17
Óñêîðåíèå 1,6 1,8 2,3 3,6
Ò à á ë è ö à 6
F Fn1
� íàáëþäàþòñÿ òîãäà, êîãäà ðàáî÷èõ ïðîöåññîðîâ áîëüøå, ÷åì îäèí,
íî ÷èñëî èõ íåâåëèêî ïî ñðàâíåíèþ ñ ÷èñëîì n êîíúþíêòèâíûõ ÷ëåíîâ ôîðìó-
ëû. Òàêèì îáðàçîì, ÷òîáû äîñòè÷ü íàèáîëüøåãî óñêîðåíèÿ ïðè ðåøåíèè çàäà÷
ðàññìàòðèâàåìîãî êëàññà íà êëàñòåðíîé ñèñòåìå ñðåäñòâàìè ÀÏÑ, íå íóæíî èñ-
ïîëüçîâàòü ìàêñèìàëüíîå êîëè÷åñòâî ïðîöåññîðîâ.
Îòìåòèì, ÷òî ýêñïåðèìåíòû ïðîâîäèëèñü â ðåæèìå óäàëåííîãî äîñòóïà
ê ñðåäñòâàì âû÷èñëåíèÿ. Èñïîëüçóåìàÿ âû÷èñëèòåëüíàÿ ñèñòåìà ÿâëÿåòñÿ ðåñóðñîì
êîëëåêòèâíîãî ïîëüçîâàíèÿ. Îñîáåííîñòè âõîäíûõ äàííûõ (ôîðìóë) â ýêñïåðèìåí-
òàõ îáóñëîâèëè íåðàâíîìåðíóþ çàãðóçêó ïðîöåññîðîâ. ÀÏÑ — ñèñòåìà, îðèåíòè-
ðîâàííàÿ íà ñîçäàíèå íå ñòîëüêî âûñîêîñêîðîñòíûõ ïðîãðàììíûõ ïðîäóêòîâ,
ñêîëüêî íà ïîñòðîåíèå ïðîòîòèïîâ ïðèêëàäíûõ ïðîãðàìì, ÷òî ñêàçûâàåòñÿ íà
âðåìåííûõ ïîêàçàòåëÿõ ðàáîòû ïðîãðàììû.
 äàëüíåéøåì ïëàíèðóåòñÿ èññëåäîâàòü âîçìîæíîñòè ïàðàëëåëüíûõ ÀÏÑ-ïðî-
ãðàìì äëÿ ðåøåíèÿ äðóãèõ êëàññîâ çàäà÷ íà âû÷èñëèòåëüíîì êîìïëåêñå ÑÊÈÒ.
ÑÏÈÑÎÊ ËÈÒÅÐÀÒÓÐÛ
1. Y a m a g u c h i T . , T e z u k a Y . , K a k u s h o O . Parallel processing of resolution // Proc. of 9th Joint
Conf. on AI (Los Angeles, 1985). — San Francisco: Morgan Kaufmann Publ. Inc., 1985. — 2. —
P. 1178–1180.
2. V i t t e r J . S . , S i m o n s R . A . Parallel algorithms for unification and other complete problems // Proc.
of ACM’84 Ann. Conf. “The Fifth Generation Challenge,” 1984. — New York: ACM, 1984. — P. 75–84.
3. S c h u m a n n J . , L e t z R . PARTHEO: A high-performance parallel theorem prover // Proc. of
CADE’90 (Kaiserlautern). — Berlin; New York: Springr-Verlag, 1990. — P. 40–56.
4. W o l f A . , L e t z R . Strategy parallelism in automated theorem proving // IJPRAI. — 1999. — 13, N 2.
— P. 219–245.
5. B o n a c i n a M . P . Ten years of parallel theorem proving: a perspective // Notes of the Workshop on
Strategies in Automated Deduction, Sec. Feder. Logic Conf. (Italy, July, 1999). — Trento, 1999. —
P. 3–15.
6. K a p i t o n o v a J . V . , L e t i c h e v s k i A . A . , a n d K o n o z e n k o S . V . Computations in aps //
Theoret. Computer Sci. — 1993. — 119. — P. 145–171.
7. Ê à ï è ò î í î â à Þ . Â . , Ë å ò è ÷ å â ñ ê è é À . À . , Â î ë ê î â Â . À . Äåäóêòèâíûå ñðåäñòâà
ñèñòåìû àëãåáðàè÷åñêîãî ïðîãðàììèðîâàíèÿ // Êèáåðíåòèêà è ñèñòåìíûé àíàëèç. — 2000. — ¹ 1.
— Ñ. 17–35.
8. à ë ó ø ê î â  . Ì . Î çàäà÷àõ òåîðèè àâòîìàòîâ è èñêóññòâåííîãî èíòåëëåêòà // Êèáåðíåòèêà. —
1970. — ¹ 2. — Ñ. 3–17.
9. Ä å ã ò ÿ ð å â À . È . , Ë ÿ ë å ö ê è é À .  . Ëîãè÷åñêèé âûâîä â ÑÀÄ // Ìàòåìàòè÷åñêèå îñíîâû
ñèñòåì èñêóññòâåííîãî èíòåëëåêòà. — Êèåâ: Èí-ò êèáåðíåòèêè ÀÍ ÓÑÑÐ, 1981. — Ñ. 3–11.
10. Ê î â à ë ü  . Ì . , Ñ å ð ã ³ º í ê î ² .  . ÑÊ²Ò — óêðà¿íñüêèé ñóïåðêîìï’þòåðíèé ïðîåêò // ³ñí.
ÍÀÍ Óêðà¿íè, 2005. — ¹ 8. — Ñ. 3–13.
Ïîñòóïèëà 19.11.2009
180 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4
|
| id | nasplib_isofts_kiev_ua-123456789-45253 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 0023-1274 |
| language | Russian |
| last_indexed | 2025-12-07T18:40:35Z |
| publishDate | 2010 |
| publisher | Інститут кібернетики ім. В.М. Глушкова НАН України |
| record_format | dspace |
| spelling | Летичевский, А.А. Герман, В.Н. Мороховец, М.К. Щеголева, Н.Н. 2013-06-10T19:01:56Z 2013-06-10T19:01:56Z 2010 Параллельный поиск вывода в логическом исчислении на основе системы алгебраического программирования / A.А. Летичевский, В.Н. Герман, М.К. Мороховец, Н.Н. Щеголева // Кибернетика и системный анализ. — 2010. — № 4. — С. 169-180. — Бібліогр.: 10 назв. — рос. 0023-1274 https://nasplib.isofts.kiev.ua/handle/123456789/45253 510.66:004.272.2 Описано програмні засоби паралельного пошуку логічного виводу у пропозиційному численні та подано результати експериментів з ними. Програмні засоби розроблено на базі системи алгебричного програмування АПС та кластерного комплексу СКІТ-1. Software for parallel inference search in propositional calculus is described and used to obtain experimental results. The software is based on the Algebraic Programming System APS and the cluster complex SCIT-1. ru Інститут кібернетики ім. В.М. Глушкова НАН України Кибернетика и системный анализ Программно-технические комплексы Параллельный поиск вывода в логическом исчислении на основе системы алгебраического программирования Паралельний пошук виводу в логічному численні на основі системи алгебричного програмування Parallel inference search in a logical calculus on the base of the Algebraic Programming System Article published earlier |
| spellingShingle | Параллельный поиск вывода в логическом исчислении на основе системы алгебраического программирования Летичевский, А.А. Герман, В.Н. Мороховец, М.К. Щеголева, Н.Н. Программно-технические комплексы |
| title | Параллельный поиск вывода в логическом исчислении на основе системы алгебраического программирования |
| title_alt | Паралельний пошук виводу в логічному численні на основі системи алгебричного програмування Parallel inference search in a logical calculus on the base of the Algebraic Programming System |
| title_full | Параллельный поиск вывода в логическом исчислении на основе системы алгебраического программирования |
| title_fullStr | Параллельный поиск вывода в логическом исчислении на основе системы алгебраического программирования |
| title_full_unstemmed | Параллельный поиск вывода в логическом исчислении на основе системы алгебраического программирования |
| title_short | Параллельный поиск вывода в логическом исчислении на основе системы алгебраического программирования |
| title_sort | параллельный поиск вывода в логическом исчислении на основе системы алгебраического программирования |
| topic | Программно-технические комплексы |
| topic_facet | Программно-технические комплексы |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/45253 |
| work_keys_str_mv | AT letičevskiiaa parallelʹnyipoiskvyvodavlogičeskomisčisleniinaosnovesistemyalgebraičeskogoprogrammirovaniâ AT germanvn parallelʹnyipoiskvyvodavlogičeskomisčisleniinaosnovesistemyalgebraičeskogoprogrammirovaniâ AT morohovecmk parallelʹnyipoiskvyvodavlogičeskomisčisleniinaosnovesistemyalgebraičeskogoprogrammirovaniâ AT ŝegolevann parallelʹnyipoiskvyvodavlogičeskomisčisleniinaosnovesistemyalgebraičeskogoprogrammirovaniâ AT letičevskiiaa paralelʹniipošukvivoduvlogíčnomučislennínaosnovísistemialgebričnogoprogramuvannâ AT germanvn paralelʹniipošukvivoduvlogíčnomučislennínaosnovísistemialgebričnogoprogramuvannâ AT morohovecmk paralelʹniipošukvivoduvlogíčnomučislennínaosnovísistemialgebričnogoprogramuvannâ AT ŝegolevann paralelʹniipošukvivoduvlogíčnomučislennínaosnovísistemialgebričnogoprogramuvannâ AT letičevskiiaa parallelinferencesearchinalogicalcalculusonthebaseofthealgebraicprogrammingsystem AT germanvn parallelinferencesearchinalogicalcalculusonthebaseofthealgebraicprogrammingsystem AT morohovecmk parallelinferencesearchinalogicalcalculusonthebaseofthealgebraicprogrammingsystem AT ŝegolevann parallelinferencesearchinalogicalcalculusonthebaseofthealgebraicprogrammingsystem |