САТ проблем

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

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

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

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

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

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

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

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

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

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

(x₁₁ ИЛИ x₁₂ ИЛИ x₁₃) И

(x₂₁ ИЛИ x₂₂ ИЛИ x₂₃) И

(x₃₁ ИЛИ x₃₂ ИЛИ x₃₃) И ...

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

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

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

Главни чланак: 2-САТ проблем

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

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

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

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

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

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

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

E = (x₁ или ~x₂ или ~x₃) и (x₁ или x₂ или x₄)

E има две клаузе (одвојене заградама), четири литерала (x₁, x₂, x₃, x₄), и k=3 (три литерала по клаузи).

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

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

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