Մասնակից:Արթուր Խամիսյան/Ավազարկղ

Ասույթային արտածումների բարդություն

Արտածումների բարդության տեսությունը ուսումնասիրում է բարդության գաղափարը տրամաբանության տեսանկյունից: Թեորեմի ապացուցման բարդության մեծությունը կարելի է նկարագրել տարբեր եղանակներով՝ ինչպիսին են տրված համակարգում նրա կարճագույն ապացույցի երկարությունը (size), քայլերի քանակը (steps), օգտագործված տարածության մեծությունը (space), յուրաքանչյուր քայլում օգտագործված պնդումների մեծագույն երկարությունը (width): Բնական է, որ ապացույցի օպտիմալությունը էապես կախված է այն համակարգից, որում կատարվում է ապացույցը: Ֆորմալ տեսություններից ամենապարզ՝ ասույթային հաշվի արտածման բարդության հետազոտումների թվացյալ պարզությունը և հետևաբար նաև ոչ այնքան կարևոր լինելը կտրականապես հերքեց Կուկի և Ռեքաուի [17] հոդվածն, որտեղ ապացուցվել էր, որ ասույթային արտածումների երկարությունների և հաշվարկելիության բարդության դասերի տարանջատման միջև առկա է ֆունդամենտալ կապ՝ NP դասը փակ է լրացման նկատմամբ այն և միայն այն դեպքում, եթե գոյություն ունի ասույթային հաշվի այնպիսի արտածման համակարգ, որում բոլոր նույնաբանությունների արտածումների երկարությունները բազմանդամորեն սահմանափակ են (այդպիսի համակարգը հեղինակները անվանում են սուպեր համակարգ): Այդ դիտակետից առաջացել է այսպես կոչված Կուկ-Ռեքաու ծրագիրը, որը հանդիսանում է ասույթային հաշվի համակարգերում արտածման բարդության բնութագրիչների հետազոտման ակտիվացման սկզբնակետերից մեկը և որը ներառում է հետևյալ հիմնական ուղղություները՝

• Տրված համակարգում բանաձևերի արտածման բնութագրիչների գնահատում,
• Նոր, առավել արդյունավետ համակարգերի սահմանում,
• Նոր, առավել բարդ արտածվող բանաձևերի որոնում:

Վերջերս  Գորդեևի և Հեյսլերի կողմից ապացուցվել է, որ NP=PSPACE և, հետևաբար,NP = coNP = PSPACE: Այսպիսով, սուպեր համակարգ գոյություն ունի: Հայտնի է, որ բազմաթիվ համակարգեր սուպեր չեն, սակայն ասույթային հաշվի առավել բնական (սեկվենցիալ կամ Ֆրեգեի) համակարգերի, ինչպես նաև վերջերս կառուցված որոշ համակարգերի վերաբերյալ սուպեր լինելու խնդիրը դեռ բաց է, հետևաբար խիստ արդիական է և անհրաժեշտ այդպիսի համակարգերի ուսումնասիրությունը արտածումների բարդության տեսանկյունից:

Սա հեռահար նպատակն է, սակայն առկա են նաև այլ հետաքրքրություններ, որոնցով նույնապես հիմնավորվում են այս ոլորտում առկա հետազոտությունների մեծամասնությունը: Այդպիսի խնդիրներից է, մասնավորապես, ԻՐԱԳՈՐԾԵԼԻՈՒԹՅԱՆ խնդրի  /SAT problem-ի/ լուծումը, որը կարող է բացահայտել արդեն P և NP դասերի փոխհարաբերությունը: Հայտնի է, որ ասույթային հաշվի յուրաքանչյուր բանաձև որոշակի ձևափոխությամբ կարելի է ներկայացնել այնպիսի կոնյունկտիվ նորմալ ձևով (ԿՆՁ), որի երկարությունը ունի ոչ ավելին, քան գծային աճ սկզբնական բանաձևի երկարության համեմատությամբ, և որն անիրագործելի է այն և միայն այն դեպքում, երբ ինքը բանաձևը նույնաբանություն է: Անիրագոծելիությունը հաստատող որևէ ալգորիթմ սահմանում է որոշակի արտածման համակարգ, որը կրկնօրինակում է ալգորիթմի կատարման քայլերը և, հակառակը,  անիրագոծելիությունը փաստող որևէ արտածման համակարգ հանդիսանում է SAT problem-ը լուծող ալգորիթմ: SAT problem-ի ժամանակակից հետազոտողները որոնում են որոշակի «թույլ» համակարգերում (Resolution, Polynomial Calculus, Analytic Tableaux, Catting Planes, Cut-fee Sequence, Elimination, Bounded Frege) արտածումների բարդության վերին և ստորին գնահատականները, որոնք հուշում են SAT problem-ի լուծման համար նվազագույն և առավելագույն բավարար ռեսուրսների մասին: Հիմնավորվել է, որ օգտագործված հիշողությունը հանդիսանում է կարևորագույն պարամետրը SAT-problem-ի լուծման ընթացքում, հետևաբար, արտածման space բարդությունը կարող է լինել օգտակար այս հարցում: Վերջերս կատարված հետազոտությունների արդյունքները փաստում են resolution համակարգում space բարդության համար ստացված տեսական արդյունքների և միևնույն ժամանակահատվածում պրակտիկորեն ստացված բարդության մեծությունների իրական մոտիկությունը: Այսպիսով, արտածումների բարդության հետազոտումները կարևոր են նաև «թույլ» համակարգերում:

Արտածումների բարդության վերոհիշյալ, ինչպես նաև որոշ այլ հարցեր, որոնք վերաբերում են բազմարժեք տրամաբանության որոշ տարատեսակների համակարգերում արտածումների բարդությունների գնահատմանը, ունենալով տեսական նշանակություն, ունեն նաև պրակտիկ կիրառություն թեորեմների արտածումների ավտոմատացման ընթացքում, հետևրաբար նաև Formal Verification, Artificial Intelligence, Operations Research, Computational Biology, Cryptography, Data Mining, Machine Learning, Hardware Design-ի հետ առնչվող հետազոտումներում։

Գրականություն

• S. R. Buss, An Introduction to Proof Theory, in: Handbook of Proof Theory, edited by S. R. Buss, Elsevier, Amsterdam, (1998), pp.1-78.
• S. R. Buss, Propositional Proof Complexity: An Introduction, in: Computational Logic, Eds. U. Berger and H. Schwichtenberg, Springer-Verlag, Berlin, (1999), pp.127-178.
• S. A. Cook and R. A. Reckhow, The relative efficiency of propositional proof systems, J. of Symbolic Logic, 44(1), (1979), pp.36-50.
• P. Pudl´ak, The lengths of proofs, in: Handbook of Proof Theory, S.R. Buss ed., Elsevier, (1998), pp.547-637
• J.Krajichek, Proof Complexity, Encyclopedia of Mathematics and its Applications, 170, Cambridge University Press, 2019