Пређи на садржај

САТ проблем

С Википедије, слободне енциклопедије
(преусмерено са Boolean satisfiability problem)

У математици и информатици, САТ проблем или проблем задовољивости се састоји у утврђивању да ли се променљивима неког буловског израза могу доделити вредности тако да цела формула има вредност ТАЧНО, или формула има вредност НЕТАЧНО за све могуће комбинације вредности променљивих. У другом случају се каже да је функција незадовољива; а у супротном је задовољива. Променљиве су буловске (имају вредности 0 или 1), што значи да је проблем бинарне природе.

Основне дефиниције, терминологија и примене

[уреди | уреди извор]

У теорији комплексности, САТ проблем је проблем одлучивања, који се састоји из буловских израза записаних само помоћу оператора И, ИЛИ, НЕ, променљивих, и заграда.

Питање је: ако је дат израз, да ли постоји нека додела вредности ТАЧНО и НЕТАЧНО променљивима, таква да цео израз има вредност ТАЧНО? Ако је тако, каже се да је формула задовољива. САТ проблем припада класи НП-комплетних проблема. Овај проблем је од кучне важности за разне области рачунарства, укључујући теоријско рачунарство, алгоритмику, вештачку интелигенцију и дизајн хардвера.

Проблем се може значајно поједноставити, а да остане НП-комплетан. Уз примену Де Морганових закона, можемо да претпоставимо да се оператори негације примењују искључиво директно на променљиве, не на изразе; променљиву или њену негацију називамо литералом. На пример, и x1 и ~(x2) (где је ~ симбол за негацију) су литерали - први је позитиван литерал, а други је негативан. Ако групишемо литерале оператором ИЛИ, добијамо клаузе, попут (x1 или ~(x2)). Коначно, нека се израз састоји од конјункција (И) клауза - ово је конјуктивна нормална форма (КНФ). Одређивање да ли је израз овог облика НП-комплетан, чак и ако свака клауза има највише три литерала. Овакав последњи проблем се назива 3-САТ.

Са друге стране, ако сваку клаузу ограничимо на највише два литерала, резултујући проблем, 2-САТ, је НЛ-комплетан. Такође, ако свака клауза мора да буде Хорнова клауза, са највише једним позитивним литералом, резултујући проблем, Хорнова задовољивост, је П-комплетан.

Кукова теорема доказује да је САТ проблем НП-комплетан. Штавише, ово је био први проблем за који је доказано да је НП-комплетан. Међутим, осим овог теоријског значаја, током протекле деценије су развијени ефикасни алгоритми за САТ проблем, који су допринели великом напретку у нашој способности да аутоматски решавамо проблеме који имају десетине хиљада променљивих и милионе услова.

Комплексност и верзије

[уреди | уреди извор]

НП-комплетност

[уреди | уреди извор]

САТ је био први проблем за који је откривено да је НП-комплетан, што је 1971. доказао Стивен Кук (види Кукову теорему за доказ). До тада чак није ни постојао концепт НП-комплетног проблема. Проблем остаје НП-комплетан чак и кад су сви изрази записани у конјуктивној нормалној форми са три литерала по клаузи (3-КНФ), што даје 3-САТ проблем. Овакав израз је облика:

(x11 ИЛИ x12 ИЛИ x13) И
(x21 ИЛИ x22 ИЛИ x23) И
(x31 ИЛИ x32 ИЛИ x33) И ...

где је свако x променљива или негација променљиве, и свака променљива може да се појављује више пута у изразу.

Корисно својство Куковог свођења јесте да одржава број прихватајућих одговора. На пример, ако граф има 17 валидних 3-бојења, САТ формула добијена свођењем ће имати 17 задовољавајућих додела.

2-задовољивост

[уреди | уреди извор]

САТ проблем је лакши ако се ограничимо на формуле у дисјунктивној нормалној форми, то јест, формуле које се састоје од дисјункције (ИЛИ) терма, где је сваки терм конјункција (ИЛИ) литерала. Таква формула је задовољива ако и само ако је бар један њен терм задовољив, а терм је задовољив ако и само ако не садржи и x и НЕ x за неку променљиву x. Ово се може проверити у полиномијалном времену.

САТ је такође лакши ако је број литерала по клаузи ограничен на 2, у ком случају се зове 2-САТ. И овај проблем се може решити у полиномијалном времену, и комплетан је за класу НЛ. Слично, ако ограничимо број литерала по клаузи на 2, и заменимо операторе И операцијама ексклузивне дисјункције, добијамо ексклузивно или 2-САТ проблем, који је комплетан за СЛ = Л.

Једна од најважнијих верзија САТ проблема је ХОРНСАТ, где је израз конјункција Хорнових клауза. Овај проблем је решив у полиномијалном времену помоћу алгоритма Хорнова задовољивост. ХОРНСАТ је П-комплетан проблем. Може се посматрати као П верзија САТ проблема.

Ако класе комплексности П и НП нису једнаке, ниједна од ових верзија није НП-комплетна, за разлику од САТ проблема. Претпоставка да П и НП нису једнаке још увек није доказана.

3-задовољивост

[уреди | уреди извор]

3-задовољивост је специјални случај k-задовољивости (k-САТ) или просто САТ, где свака клауза садржи тачно k = 3 литерала. Ово је један од Карпових 21 НП-комплетних проблема.

Следи један пример, симбол ~ означава негацију:

E = (x1 или ~x2 или ~x3) и (x1 или x2 или x4)

E има две клаузе (одвојене заградама), четири литерала (x1, x2, x3, x4), и k=3 (три литерала по клаузи).

Да бисмо решили овакав 3-САТ проблем, морамо да утвридмо да ли постоји истинитосна вредност (ТАЧНО или НЕТАЧНО) коју можемо да доделимо сваком од литерала (x1 до x4) тако да цео израз има вредност ТАЧНО. У горњем примеру постоји таква додела (x1 = ТАЧНО, x2 = ТАЧНО, x3=ТАЧНО, x4=ТАЧНО), па је ова формула задовољива. Ово је само једна од много могућих додела, јер у овом случају би свака комбинација где је x1 = ТАЧНО исправна. У случају да не постоји одговарајућа додела, формула је незадовољива.

Како се k-САТ (општи случај) може свести на 3-САТ, а за 3-САТ се може доказати[тражи се извор] да је НП-комплетан, он се може користити да се за друге проблеме докаже да су НП-комплетни. Ово се ради тако што се покаже на који начин се решење неког проблема може искористити да се реши 3-САТ. Пример проблема где се користи овај метод је проблем клике. Често је лакше вршити свођења са 3-САТ проблема него са САТ проблема на проблеме за које се испитује НП-комплетност.

Постоји верзија 3-САТ проблема где се захтева да је тачно једна променљива у свакој клаузи тачна, уместо барем једна. И ова верзија проблема је НП-комплетна.

Референце

[уреди | уреди извор]