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). Както се вижда, при тази операция можем да получим 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 форма (едноцветните върхове са в една силно-свързана компонента):

Следният код реализира проверка дали дадена формула в 2-SAT форма е удовлетворима:

Свеждането от формула до импликации може да става за линейно време спрямо дължината ѝ. Ако означим с $m$ броя импликации, то това съответства и на броя ребра в графа на импликациите. Понеже времето за намиране на силно-свързаните компоненти е линейно, то сложността за отговаряне на въпроса дали е удовлетворима формула, е $O(n+m)$. Тук обръщаме внимание на броя импликации, защото често в задачи е по-лесно директно да се моделират импликациите. В следващата точка ще се убедим, че със сложност $O(n)$ се намира и конкретно решение.

Единствено остана да изясним един важен въпрос. Когато знаем, че имаме решение - как да намерим едно такова. Това не е тривиален въпрос. Оказва се, че има лесен начин за намиране на решение, но преди да стигнем до него, ще покажем един лесен за обосноваване алгоритъм, от който следва този начин. Нека графът на импликациите има решение и вземем път между $x$ и $!x$. От вече направените разсъждения е ясно, че тогава истина трябва да сложим за $!x$, иначе ще имаме противоречие. По тази причина се вижда, че слагането на истина трябва да е процес отдолу-нагоре. Освен това, ако за един връх сложим истина, това означава, че трябва да сложим истина за всички останали върхове, до които имаме път от този връх. В частност, на всички върхове от силно-свързаната компонента на върха, трябва да сложим истина. Това означава, че във всяка компонента или всички върхове са истина, или всички са лъжа. Така можем да говорим за слагане на истина или лъжа на компонентите, от което ще разбираме слагане на съответната стойност за всеки връх от компонентите. Имаме и една интересна ситуация. Фиксирането на стойност на една компонента, винаги фиксира стойностите и в друга компонента. Това може да се забележи от факта, че за всяка компонента $C$ има дуална на нея $!C$, в която има същите променливи като в $C$ само че с отрицания, и ребра в обратната посока (...за по-добро разбиране погледнете силно-свързаните компоненти на графа на импликациите за удовлетворима формула). Този факт произтича от наблюдението за контрапозиция на импликациите (импликации в обратната посока на отрицанията на променливите). Затова фиксирането на стойността на компонента $C$, фиксира стойността и на дуалната компонента $!C$ на противоположната стойност.

Направените разсъждения ни позволяват да измислим следния лесен алгоритъм. Нека направим DFS обхождане на кондензирания граф (с върхове - силно-свързаните компоненти), като за всяка компонента преценяваме каква стойност ще сложим чак след като сме фиксирали стойностите на съседните компоненти. Условието, по което фиксираме стойност е следното. Първо проверяваме дали не сме фиксирали стойността на дуалната компонента. Ако това е така, то фиксираме текущата стойност на противоположната на дуалната. В противен случай, гледаме дали има съседна компонента със стойност лъжа. Ако има такава, то няма как да сложим истина на текущата компента, затова слагаме лъжа. Ако няма такава, то слагаме истина.

Сега остана да се убедим че описаният алгоритъм намира валидно решение. Можем да видим, че винаги когато сме сложили стойност лъжа на компонента $C$, това е дошло от фиксирането на стойност истина на дуалната компонента $!C$ в по-ранен момент (от обхождането). Нека допуснем противното. Това означава, че след минаването през съседите на $C$, все още стойността на компонентата $!C$ не е фиксирана, но има съсед на компонентата $C$ - някаква компонента $D$, на която сме сложили лъжа. Да допуснем, че лъжата на компонента $D$ е дошла отново от съсед с лъжа, продължавайки по този начин със сигурност ще достигнем компонента, която е станала лъжа, заради фиксирана в по-ранен момент истина на дуалната компонента. Нека означим тази компонента с $P$. Начина, по който стигнахме до нея, ни осигурява път от компонента $C$ до компонента $P$. Използвайки наблюдението за контрапозиция, получаваме, че в графа има път от компонента $!P$ до $!C$. Тук идва и противоречието. Понеже компонента $!C$ не е фиксирана в този момент, то няма как по-горна компонента, в случая $!P$, да е фиксирана. Използвайки доказаното свойство, получаваме лесно, че обратно - стойност истина няма как да се получи от вече фиксирана стойност лъжа на дуалната ѝ компонента. Наистина ако това, беше така за компонента $C$, то стойността лъжа на $!C$ трябваше да се е получила от вече фиксирана стойност истина на $!!C=C$, което е невъзможно. Така стойност истина на компонента, получаваме само в случая, когато всички съседи на компонентата са със стойност истина. Сега лесно можем да се убедим, че алгоритъмът е верен. Единствената грешка би могла да бъде, ако за компонента е фиксирана стойност истина, а за някой нейн съсед е фиксирана стойност лъжа. Но това няма как да стане - стойност истина на компонента означава, че няма съсед със стойност лъжа. Освен това дуалните компоненти са съгласувани по стойност, така че всичко е наред. Направените разсъждения, може да разгледате на интерактивния пример - при удовлетворима формула се намира решение и компонентите със сложена истина, се оцветяват в зелено, а тези със сложена лъжа се оцветяват в червено. Забележете, че само долните компоненти (спрямо ориентацията в кондензирания ацикличен граф) са зелени, а горните са само червени. От там именно идва и доказаното свойство на нашия алгоритъм.

Сега остана най-приятната част. Понеже кондензираният граф е ацикличен, то фиксирането става в ред обратен на топологично сортиране на компонентите. Нека номерираме компонентите в този ред. Тогава номерата на компонентите са в ред обратен на топологично сортиране. Да вземем връх $x$ и нека с $C_1$ означим номера на компонентата, в която се намира, а с $C_2$ - номера на компонентата на връх $!x$. Да допуснем, че $C_1 \lt C_2$. Това означава, че първо сме фиксирали компонентата на връх $x$. Нека допуснем, че е фиксирана стойност лъжа за компонентата $C_1$. От свойствата на алгоритъма, тази стойност лъжа трябва да е дошла от вече фиксирана стойност истина на дуалната компонента $!C_1$, която всъщност е $C_2$. Но това би означавало, че $C_2 \lt C_1$, което е противоречие с началното ни условие. Затова единствения вариант е да е фиксирана истина за компонентата, а от там и за връх и променлива $x$. Аналогично, ако $C_1 \lt C_2$, то първо сме фиксирали истина за компонентата на връх $!x$, т.е. сме фиксирали лъжа за променлива $x$. Така получаваме много лесен начин за намиране на решение - като гледаме единствено подредбата в топологична сортировка на компонентите. Тук е момента да се възползваме от това, че алгоритъма на Косаруджо, намира и номерира компонентите в ред на топологично сортиране. По тази причина ако номера на компонентата на връх $!x$ е по-малък от номера на компонентата на връх $x$ (т.е. първо фиксираме $x$), то $x$ трябва да е със стойност истина. В противен случай - със стойност лъжа. Следва код за намиране на решението на удовлетворима формула, при вече намерени номера на силно-свързаните компоненти в топологичен ред: