Բանաձևերի լուծելիություն տեսություններում
 |
Այս հոդվածն աղբյուրների կարիք ունի։ Դուք կարող եք բարելավել հոդվածը՝ գտնելով բերված տեղեկությունների հաստատումը վստահելի աղբյուրներում և ավելացնելով դրանց հղումները հոդվածին։ Անհիմն հղումները ենթակա են հեռացման։ |
 |
Այս հոդվածը կարող է վիքիֆիկացման կարիք ունենալ Վիքիպեդիայի որակի չափանիշներին համապատասխանելու համար։ Դուք կարող եք օգնել հոդվածի բարելավմանը՝ ավելացնելով համապատասխան ներքին հղումներ և շտկելով բաժինների դասավորությունը, ինչպես նաև վիքիչափանիշներին համապատասխան այլ գործողություններ կատարելով։ |
Բանաձևերի լուծելիություն տեսություններում ― (անգլ․ Satisfiability modulo theories ― SMT) ինֆորմատիկայում և մաթեմատիկական տրամաբանությունում տրամաբանական բանաձևերի լուծելիության պրոբլեմի տեսակ է, որտեղ հաշվի են առնվում դրանց հիմքում ընկած տեսությունները։ Ինֆորմատիկայում հաճախակի օգտագործվող տեսություններից են իրական թվերի տեսությունը, ամբողջ թվերի տեսությունը, ինչպես նաև տարատեսակ տվյալների կառուցվածքների (ցուցակ, զանգված, բիթային վեկտոր և այլն) տեսությունները։ SMT֊ն կարելի է դիտարկել նաև որպես սահմանափակումների լուծելիության խնդրի մի տեսակ՝ դրանով իսկ որպես նաև սահմանափակումներով ծրագրավորման ֆորմալ մոտեցում։
Սահմանումներ[խմբագրել | խմբագրել կոդը]
SMT բանաձևը առաջին կարգի տրամաբանության բանաձև է, որտեղ որոշ ֆունկցիաների ու պրեդիկատների նշանակումներ (սիմվոլներ) ունեն լրացուցիչ նշանակություն, և SMT֊ն այդ բանաձևի լուծելիությունը որոշող խնդիրն է։ Այլ խոսքերով՝ պատկերացնենք Բուլյան լուծելիության խնդրի բանաձև, որում բինար փոփոխականները փոխարինված են ոչ֊բինար փոփոխականների բազմության վրա որոշված պրեդիկատներով։ Սովորաբար պրեդիկատը ոչ֊բինար արժեքների համար բինար արժեքներ վերադարձնող ֆունկցիա է։ Պրեդիկատների օրինակներ են գծային անհավասարությունները (օր․ )։ Պրեդիկատները մեկնաբանվում են ըստ իրենց տեսությունների։
Կիրառություններ[խմբագրել | խմբագրել կոդը]
SMT բանաձևերը լուծող գործիքները կիրառելի են վերիֆիկացիայի, ծրագրերի կոռեկտության ստուգման, սիմվոլիկ կատարման վրա հիմնված թեսթավորման, և մատչելի ծրագրերի մեջ պետք եղածը որոնելով ծրագրերի հատվածների գեներացիայի համար։
Վերիֆիկացիա[խմբագրել | խմբագրել կոդը]
Կոմպյուտերային ծրագրերի թեսթավորման համար հաճախ օգտագորխվում են SMT բանաձևերը լուծող գործիքներ։ Ընդունված մեթոդ է նախապայմանները, ետպայմանները, կրկնությունների պայմանները և պնդումները թարգմանել SMT բանաձևերի՝ որոշելու համար, որ բոլոր հատկությունները պահպանվում են։
Սիմվոլիկ կատարում[խմբագրել | խմբագրել կոդը]
SMT բանաձևերը լուծող գործիքների կարևոր կիրառություն է ծրագրերի վերլուծության և թեսթավորման ժամանակ սիմվոլիկ կատարումը։