Жұп айнымалының қанағаттандырылуы (2-қанағаттандырылу) мәселесі

Кіріспе

Логикалық мәселе, жұптық ОР. Компьютерлік ғылымда 2 қанағаттандырылуы, 2 SAT немесе жай ғана 2SAT – айнымалыларға мәндер тағайындаудың есептеулік мәселесі, олардың әрқайсысы екі мүмкін мәнге ие, айнымалы жұптарына қатысты шектеулер жүйесін қанағаттандыру үшін. Бұл жалпы Бульдік қанағаттандырылу проблемасының ерекше жағдайы, ол екіден астам айнымалыға шектеулерді қамти алады, және әр айнымалының мәні үшін екіден астам таңдау жасауға мүмкіндік беретін шектеу қанағаттандыру проблемалары. Бірақ NP толықтығына байланысты жалпы проблемалардан айырмашылығы, 2 қанағаттандыруды көп уақытта шешуге болады. 2 қанағаттандыру проблемасының мысалдары әдетте конъюнктивті қалыпты форма (2 CNF) немесе Кром формулалары деп аталатын арнайы типтегі Буль формулалары ретінде беріледі. Сонымен қатар, олар арнайы бағытталған граф түрінде, мысалдың айнымалылары мен олардың жоқтарын графтың төбелері ретінде, ал айнымалы жұптарына шектеулерді бағытталған қабырғалар ретінде көрсететін импликациялық граф ретінде де берілуі мүмкін. Бұл екі түрдегі кіріс деректері де сызықтық уақытта, кері іздеу әдісімен немесе импликациялық графтың берік байланысқан компоненттерін пайдалану арқылы шешілуі мүмкін. Резолюция, қосымша жарамды шектеулер жасау үшін шектеулердің жұптарын біріктіру әдісі, сонымен қатар полиномиалдық уақыт шешімін береді. 2 қанағаттандыру проблемалары конъюнктивті қалыпты формадағы формулалардың полиномиалдық уақытта шешілетін екі негізгі субкластарының біреуін ұсынады; екі субкластың екіншісі – Хорн қанағаттандырылуы. 2 қанағаттандыру геометрия және визуализациялау мәселелеріне қолданылуы мүмкін, онда объектілер жиынтығының әрқайсысы екі мүмкін орналасқан жерге ие және мақсат – басқа объектілермен қабаттаспайтын әрбір объект үшін орналасқан жерді табу. Басқа қолданыстар кластерлердің диаметрлерінің қосындысын азайту үшін деректерді кластерлеуді, сыныптар мен спортты жоспарлауды және қималары туралы ақпараттан пішіндерді қалпына келтіруді қамтиды. Есептеу күрделілігі теориясында 2 қанағаттандыру NL толық проблемасының мысалын ұсынады, оны логарифмдік көлемде сақтауды пайдалану арқылы детерминисттік емес түрде шешуге болады және бұл ресурспен шектелген ең қиын проблемалардың бірі болып табылады. 2 қанағаттандыру мысалының барлық шешімдерінің жиынтығына медиандық графтың құрылымын беруге болады, бірақ осы шешімдерді санау #P толық және сондықтан полиномиалдық уақыт шешімі күтілмейді. Кездейсоқ мысалдар шешілмейтін мысалдарға өткенде кескіш фазалық өтуден өтеді, өйткені шектеулердің айнымалыларға қатынасы 1-ден асып кетеді, бұл құбылыс қанағаттандыру мәселесінің күрделі формалары үшін болжанады, бірақ дәлелденбеген. 2 қанағаттандырудың есептеу қиын нұсқасы, қанағаттандырылған шектеулердің санын барынша арттыратын шындық мәнін табу, оптималдық ерекше ойындар болжамдарына байланысты болатын жуықтау алгоритміне ие, ал басқа қиын нұсқасы, қанағаттандыратын мәнін табу, шын айнымалылардың санын азайту, параметрленген күрделілік үшін маңызды сынақ жағдайы болып табылады.

Logic problem, AND of pairwise ORs

In computer science, 2 satisfiability, 2 SAT or just 2SAT is a computational problem of assigning values to variables, each of which has two possible values, in order to satisfy a system of constraints on pairs of variables. It is a special case of the general Boolean satisfiability problem, which can involve constraints on more than two variables, and of constraint satisfaction problems, which can allow more than two choices for the value of each variable. But in contrast to those more general problems, which are NP complete, 2 satisfiability can be solved in polynomial time. Instances of the 2 satisfiability problem are typically expressed as Boolean formulas of a special type, called conjunctive normal form (2 CNF) or Krom formulas. Alternatively, they may be expressed as a special type of directed graph, the implication graph, which expresses the variables of an instance and their negations as vertices in a graph, and constraints on pairs of variables as directed edges. Both of these kinds of inputs may be solved in linear time, either by a method based on backtracking or by using the strongly connected components of the implication graph. Resolution, a method for combining pairs of constraints to make additional valid constraints, also leads to a polynomial time solution. The 2 satisfiability problems provide one of two major subclasses of the conjunctive normal form formulas that can be solved in polynomial time; the other of the two subclasses is Horn satisfiability. 2 satisfiability may be applied to geometry and visualization problems in which a collection of objects each have two potential locations and the goal is to find a placement for each object that avoids overlaps with other objects. Other applications include clustering data to minimize the sum of the diameters of the clusters, classroom and sports scheduling, and recovering shapes from information about their cross sections. In computational complexity theory, 2 satisfiability provides an example of an NL complete problem, one that can be solved non deterministically using a logarithmic amount of storage and that is among the hardest of the problems solvable in this resource bound. The set of all solutions to a 2 satisfiability instance can be given the structure of a median graph, but counting these solutions is #P complete and therefore not expected to have a polynomial time solution. Random instances undergo a sharp phase transition from solvable to unsolvable instances as the ratio of constraints to variables increases past 1, a phenomenon conjectured but unproven for more complicated forms of the satisfiability problem. A computationally difficult variation of 2 satisfiability, finding a truth assignment that maximizes the number of satisfied constraints, has an approximation algorithm whose optimality depends on the unique games conjecture, and another difficult variation, finding a satisfying assignment minimizing the number of true variables, is an important test case for parameterized complexity.

Проблемалық бейнелеулер

2-қанағаттандыру мәселесін ерекше шектелген түрі бар Бульдік өрнек арқылы сипаттауға болады. Бұл – Бульдік және операциясы арқылы біріктірілген шарттардың жиынтығы, мұнда әрбір шарт екі айнымалының немесе жоққа шығарылған айнымалылардың (Бульдік немесе операциясы) дизъюнкциясы болып табылады. Бұл формулаға кіретін айнымалылар немесе олардың жоққа шығарылуы – литералдар деп аталады. Мысалы, төмендегі формула жеті айнымалы, он бір шарт және 22 литералдан тұратын конъюнктивті қалыпты формада: 2-қанағаттандыру мәселесі – бұл формуланың барлығын шындыққа айналдыратын осы айнымалыларға шындық мәнін беруді табу. Мұндай тапсырма әрбір айнымалыны шын немесе жалған деп таңдайды, сондықтан әрбір шарттағы кем дегенде бір литерал шын болады. Жоғарыда көрсетілген өрнек үшін, мүмкін болатын қанағаттандыру тапсырмасы – барлық жеті айнымалыны шындыққа орнату. Әрбір шартта кем дегенде бір жоққа шығарылмаған айнымалы бар, сондықтан бұл тапсырма барлық шарттарды қанағаттандырады. Сонымен қатар, формула шындыққа айналуы үшін барлық айнымалыларды орнатудың 15 басқа жолы бар. Сондықтан, осы өрнекте көрсетілген 2-қанағаттандыру мысалы қанағаттандырылатын. Бұл формулалар 2 CNF формулалары деп аталады. Бұл атаудағы "2" – әрбір шарттағы литералдар санын білдіреді, ал "CNF" – конъюнктивті қалыпты форманы, дизъюнкциялардың конъюнкциясы түріндегі Бульдік өрнектің түрін білдіреді. 2-CNF формуласындағы әрбір шарт бір айнымалының немесе жоққа шығарылған айнымалының екіншісіне логикалық түрде эквивалентті. Мысалы, мысалдың екінші шартын үш теңдестірілген тәсілмен жазуға болады: Бұл операция түрлері арасындағы эквиваленттілікке байланысты, 2-қанағаттандыру мысалын импликативті қалыпты формада да жазуға болады, онда конъюнктивті қалыпты формадағы әрбір "немесе" шартын оған эквивалентті екі импликациямен алмастырамыз. 2-қанағаттандыру мысалын сипаттаудың үшінші, графикалық тәсілі – импликациялық граф. Импликациялық граф – бағытталған граф, онда әрбір айнымалы немесе жоққа шығарылған айнымалы үшін бір төбе болады және сәйкес айнымалылар мысалдың импликативті қалыпты түрінде импликация арқылы байланысты болған кезде бір төбеден екіншісіне жиек жалғанады. Импликациялық граф қисық симметриялық граф болуы керек, яғни, ол әрбір айнымалыны оның жоққа шығарылуына жіберу және барлық жиектердің бағытын кері қайтару симметриясына ие.

A 2 satisfiability problem may be described using a Boolean expression with a special restricted form. It is a conjunction (a Boolean and operation) of clauses, where each clause is a disjunction (a Boolean or operation) of two variables or negated variables. The variables or their negations appearing in this formula are known as literals. For example, the following formula is in conjunctive normal form, with seven variables, eleven clauses, and 22 literals:

The 2 satisfiability problem is to find a truth assignment to these variables that makes the whole formula true. Such an assignment chooses whether to make each of the variables true or false, so that at least one literal in every clause becomes true. For the expression shown above, one possible satisfying assignment is the one that sets all seven of the variables to true. Every clause has at least one non negated variable, so this assignment satisfies every clause. There are also 15 other ways of setting all the variables so that the formula becomes true. Therefore, the 2 satisfiability instance represented by this expression is satisfiable. Formulas in this form are known as 2 CNF formulas. The "2" in this name stands for the number of literals per clause, and "CNF" stands for conjunctive normal form, a type of Boolean expression in the form of a conjunction of disjunctions. Each clause in a 2 CNF formula is logically equivalent to an implication from one variable or negated variable to the other. For example, the second clause in the example may be written in any of three equivalent ways:

Because of this equivalence between these different types of operation, a 2 satisfiability instance may also be written in implicative normal form, in which we replace each or clause in the conjunctive normal form by the two implications to which it is equivalent. A third, more graphical way of describing a 2 satisfiability instance is as an implication graph. An implication graph is a directed graph in which there is one vertex per variable or negated variable, and an edge connecting one vertex to another whenever the corresponding variables are related by an implication in the implicative normal form of the instance. An implication graph must be a skew symmetric graph, meaning that it has a symmetry that takes each variable to its negation and reverses the orientations of all of the edges.

Алгоритмдер

2-қанағаттандыру мәселесін шешу үшін бірнеше алгоритм белгілі. Олардың ең тиімділері сызықты уақыт алады.

Шектелген кері қайтару

бинарлық айнымалылармен және жұптық шектеулермен шектеулерді қанағаттандыру мәселелерін шешу үшін шектеулі кері қайтаруды қолданатын әдісті сипаттаңыз. Олар бұл әдісті сынып кестесін құру мәселесіне қолданады, бірақ оны басқа мәселелерге де, соның ішінде 2 SAT-қа да қолданатынын байқайды. Олардың негізгі идеясы – бір уақытта бір айнымалыны бөліп, жартылай шындық мәнін құру. Алгоритмнің кейбір қадамдары «шешім нүктелері» болып табылады, онда айнымалыға екі түрлі шындық мәнінің біреуін беруге болады, ал алгоритмнің кейінгі қадамдары оны осы шешім нүктелерінің біріне кері қайтаруға әкелуі мүмкін. Дегенмен, тек соңғы таңдалған мәнге ғана кері қайтаруға болады. Соңғыдан бұрын жасалған барлық шешімдер өзгеріссіз қалады. Және жол негізіндегі күшті компоненттер алгоритмі әрқайсысы бір тереңдікке дейін іздеуді орындайды. Косаражу алгоритмі екі тереңдікке дейін іздеуді жүргізеді, бірақ өте қарапайым. Импликациялық граф бойынша екі литераль бір-бірімен күшті байланысты компонентке жатады, егер бір литеральден екіншісіне және керісінше импликациялардың тізбегі болса. Сондықтан, екі литеральдың берілген 2 қанағаттандыру инстанциясына кез келген қанағаттандырарлық тапсырмада бірдей мәні болуы тиіс. Атап айтқанда, егер айнымалы мен оның терістігі бір-бірімен күшті байланысты компонентке жатса, инстанцияны қанағаттандыру мүмкін емес, өйткені бұл екі литеральді бірдей мәнге жатқызу мүмкін емес. Aspvall және басқалар көрсеткендей, бұл қажетті және жеткілікті шарт: 2 CNF формуласы қанағаттандырылатындығы, егер және тек егер оның теріске шығаруы сияқты күшті байланысты компонентке жататын айнымалы болмаса. Кері топологиялық реттің әрбір компоненті үшін, егер оның айнымалылары шындық мәніне ие болмаса, компоненттегі барлық литеральдарды шындық деп қойыңыз. Бұл сонымен қатар толықтыратын компоненттегі барлық литеральдардың жалған деп орнатылуына әкеледі. Кері топологиялық ретке келтіру және қисық симметрияға байланысты, литераль шындыққа орнатылған кезде, одан импликациялар тізбегі арқылы қол жетімді барлық литеральдар шындыққа орнатылады. Симметриялы түрде, x литералін жалған деп белгілегенде, оған алып келетін барлық литеральдер де жалған деп белгіленеді. Сондықтан, осы рәсіммен құрылған шындық мәні берілген формулаға сәйкес келеді, бұл сонымен қатар Aspvall және басқалар анықтаған қажетті және жеткілікті шарттың дұрыстығын дәлелдеуді толықтырады. картаны таңбалау мәселесін сипаттаңыз, онда әрбір таңба – тік төртбұрыш, оны таңбалаған сызық сегментіне қатысты үш позицияның біріне орналастыруға болады: ол сегментті бір қабырғасы ретінде қамтуы мүмкін немесе сегментке ортақталуы мүмкін. Олар осы үш позицияны екі екілік айнымалыны қолдана отырып, жарамды таңбалаудың бар-жоғын тексеруді 2 қанағаттандыру мәселесіне айналдырады. Берілген нүктелер жиынтығы үшін мүмкіндігінше үлкен өлшемді тік төртбұрышты таңбаларды табу мәселесі үшін 2 қанағаттандыру, әрбір таңбаның бір бұрышы таңбаланған нүктеде болуы деген шектеумен, шамалау алгоритмінің бөлігі ретінде қолданылады. Берілген өлшемдегі таңбалауды табу үшін, егер екі еселенгенде басқа нүктемен жапсарласқан тік төртбұрыштарды алып тастайды, және басқа нүктелердің таңбасымен жапсарласпайтын жолмен таңбалана алатын нүктелерді алып тастайды. Олар осы жою ережелері қалған нүктелердің нүктеге тек екі таңба орналастыру мүмкіндігіне ие екенін көрсетеді, бұл 2 қанағаттандыру инстанциясының шешімі ретінде жарамды таңба орналастыруды (егер ол бар болса) табуға мүмкіндік береді. 2 қанағаттандыру инстанциясын шешуге әкелетін ең үлкен таңба өлшемін іздеу арқылы олар таңбалары оңтайлы шешімнің кем дегенде жартысы мөлшерінде болатын жарамды таңба орналастыруды табады. Яғни, олардың алгоритмінің шамалас қатынасы ең көп дегенде екі. Сол сияқты, егер әрбір таңба тікбұрышты болып, таңбалау нүктесі оның төменгі жиегі бойымен орналасуы керек болса, онда 2 қанағаттандыруды пайдалану ең үлкен таңба өлшемін табу үшін, онда әрбір таңбалау нүктесі төменгі бұрышта болса, бұл ең көп дегенде екіге жуық қатынасқа әкеледі. 2 қанағаттандырудың ұқсас қолданбалары басқа геометриялық орналастыру мәселелеріне де қолданылған. Егер графиктік сызбада нүктелердің орналасуы белгіленсе және әрбір жиек екі ықтимал орынның бірімен (мысалы, доғалық диаграмма ретінде) дөңгелек доға ретінде тартылуы керек болса, онда қиылысудан аулақ болу үшін әрбір жиек үшін қай доғаны пайдалану мәселесі, әрбір жиек үшін айнымалысы және қиылысқа әкелетін орналастыру жұбы үшін шектеуі бар 2 қанағаттандыру мәселесі болып табылады. Дегенмен, бұл жағдайда импликациялық графтың нақты бейнесін құру және іздеуге қарағанда, графты жасырын түрде іздеу арқылы шешімді жылдамдатуға болады. VLSI интегралдық схеманы жобалауда, егер модульдер жиынтығын сымдармен қосу керек болса, олардың әрқайсысы бір рет қана иілуге болатын болса, сымдар үшін екі мүмкін бағыт бар, және барлық сымдарды схеманың бір қабатында маршруттап беруге болатындай етіп, осы екі бағыттың қайсысын пайдалану мәселесі 2 қанағаттандыру инстанциясы ретінде шешіледі. басқа VLSI жобалау мәселесін қарастырыңыз: схема жобасындағы әрбір модульді айнаға көшіру керек пе, әлде керісінше, әлде керісінше. Бұл айнаға көшіру модульдің операцияларын өзгеріспейді, бірақ модульдің кіріс және шығыс сигналдарының модульге қосылатын нүктелерінің ретін өзгертеді, бұл модульдің қалған бөлікке қаншалықты жақсы сәйкес келетінін өзгертеді. Boros және басқалар модульдердің тік сызықты каналға орналасқан, сымдар модульдер арасында маршрутталған және каналдың тығыздығына белгілі шектеу бар (каналдың кез келген қимасынан өтуі керек сигналдардың максималды саны) мәселенің жеңілдетілген нұсқасын қарастырады. Олар бұл мәселенің нұсқасын 2 қанағаттандыру инстанциясы ретінде шешуге болатынын байқайды, онда шектеулер бір-біріне қарама-қарсы каналда орналасқан модульдер жұбының бағдарларын байланыстырады. Салдарынан, оңтайлы тығыздық осылайша тиімді есептелуі мүмкін, екілік іздеуді орындау арқылы, әр қадамда 2 қанағаттандыру инстанциясын шешуді қамтиды.

describe a technique involving limited backtracking for solving constraint satisfaction problems with binary variables and pairwise constraints. They apply this technique to a problem of classroom scheduling, but they also observe that it applies to other problems including 2 SAT. The basic idea of their approach is to build a partial truth assignment, one variable at a time. Certain steps of the algorithms are "choice points", points at which a variable can be given either of two different truth values, and later steps in the algorithm may cause it to backtrack to one of these choice points. However, only the most recent choice can be backtracked over. All choices made earlier than the most recent one are permanent. and the path based strong component algorithm each perform a single depth first search. Kosaraju's algorithm performs two depth first searches, but is very simple. In terms of the implication graph, two literals belong to the same strongly connected component whenever there exist chains of implications from one literal to the other and vice versa. Therefore, the two literals must have the same value in any satisfying assignment to the given 2 satisfiability instance. In particular, if a variable and its negation both belong to the same strongly connected component, the instance cannot be satisfied, because it is impossible to assign both of these literals the same value. As Aspvall et al. showed, this is a necessary and sufficient condition: a 2 CNF formula is satisfiable if and only if there is no variable that belongs to the same strongly connected component as its negation. For each component in the reverse topological order, if its variables do not already have truth assignments, set all the literals in the component to be true. This also causes all of the literals in the complementary component to be set to false. Due to the reverse topological ordering and the skew symmetry, when a literal is set to true, all literals that can be reached from it via a chain of implications will already have been set to true. Symmetrically, when a literal x is set to false, all literals that lead to it via a chain of implications will themselves already have been set to false. Therefore, the truth assignment constructed by this procedure satisfies the given formula, which also completes the proof of correctness of the necessary and sufficient condition identified by Aspvall et al. describe a map labeling problem in which each label is a rectangle that may be placed in one of three positions with respect to a line segment that it labels: it may have the segment as one of its sides, or it may be centered on the segment. They represent these three positions using two binary variables in such a way that, again, testing the existence of a valid labeling becomes a 2 satisfiability problem. use 2 satisfiability as part of an approximation algorithm for the problem of finding square labels of the largest possible size for a given set of points, with the constraint that each label has one of its corners on the point that it labels. To find a labeling with a given size, they eliminate squares that, if doubled, would overlap another point, and they eliminate points that can be labeled in a way that cannot possibly overlap with another point's label. They show that these elimination rules cause the remaining points to have only two possible label placements per point, allowing a valid label placement (if one exists) to be found as the solution to a 2 satisfiability instance. By searching for the largest label size that leads to a solvable 2 satisfiability instance, they find a valid label placement whose labels are at least half as large as the optimal solution. That is, the approximation ratio of their algorithm is at most two. Similarly, if each label is rectangular and must be placed in such a way that the point it labels is somewhere along its bottom edge, then using 2 satisfiability to find the largest label size for which there is a solution in which each label has the point on a bottom corner leads to an approximation ratio of at most two. Similar applications of 2 satisfiability have been made for other geometric placement problems. In graph drawing, if the vertex locations are fixed and each edge must be drawn as a circular arc with one of two possible locations (for instance as an arc diagram), then the problem of choosing which arc to use for each edge in order to avoid crossings is a 2 satisfiability problem with a variable for each edge and a constraint for each pair of placements that would lead to a crossing. However, in this case it is possible to speed up the solution, compared to an algorithm that builds and then searches an explicit representation of the implication graph, by searching the graph implicitly. In VLSI integrated circuit design, if a collection of modules must be connected by wires that can each bend at most once, then again there are two possible routes for the wires, and the problem of choosing which of these two routes to use, in such a way that all wires can be routed in a single layer of the circuit, can be solved as a 2 satisfiability instance. consider another VLSI design problem: the question of whether or not to mirror reverse each module in a circuit design. This mirror reversal leaves the module's operations unchanged, but it changes the order of the points at which the input and output signals of the module connect to it, possibly changing how well the module fits into the rest of the design. Boros et al. consider a simplified version of the problem in which the modules have already been placed along a single linear channel, in which the wires between modules must be routed, and there is a fixed bound on the density of the channel (the maximum number of signals that must pass through any cross section of the channel). They observe that this version of the problem may be solved as a 2 satisfiability instance, in which the constraints relate the orientations of pairs of modules that are directly across the channel from each other. As a consequence, the optimal density may also be calculated efficiently, by performing a binary search in which each step involves the solution of a 2 satisfiability instance.

Деректерді кластерлеу

Метрикалық кеңістіктегі дерек нүктелерінің жиынтығын екі кластерге топтастырудың бір жолы – кластерлердің диаметрлерінің қосындысын ең төмендету үшін кластерлерді таңдау, мұнда әрбір кластердің диаметрі оның кез келген екі нүктесі арасындағы ең үлкен қашықтық болып табылады. Бұл кластердің максималды мөлшерін ең төмендетуге қарағанда жақсырақ, себебі соңғысы өте ұқсас нүктелердің әртүрлі кластерлерге жіберілуіне алып келуі мүмкін. Егер екі кластердің мақсатты диаметрлері белгілі болса, онда осы мақсаттарға жететін кластерлеуді 2-қанағаттандыру (2-satisfiability) инстанциясын шешу арқылы табуға болады. Инстанцияда әрбір нүкте үшін бір айнымалы болады, ол осы нүкте бірінші кластерге, немесе екінші кластерге жататынын көрсетеді. Егер екі нүкте бір-бірінен тым алыс болса, олардың екеуі де бір кластерге жата алмайды, сондықтан инстанцияға осы шартты сақтамайтын жағдайды болдырмайтын клауза қосылады. Бұл әдіс жеке кластерлердің диаметрлері белгісіз болғанда да қолданылуы мүмкін, яғни қосалқы процедура ретінде пайдаланылуы мүмкін. Диаметрлердің белгілі бір қосындысына қол жеткізуге болатынын, жеке кластерлердің диаметрлерін білмей тексеру үшін, берілген қосындыдан аспайтын мақсатты диаметрлердің барлық мүмкін жұптарын қарастыруға болады. Әрбір жұп диаметрді 2-қанағаттандыру инстанциясы ретінде бейнелей отырып, осы жұпты кластерлеу арқылы жүзеге асыруға болатынын анықтау үшін 2-қанағаттандыру алгоритмін қолдануға болады. Диаметрлердің оңтайлы қосындысын табу үшін, әрбір қадамы осы типтегі мүмкіншілік тесті болатын екілік іздеуді (binary search) жүзеге асыруға болады. Осы тәсіл кластер диаметрлерінің қосындысынан басқа да комбинацияларды оңтайландыруға мүмкіндік береді, сондай-ақ кластердің мөлшерін өлшеу үшін метрикалық кеңістіктегі қашықтықтардың орнына кез келген ұқсамаушылық сандарын (dissimilarity numbers) қолдануға болады. Бұл алгоритмнің жұмыс уақыты 2-қанағаттандыру инстанцияларының тізбесін шешуге кеткен уақытпен анықталады, бұл инстанциялар бір-бірімен тығыз байланысты. Алгоритм осы байланысты инстанцияларды бір-бірінен тәуелсіз шешуге қарағанда жылдамырақ шешуге қалай болатынын көрсетеді, нәтижесінде диаметрлер қосындысы кластерлеу мәселесі үшін O(n³) жалпы жұмыс уақыты шығады.

One way of clustering a set of data points in a metric space into two clusters is to choose the clusters in such a way as to minimize the sum of the diameters of the clusters, where the diameter of any single cluster is the largest distance between any two of its points. This is preferable to minimizing the maximum cluster size, which may lead to very similar points being assigned to different clusters. If the target diameters of the two clusters are known, a clustering that achieves those targets may be found by solving a 2 satisfiability instance. The instance has one variable per point, indicating whether that point belongs to the first cluster or the second cluster. Whenever any two points are too far apart from each other for both to belong to the same cluster, a clause is added to the instance that prevents this assignment. The same method also can be used as a subroutine when the individual cluster diameters are unknown. To test whether a given sum of diameters can be achieved without knowing the individual cluster diameters, one may try all maximal pairs of target diameters that add up to at most the given sum, representing each pair of diameters as a 2 satisfiability instance and using a 2 satisfiability algorithm to determine whether that pair can be realized by a clustering. To find the optimal sum of diameters one may perform a binary search in which each step is a feasibility test of this type. The same approach also works to find clusterings that optimize other combinations than sums of the cluster diameters, and that use arbitrary dissimilarity numbers (rather than distances in a metric space) to measure the size of a cluster. The time bound for this algorithm is dominated by the time to solve a sequence of 2 satisfiability instances that are closely related to each other, and shows how to solve these related instances more quickly than if they were solved independently from each other, leading to a total time bound of O(n^(3)) for the sum of diameters clustering problem.

Жоспарлау

Сабақ кестесін құрудың үлгісін қарастырайық, онда n мұғалімнің әрқайсысы m студенттік топтарға сабақ беруі керек. Мұғалімнің әрбір топпен аптасына өткізетін сағаттарының саны кіріс ретінде берілген матрицаның элементтері арқылы сипатталады, сондай-ақ әр мұғалімнің кестеге жазылу үшін қолжетімді сағаттары бар. Олар көрсеткендей, тіпті әр мұғалімде ең көп үш сағат болған жағдайда да, мәселе NP-толық болып табылады, бірақ әр мұғалімде тек екі сағат болса, оны 2-қанағаттандырудың бір мысалы ретінде шешуге болады. (Тек бір сағаты бос мұғалімдерді мәселеден оңай шығарып тастауға болады.) Бұл мәселеде әрбір айнымалы мұғалімнің белгілі бір топпен өткізетін сағатына сәйкес келеді, айнымалыға берілген мән сол сағаттың мұғалімнің қолжетімді сағаттарының біріншісі ме, екіншісі ме екенін көрсетеді, және екі түрлі қақтығыстың кез келгенін болдырмайтын 2-қанағаттандыру шарты бар: бір мұғалімге бір уақытта екі топ немесе бір топқа бір уақытта екі мұғалім тағайындалған.

Дискретті томография

Томография – нысандардың қималарынан олардың пішінін қалпына келтіру процесі. Дискретті томографияда, жиі зерттелетін проблеманың қарапайымдалған түрінде, қалпына келтірілетін пішін полиомино (екі өлшемді квадраттық тордағы квадраттардың ішкі жиыны) болып табылады, ал қималар тордың жеке қатарлары мен бағандарындағы квадраттар жиынтығы туралы жиынтық ақпаратты ұсынады. Мысалы, танымал нонограмм жұмбақтарында, сондай-ақ сандар бойынша бояу немесе гридлерде, анықталуға тиіс квадраттар жиынтығы екілік кескіндегі қара пиксельдерді көрсетеді, ал жұмбақты шешушіге берілген ақпарат әрбір қатарда немесе бағанда қанша қара пиксель блогын қосу керектігін және осы блоктардың әрқайсысының ұзындығын көрсетеді. Цифрлық томографияның басқа түрлерінде әр қатар немесе баған туралы ақпарат одан да аз беріледі: тек квадраттардың жалпы саны, ал квадраттардың блоктары мен ұзындығы емес. Мәселенің эквивалентті түрі – берілген 0-1 матрицаны, тек матрицаның әрбір қатары мен бағанындағы мәндердің қосындысы бойынша қалпына келтіру. Матрицаны табуға полиномиалдық уақыт алгоритмдері бар болғанымен, шешім бірегей болмауы мүмкін: 2x2 бірлік матрицасы түріндегі кез келген кіші матрицаны шешімнің дұрыстығына әсер етпей толықтыруға болады. Сондықтан зерттеушілер қалпына келтірілетін пішінге шектеулер іздестірді, олар шешімдер кеңістігін шектеуге пайдаланылуы мүмкін. Мысалы, пішін байланысты деп болжауға болады; алайда, байланысқан шешімнің бар-жоғын тексеру NP-толық мәселе. Одан да оңай шешілетін нұсқасы – пішін ортогоналды түрде дөңгелек: әрбір қатарда және бағанда бір-бірімен жалғасқан квадраттар блогы бар. Бірнеше бұрынғы шешімдерді жақсартып, 2-SAT қолдану арқылы, байланысқан ортогоналды дөңгелек пішіндерді тиімді қалпына келтіруді көрсетті. Олардың шешімінің идеясы – қалпына келтірілетін пішіннің ең сол және ең оң жасушаларын қамтитын қатарлардың индекстерін болжау, содан кейін осы болжаулармен және берілген қатарлар мен бағандардың қосындысымен сәйкес келетін пішіннің бар-жоғын тексертін 2-қанағаттандыру мәселесін құру. Олар берілген пішіннің бөлігі болуы мүмкін әрбір квадрат үшін төрт 2-қанағаттандыру айнымалысын қолданады, олардың бірі оның пішіннің төрт мүмкін «бұрыш аймақтарының» біріне жататынын көрсетеді, және осы аймақтардың ажыратылуын қамтамасыз ететін шектеулерді қолданады, қажетті пішіндерге ие болу, жалғасқан қатарлар мен бағандардан тұратын жалпы пішін құру және қажетті қатарлар мен бағандардың қосындысына ие болу. Олардың алгоритмі O(m³n) уақыт алады, мұнда m – кіші өлшем, n – үлкен өлшем. Кейіннен сол әдіс ортогоналды байланысты талап етпей, тек диагональды байланыста болатын ортогоналды дөңгелек пішіндерге де қолданылды. Толық нонограмм жұмбақтарын шешуге арналған шешуші құралдың бір бөлігі ретінде, бірнеше басқа эвристикалардан алынған ақпаратты біріктіру үшін 2-қанағаттандыру қолданылды. Ойынның ішінара шешімін тапқаннан кейін, олар әрбір қатардың немесе бағанның динамикалық бағдарламалауын қолданып, сол қатардың немесе бағанның шектеулері оның кез келген квадратын ақ немесе қара болуға мәжбүрлейтінін, және бір қатардағы немесе бағандағы кез келген екі квадратты импликациялық қатынаспен байланыстыруға болатынын анықтайды. Олар сондай-ақ нонограмды цифрлық томография мәселесіне айналдырады, әрбір қатар мен бағандағы блок ұзындығының тізбегін оның қосындысымен алмастырады және осы цифрлық томография мәселесінің барлық қатарлар мен бағандарды біріктіретін кез келген квадратының күйін анықтауға болатынын немесе квадраттардың жұптарын импликациялық қатынаспен байланыстыруға болатынын анықтау үшін максималды ағын формуласын қолданады. Егер осы екі эвристиканың бірі квадраттардың бірінің мәнін анықтаса, ол ішінара шешімге қосылады және бірдей есептеулер қайталанады. Алайда, егер екі эвристика да кез келген квадраттарды орнатпаса, олардың екеуі де тапқан импликациялар 2-қанағаттандыру мәселесіне біріктіріледі және мәселемен белгіленген квадраттарды табу үшін 2-қанағаттандыру шешушісі қолданылады, содан кейін процедура қайтадан қайталанады. Бұл процедура шешім табуға жетуі мүмкін немесе мүмкін емес, бірақ ол полиномиалдық уақытта орындалуы кепілдік беріледі. Бетенбург пен Костерс хабарлағандай, газеттегі көптеген жұмбақтар оның толық қуатын қажет етпесе де, бұл процедура және осы 2-қанағаттандыру әдісін шектеулі кері ізденумен біріктіретін, бірақ баяурақ процедура да қолданылады.

Tomography is the process of recovering shapes from their cross sections. In discrete tomography, a simplified version of the problem that has been frequently studied, the shape to be recovered is a polyomino (a subset of the squares in the two dimensional square lattice), and the cross sections provide aggregate information about the sets of squares in individual rows and columns of the lattice. For instance, in the popular nonogram puzzles, also known as paint by numbers or griddlers, the set of squares to be determined represents the dark pixels in a binary image, and the input given to the puzzle solver tells him or her how many consecutive blocks of dark pixels to include in each row or column of the image, and how long each of those blocks should be. In other forms of digital tomography, even less information about each row or column is given: only the total number of squares, rather than the number and length of the blocks of squares. An equivalent version of the problem is that we must recover a given 0 1 matrix given only the sums of the values in each row and in each column of the matrix. Although there exist polynomial time algorithms to find a matrix having given row and column sums, the solution may be far from unique: any submatrix in the form of a 2 × 2 identity matrix can be complemented without affecting the correctness of the solution. Therefore, researchers have searched for constraints on the shape to be reconstructed that can be used to restrict the space of solutions. For instance, one might assume that the shape is connected; however, testing whether there exists a connected solution is NP complete. An even more constrained version that is easier to solve is that the shape is orthogonally convex: having a single contiguous block of squares in each row and column. Improving several previous solutions, showed how to reconstruct connected orthogonally convex shapes efficiently, using 2 SAT. The idea of their solution is to guess the indexes of rows containing the leftmost and rightmost cells of the shape to be reconstructed, and then to set up a 2 satisfiability problem that tests whether there exists a shape consistent with these guesses and with the given row and column sums. They use four 2 satisfiability variables for each square that might be part of the given shape, one to indicate whether it belongs to each of four possible "corner regions" of the shape, and they use constraints that force these regions to be disjoint, to have the desired shapes, to form an overall shape with contiguous rows and columns, and to have the desired row and column sums. Their algorithm takes time O(m^(3)n) where m is the smaller of the two dimensions of the input shape and n is the larger of the two dimensions. The same method was later extended to orthogonally convex shapes that might be connected only diagonally instead of requiring orthogonal connectivity. A part of a solver for full nonogram puzzles, used 2 satisfiability to combine information obtained from several other heuristics. Given a partial solution to the puzzle, they use dynamic programming within each row or column to determine whether the constraints of that row or column force any of its squares to be white or black, and whether any two squares in the same row or column can be connected by an implication relation. They also transform the nonogram into a digital tomography problem by replacing the sequence of block lengths in each row and column by its sum, and use a maximum flow formulation to determine whether this digital tomography problem combining all of the rows and columns has any squares whose state can be determined or pairs of squares that can be connected by an implication relation. If either of these two heuristics determines the value of one of the squares, it is included in the partial solution and the same calculations are repeated. However, if both heuristics fail to set any squares, the implications found by both of them are combined into a 2 satisfiability problem and a 2 satisfiability solver is used to find squares whose value is fixed by the problem, after which the procedure is again repeated. This procedure may or may not succeed in finding a solution, but it is guaranteed to run in polynomial time. Batenburg and Kosters report that, although most newspaper puzzles do not need its full power, both this procedure and a more powerful but slower procedure which combines this 2 satisfiability approach with the limited backtracking of

Қайта аталатын мүйіздің қанағаттанушылығы

2-қанағаттандырылғандықтан кейін, полиномиалдық уақытта шешілетін қанағаттандырылғандық проблемаларының тағы бір маңызды кіші классы – Хорн қанағаттандырылғандығы. Бұл қанағаттандырылғандық проблемалары класында кіріс қайтадан конъюнктивті нормалық формадағы формула болып табылады. Әрбір клауда кез келген саны литералдар болуы мүмкін, бірақ оң литералдардың саны ең көп дегенде біреу болуы керек. Осы кластың жалпылама нұсқасы – қайта аттауға болатын Хорн қанағаттандырылғандығы табылған, оны қосалқы 2-қанағаттандырылғандық мысалы арқылы полиномиалдық уақытта шешуге болады. Егер формуланың кейбір айнымалыларын олардың инверсияларымен алмастыру арқылы Хорн формасына келтіруге болады, онда ол қайта аттауға болатын Хорн формуласы деп аталады. Мұны істеу үшін Льюис қайта аттауға болатын Хорн мысалының әрбір айнымалысы үшін бір айнымалыдан тұратын 2-қанағаттандырылғандық мысалын құрады, онда 2-қанағаттандырылғандық айнымалылары сәйкес қайта аттауға болатын Хорн айнымалыларын инверсиялау қажеттігін немесе қажет еместігін көрсетеді. Хорн мысалын алу үшін, қайта аттауға болатын Хорн мысалының бір клаузасында пайда болатын екі айнымалы сол клауда оң литерал ретінде пайда болмауы керек; айнымалылар жұбына қатысты бұл шектеу 2-қанағаттандырылғандық шектеуі болып табылады. Нәтижесінде алынған 2-қанағаттандырылғандық мысалына қанағаттандырарлық тапсырманы тауып, Льюис кез келген қайта аттауға болатын Хорн мысалын полиномиалдық уақытта Хорн мысалына қалай айналдыруға болатынын көрсетеді. Ұзын клаузаларды бірнеше кішкентай клаузаларға бөліп, сызықтық уақытты 2-қанағаттандырылғандық алгоритмін қолдану арқылы, оны сызықтық уақытқа дейін қысқартуға болады.

Басқа қолданбалар

2 қанағаттандырушылық сонымен қатар тәуелсіз жиынтыққа және кішкентай сандағы толық екі жақты кішкентай графтарға бөлінетін бағытталмаған графтарды тану, интернеттің автономды жүйелері арасындағы бизнес қатынастарды анықтау және эволюциялық ағаштарды қайта құру сияқты мәселелерде қолданылды.

NL-толықтығы

2-қанағаттандырылатын инстанцияның қанағаттандырылмайтынын анықтау үшін нондетерминистік алгоритмді сипаттау оңай: жай ғана (нондетерминистік) v айнымалысын таңдап, (нондетерминистік) v-ден оның жоқтығына және содан кейін v-ге қайта әкелетін салдарлар тізбегін іздеңіз. Егер мұндай тізбек табылса, инстанция қанағаттандырылмайды. Immerman–Szelepcsényi теоремасы бойынша, нондетерминистік логикалық кеңістікте қанағаттандырылатын 2-қанағаттандырылатын инстанцияның қанағаттандырылатындығын тексеру де мүмкін. 2-қанағаттандырылатындық NL-толық, яғни ол логарифмдік кеңістікте нондетерминистік түрде шешілетін мәселелердің NL күрделілік класындағы «ең қиын» немесе «ең көрнекті» мәселелердің бірі. Мұндағы толықтық – логарифмдік кеңістікті пайдаланатын детерминистік Тьюринг машинасы NL-дегі кез келген басқа мәселені 2-қанағаттандырылатын мәселеге айналдыра алады дегенді білдіреді. NP күрделілік класы үшін белгілі нәтижелерге ұқсас, бұл түрлендіру Immerman–Szelepcsényi теоремасымен бірге NL-дегі кез келген мәселені жалғыз экзистенциалды сандық предикатпен және ұзындығы 2-ге дейін шектелген клаузалармен екінші реттік логикалық формула ретінде көрсетуге мүмкіндік береді. Мұндай формулалар SO Krom деп аталады. Сол сияқты, импликативті қалыпты форманы транзитивті жабу операторын қосу арқылы бірінші реттік логикада дамытуға болады. Белгілі бір 2-қанағаттандырылатын инстанцияның барлық шешімдерін тиімді тізімдеу және бірнеше байланысты мәселелерді шешу үшін алгоритмді сипаттайды. Сондай-ақ, бір-бірінен максималды Хамминг қашықтығы бар екі қанағаттандыратын тапсырманы табуға арналған алгоритмдер де бар.

Қанағаттандырарлық тапсырмалардың санын есептеу

#2SAT – берілген 2 CNF формуласына қанағаттандыратын тапсырмалардың санын есептеу мәселесі. Бұл есептеу мәселесі #P толық, яғни P = NP болмаса, оны полиномиалдық уақытта шешу мүмкін емес. Сонымен қатар, егер NP = RP болмаса, #2SAT үшін толық полиномиалдық кездейсоқ жуықтау схемасы жоқ, тіпті кіріс монотонды 2 CNF формулаларымен, яғни әрқайсысы айнымалының оң түрінде болатын 2 CNF формулаларымен шектелген жағдайда да. 2SAT формуласына қанағаттандыратын тапсырмалардың нақты санын есептеуге арналған ең жылдам алгоритм уақытта жұмыс істейді.

Кездейсоқ 2-қанағаттандырарлық инстанциялар

Кездейсоқ 2-қанағаттандырылатын мысал n айнымалы және m түйін үшін, барлық мүмкін екі айнымалы түйіндер жиынынан әрбір түйін біркелкі түрде кездейсоқ таңдалып алыну арқылы құрастырылуы мүмкін. m саны n санына қарағанда кішкентай болса, мұндай мысал қанағаттандырылатын болуы мүмкін, бірақ m санының үлкендеуі қанағаттандырылу ықтималдығын азайтады. Нақтырақ айтқанда, егер m/n тұрақты α ≠ 1 ретінде белгіленсе, n шексізге ұмтылғанда қанағаттандырылу ықтималдығы белгілі бір шекке жетеді: егер α < 1 болса, онда шек бірге тең, ал егер α > 1 болса, онда шек нөлге тең. Осылайша, бұл мәселе α = 1 кезінде фазалық өтуді көрсетеді.

2-қанағаттандырарлық деңгей

Максималды 2 қанағаттандыру мәселесінде (MAX 2 SAT) кіріс – әрбір клаузада екі литераль болатын конъюнктивті нормалық формадағы формула, ал міндет – бір тағайындама арқылы бір уақытта қанағаттандырылатын клаузалардың максималды санын анықтау. Жалпылама максималды қанағаттандыру мәселесі сияқты, MAX 2 SAT NP-қиын. Дәлел 3SAT-тен азайту арқылы жүзеге асырылады. MAX 2 SAT-ты кесім табу мәселесі ретінде (яғни, төбелерді екі ішкі жиынға бөлу) қарастырып, бірінші ішкі жиынның бір ұшы мен екіншісінің бір ұшында болатын қабырғалар санын барынша арттыру арқылы, импликациялық графқа байланысты граф ішінде және жартылай анық бағдарламалау әдістерін қолдану арқылы, полиномиалдық уақытта оптималды санды кем дегенде 0,940 есеге қанағаттандыратын жуық шешім табуға болады. Теңгерілген MAX 2 SAT мысалы – MAX 2 SAT мысалы, онда әрбір айнымалы оң және теріс пішімде бірдей салмақта болады. Бұл мәселе үшін Острин жуықтау коэффициентін жақсартты. Егер бірегей ойындар туралы болжам дұрыс болса, онда MAX 2 SAT-ты, теңгерілген немесе теңгерілмегенін, полиномиалдық уақытта 0,943-тен жақсы жуықтау тұрақтысымен жуықтау мүмкін емес. P ≠ NP деген әлсіз болжам бойынша, мәселе 21/22 = 0,95454-тен жақсы тұрақтымен жуықтауға болмайтыны белгілі. Әртүрлі авторлар MAX 2 SAT мысалдарын дәл шешу үшін нашар жағдай бойынша экспоненциалдық уақыт шектерін зерттеді.

Салмақты 2-қанағаттанушылық

Салмақты 2 қанағаттандыру мәселесінде (W2SAT) кіріс ретінде 2SAT мысалы мен k бүтін саны беріледі, ал мәселе – дәл k айнымалысының мәні шын болатын қанағаттандыратын тапсырманың бар-жоғын анықтау. Бұл W2SAT-тың барлық W[1] проблемалары үшін бұл орындалса ғана тұрақты параметрлік шешімге ие емес екенін білдіреді. Яғни, W2SAT үшін f(k)·n^(O(1)) түрінде жұмыс істейтін алгоритмнің табылуы екіталай. Тіпті одан да күшті, экспоненциалдық уақыт гипотезасы дұрыс болмаса, W2SAT n^(o(k)) уақытында шешілмейді.

Сандық Буль формулалары

2-қанағаттандыру үшін алғашқы полиномиалдық уақыт алгоритмін тапқаннан басқа, толыққанды квантталған Буль формулаларын бағалау мәселесін де қойды, онда квантталатын формула 2-CNF формуласы болып табылады. 2-қанағаттандыру мәселесі – бұл квантталған 2-CNF мәселесінің ерекше жағдайы, онда барлық кванторлар барлыққа қатысты. Krom сондай-ақ осы формулалар үшін тиімді шешім процедурасын жасады. Олар күшті байланысқан компоненттер және топологиялық реттеу техникасын кеңейту арқылы оны сызықтық уақытта шешуге болатынын көрсетті.