2-SAT

Ще започнем по отдалеч и първо ще поговорим само за SAT задачата (SAT идва от satisfiability - удовлетворимост). SAT задачата е много проста - трябва да определим възможно ли е булева формула да бъде удовлетворена, т.е. да приеме стойност истина. Нека първо да дефинираме какво ще разбираме под булева формула. Булева формула ще наричаме формула, в която са използвани единствено булеви променливи, скоби и операциите: логическо и, логическо или и логическо отрицание. Обикновено логическото отрицание е с най-голям приоритет, а логическо или с най-малък. Променливите ще означаваме с малки латински букви (възможно е и с индекси) - \(a_1,a_2,b, \dots \), логическата операция и с \(\&\&\), логическата операция или с \(||\), а логическо отрицане на някоя променлива \(a\) с \(!a\) (както в езика C++). Възможна булева формула е следната: \((a||b||c)\&\&(!a||!b||d)\). Булевите променливи приемат само стойности истина и лъжа, като ние за краткост ще ги означаваме съответно с 1 и 0. Така предната формула е удовлетворима - например при \(a=b=d=1\) и \(c=0\). Ако разгледаме обаче формулата: \((a||b)\&\&(a||!b)\&\&(!a||b)\&\&(!a||!b)\), можем да се убедим, че е неудовлетворима.

Ние ще разглеждаме специален вид на формулите, който се нарича конюнктивна нормална форма (КНФ). Една формула е в КНФ, ако най-външните действия са само логическо и, които свързват формули, в които участват единствено променливи или логическо отрицание на променливи, свъзани с логическо или. Формулите в миналия абзац са в КНФ, а тези не са: \((!a\&\& b)||(!c)\), \((a||(b\&\& c))\&\&(!a||!b)\). На някой може да му изглежда, че се ограничаваме, като разглеждаме формулите само в КНФ, но това не е така, защото всяка формула може да се сведе до КНФ! Така например, ако имаме операцията xor, то лесно можем да се убедим, че \(a\land b\equiv(a||b)\&\&(!a||!b)\). Друг пример как можем да сведем предната формула \((a||(b\&\& c))\&\&(!a||!b)\) в КНФ е като използваме дистрибутивните закони за логическо и и логическо или: \((a||(b\&\& c))\&\&(!a||!b)\equiv\) \(((a||b)\&\&(a||c))\&\&(!a||!b)\equiv\) \((a||b)\&\&(a||c)\&\&(!a||!b)\). Подобни преобразувания показват как в повечето случаи лесно можем да превръщаме някои формули до КНФ, защото в общия случай има общ алгоритъм, от който може да се получи много дълга формула.

Обикновено при SAT задачата, когато разглеждаме дали булеви формули могат да бъдат удовлетворени, си мислим, че са в КНФ. За съжаление в общия случай това е задача от класа NP, т.е. не е известен полиномиален алгоритъм, който да я решава. Дори е една от най-известните NP задачи. Тя е даже от класа NP-пълни задачи, което ще рече, че всяка задача от класа NP може да бъде сведена за полиномиално време до SAT задачата. Нека разгледаме един много лесен частен случай: 1-SAT задачата. При нея формулите, които са свързвани с логическо и, не съдържат логическо или, т.е. съдържат само една променлива. Никоя от досега разгледаните булеви формули не е такава, такива са например: \(!a\), \(!a\&\&!b\&\& a\), \(a\&\&!b\&\&!c\). Ще казваме, че такива булеви формули са в 1-SAT форма. Лесно се вижда, че при 1-SAT задачата е тривиално да преценим кога имаме удовлетворимост или по-точно, кога нямаме. Единственият случай да не можем да удовлетворим формулата е, ако тя съдържа някоя променлива и отрицанието ѝ. В останалите случаи просто даваме стойност на променливата 1, ако участва във формулата без отрицание, и стойност 0, ако участва във формулата с отрицание. Така вторият пример от преди малко, е неудовлетворима формула, заради променливата \(a\), а третият пример е удовлетворим, само ако \(a=1\), \(b=c=0\). Тук е ясно, че този "алгоритъм" е с линейна сложност спрямо дължината на формулата, а в някои случаи би могло да е и линеен спрямо броя променливи.

Аналогично 2-SAT задачата също е частен случай на общата задача, при който формулите, които са свързани с логическо и, съдържат най-много едно логическо или, т.е. съдържат най-много по две променливи. Аналогично, ще казваме, че такива формули са в 2-SAT форма. Разбира се, всички формули които са в 1-SAT форма са и в 2-SAT форма. Формули, които са в 2-SAT форма, но не и в 1-SAT форма са например: \(a\&\&(!b||c)\), \((a||!b)\&\&(!a||b)\). В следващите точки ще опишем алгоритъм, който решава задачата за линейно време спрямо дължината на формулата. Интересно е, че тази задача е като баланс между известните решими в полиномиално време задачи и тези, за които не се знае. Ако малко усилим тази задача, получаваме задача, за която няма известно полиномиално решение. Така например 3-SAT задачата е в NP. Също така min/max 2-SAT задачата, в която търсим решение с минимален/максимален брой единици е в NP. В общия случай дори и не можем и да преброим решенията на дадена формула в 2-SAT форма за полиномиално време.

Идеята за решаване на формула в 2-SAT форма е следната. Бихме искали да знаем, когато присвоим на някоя променлива дадена стойност, то какво следва за другите променливи. Понеже най-въшното действие във формулите е логическо и, то за да е удовлетворен цялата формула, искаме всяка подформула с логическо или да бъде удовлетворена. Затова ще изразим логическото или в алтернативна форма. Ще използваме бинарната логическата операция импликация, която ще означаваме с \(\to\). Тя има следната истинна таблица:

\(a\)\(b\)\(a\to b\)
001
011
100
111

Смисълът на тази операция е като математическото следователно - искаме да кажем, че ако едно твърдение е истина (a), то друго твърдение също трябва да е истина (b). Както се вижда, при тази операция можем да получим 0, само ако първата променлива e 1, а втората е 0. Нека например имаме \(x||y\). Тогава ако \(x=1\), нямаме претенции за стойността на \(y\). Но ако \(x=0\), тогава за да удовлетворим тази формула, трябва \(y=1\). Това можем да запишем с импликация по следния начин: \(!x\to y\), което е напълно еквивалетно на началната формула \(x||y\). По-рано казахме, че искаме да знаем за всяка променлива какво следва, ако ѝ присвоим дадена стойност. Затова аналогично, ако разсъждаваме за \(y\) трябва да имаме импликацията \(!y\to x\), която също е еквивалентна на началната формула. Така тези две импликации ни описват точно какво трябва да се случи в зависимост от това какви стойности присвоим на \(x\) и \(y\). По този начин можем за всяко едно от логическите или-та да разпишем съответни импликации на това какво трябва да следва при присвояване на дадена стойност на някоя променлива. Понеже те са обединени с логическо и, то всички тези импликации трябва да са верни. Цялата тази информация най-компактно и приложимо можем да я запишем в граф, чиито върхове са променливите и техните отрицания, а ребрата са именно тези импликации. Следният интерактивен пример илюстрира как от формула, която е в 2-SAT форма, можем да получим така наречения граф на импликациите:

Нещо, което следва да уточним е следното - може да има самостоятелна променлива (или отрицание на променлива) като формула, обградена с логическо и. Ако например имаме самостоятелно променливата \(x\), това означава, че за да е удовлетворима цялата формула трябва \(x=1\). Това с импликации можем да го наложим по-следния начин: \(!x\to x\), така ако се опитаме да сложим \(x=0\) ще стигнем до противоречие. Аналогично ако имаме самостоятелно \(!x\), то ще имаме импликацията \(x\to !x\). Разсъждението преди малко показва и начина на мислене, като имаме този граф. Идеята е, че ако приемем, даден връх за правилно твърдение, то импликациите показват какво следва от него за останалите променливи. Проблем възниква, както преди малко, ако по някакъв начин стигнем до връх, който отрича началното твърдение.

Последните изречения на предната точка са основните за алгоритъма, който решава задачата. Това, което споменахме е следното. Ако БОО (...) сме приели, че връх \(x\) ще е правилно твърдение (т.е. \(x\) ще е 1) и движейки се по ребрата (импликациите), достигнем връх \(!x\), то получаваме противоречие за каква стойност трябва да има \(x\). Другият начин, когато получаваме нещо нередно е ако от връх \(x\) има път до връх \(y\) и има път и до връх \(!y\). Но в този случай можем да забележим, че това не се различава от предния случай, т.е. можем да намерим път до връх \(!x\). Наблюдението е следното, ако имаме например импликация \(a\to b\) (която съответсва на \(!a||b\) ), то имаме и импликация, която е \(!b\to!a\) - в обратната посока между отрицанията на променливите. Забележете, че това важи дори и за импликациите, които следват от една променлива, защото се получава същата импликация (например от \(x\to !x\), получаваме същото). Това означава, че като имаме път от връх \(x\) до връх \(!y\), получаваме път от връх \((!(!y)=y)\) до връх \(!x\). Така ако сглобим пътят, който имахме от връх \(x\) до връх \(y\) с този път от връх \(y\) до връх \(!x\) ще получим път от \(x\) до \(!x\) (не е нужно полученият път да е прост, но лесно бихме конструирали от него прост път). Последното, което доказахме, означава, че ако приемем връх за правилно твърдение, то той не би участвал в решението, ако има път от него до върха с обратното твърдение (казано по друг начин, ако има път от връх \(a\) до връх \(!a\), то \(a\) не може да е единица и обратното). Това ни дава и НДУ (...) кога нямаме решение - нямаме решение ако има променлива \(x\), такава че в графът на импликациите има път от връх \(x\) до връх \(!x\), както и път в обратната посока - от връх \(!x\) до връх \(x\). Това е вярно, защото ако съществуват тези два пътя, то няма валидна стойност, която да присвоим на \(x\) без да получим противоречие от импликациите. Ако няма такава променлива, то имаме поне едно решение.

Можем да преразкажем последното условие по следния начин. Дадена формула в 2-SAT форма е неудовлетворима\(\iff\) за някоя променлива \(x\) съществува цикъл в графа на импликациите между върха на \(x\) и върха на \(!x\). Това лесно може да се открие за ориентиран граф, какъвто е и графът на импликациите. Ако разглеждаме силно-свързаните му компоненти (...), то търсим дали има такава компонента, в която да се намира променлива и нейното отрицание. Следният интерактивен пример онагледява силно-свързаните компоненти на графа на импликациите за дадена формула в 2-SAT форма (едноцветните върхове са в една силно-свързана компонента):

Единствено остана да изясним един важен въпрос. Когато имаме решение как да намерим едно такова. Това не е тривиален въпрос. Има лесен начин, използвайки вече намерените силно-свързани компоненти. Стандартният алгоритъм (на Косаруджо), с който се намират, ги обхожда в топологичен ред. Нека сме ги номерирали в този ред. Нека \(a\) е номерът на компонентата на връх \(x\), а \(b\) е номерът на компонентата на връх \(!x\). Ако \(b \lt a\), то е възможно да има потенциален път между върховете \(!x\) и \(x\), но е сигурно, че няма път между тях в обратната посока. Това означава, че можем да сложим стойност истина на \(x\). В обратния случай трябва да сложим стойност лъжа на тази променлива. Следният код реализира описаният досега алгоритъм за удовлетворяване на формула в 2-SAT форма:

Някой може да се зачуди дали последният прост алгоритъм за намиране на решение, в действителност намира правилно решение. От това, което казахме досега за разсъжденията в графа на импликациите, би трябвало като фиксираме стойността на връх (променлива), то с това да се фиксират и стойностите на останалите променливи от силно-свързната компонента. Може да се забележи, че наблюдението за импликации в обратната посока, ни осигурява за всяка компонента \(C\) дуална на нея \(!C\), в която има същите променливи като в \(C\) само че с отрицания, и ребра в обратната посока (...). По този начин е гарантирано, че този алгоритъм работи по един и същ начин за всички променливи от дадена компонента, защото симетрично се попълва и дуалната компонента, и няма как да има някакво смесване.