2-Удовлетворимость: Полиномиальная разрешимость и приложения

2-SAT: решение задач выполнимости булевых формул с двумя литералами в каждом дизъюнкте. Полиномиальный алгоритм, графы импликаций, 2CNF формулы.

20 мин чтения

100%

Источник: 2-satisfiability — Wikipedia

Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.

Содержание

Введение

Логическая задача, И попарных ИЛИ

В информатике, 2-удовлетворимость (2-SAT) – это вычислительная задача, заключающаяся в присвоении значений переменным, каждая из которых может принимать одно из двух возможных значений, с целью удовлетворения системы ограничений, наложенных на пары переменных. Это частный случай общей задачи булевой выполнимости (SAT), которая может включать ограничения на более чем две переменные, и задач удовлетворения ограничений, допускающих более двух вариантов для значения каждой переменной. Однако, в отличие от этих более общих задач, являющихся NP-полными, 2-удовлетворимость может быть решена за полиномиальное время. Экземпляры задачи 2-удовлетворимости обычно представляются в виде булевых формул специального типа, называемых конъюнктивной нормальной формой (2-КНФ) или формулами Крома. Альтернативно, они могут быть представлены в виде специального типа ориентированного графа – графа импликаций, который отображает переменные экземпляра и их отрицания в виде вершин графа, а ограничения на пары переменных – в виде ориентированных ребер. Оба этих типа входных данных могут быть решены за линейное время, либо методом, основанным на возврате (backtracking), либо с использованием сильно связных компонент графа импликаций. Метод резолюции, позволяющий объединять пары ограничений для получения дополнительных допустимых ограничений, также приводит к решению за полиномиальное время. Задачи 2-удовлетворимости представляют собой один из двух основных подклассов формул конъюнктивной нормальной формы, которые могут быть решены за полиномиальное время; другим подклассом является удовлетворимость Хорна. 2-удовлетворимость может применяться к задачам геометрии и визуализации, в которых набор объектов имеет два возможных положения, и требуется найти размещение для каждого объекта, избегающее перекрытий с другими объектами. Другие области применения включают кластеризацию данных для минимизации суммы диаметров кластеров, составление расписаний занятий и спортивных мероприятий, а также восстановление формы объекта по информации о его поперечных сечениях. В теории вычислительной сложности 2-удовлетворимость является примером NL-полной задачи, которую можно решить недетерминированно, используя логарифмический объем памяти, и которая относится к числу наиболее сложных задач, разрешимых при таких ограничениях по ресурсам. Множество всех решений экземпляра 2-удовлетворимости может быть представлено в виде структуры медианного графа, однако подсчет этих решений является #P-полным и, следовательно, не предполагает существования решения за полиномиальное время. Случайные экземпляры демонстрируют резкий фазовый переход от разрешимых к неразрешимым экземплярам при увеличении отношения ограничений к переменным сверх 1 – явление, предполагаемое, но не доказанное для более сложных форм задачи выполнимости. Вычислительно сложная вариация 2-удовлетворимости, заключающаяся в поиске такого назначения истинности, которое максимизирует количество удовлетворенных ограничений, имеет алгоритм аппроксимации, оптимальность которого зависит от гипотезы об уникальных играх, а другая сложная вариация, заключающаяся в поиске удовлетворяющего назначения, минимизирующего количество истинных переменных, является важным тестовым примером для параметризованной сложности.

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-удовлетворимости – это граф импликаций. Граф импликаций – это ориентированный граф, в котором для каждой переменной или ее отрицания существует одна вершина, и ребро соединяет одну вершину с другой, если соответствующие переменные связаны импликацией в импликативной нормальной форме экземпляра. Граф импликаций должен быть кососимметричным, то есть обладать симметрией, которая переводит каждую переменную в ее отрицание и меняет направление всех ребер.

Алгоритмы

Несколько алгоритмов известны для решения задачи 2-удовлетворимости. Самые эффективные из них выполняются за линейное время.

Ограниченное отслеживание

описать технику, включающую ограниченный возврат для решения задач поиска удовлетворения ограничений с бинарными переменными и попарными ограничениями. Они применяют эту технику к задаче составления расписания занятий, но также отмечают, что она применима и к другим задачам, включая 2-SAT. Основная идея их подхода заключается в построении частичного назначения истинности, переменная за переменной. Определенные шаги алгоритмов являются "точками выбора", точками, в которых переменной можно присвоить одно из двух различных значений истинности, и последующие шаги алгоритма могут привести к возврату к одной из этих точек выбора. Однако возврат возможен только к самому последнему сделанному выбору. Все предыдущие решения являются окончательными. Алгоритм на основе сильных компонент связности и алгоритм Косараджу выполняют один поиск в глубину. Алгоритм Косараджу выполняет два поиска в глубину, но он очень прост. В терминах графа импликаций два литерала принадлежат к одной и той же сильно связной компоненте, если существует цепочка импликаций от одного литерала к другому и обратно. Следовательно, в любом удовлетворяющем назначении для данного экземпляра 2-удовлетворимости, эти два литерала должны иметь одно и то же значение. В частности, если переменная и ее отрицание принадлежат к одной и той же сильно связной компоненте, экземпляр не может быть удовлетворен, поскольку невозможно присвоить обоим литералам одно и то же значение. Как показали Aspvall и др., это необходимое и достаточное условие: формула 2-CNF удовлетворяется тогда и только тогда, когда нет переменной, принадлежащей к той же сильно связной компоненте, что и ее отрицание. Для каждой компоненты в обратном топологическом порядке, если ее переменные еще не имеют назначений истинности, присвойте всем литералам в компоненте значение "истина". Это также приводит к присвоению значения "ложь" всем литералам в дополнительной компоненте. Благодаря обратному топологическому упорядочению и скошенной симметрии, когда литерал устанавливается в "истину", все литералы, достижимые из него по цепочке импликаций, уже будут установлены в "истину". Симметрично, когда литерал x устанавливается в "ложь", все литералы, ведущие к нему по цепочке импликаций, уже будут установлены в "ложь". Следовательно, присвоение истинности, построенное этой процедурой, удовлетворяет данной формуле, что завершает доказательство корректности необходимого и достаточного условия, установленного Aspvall и др. описать задачу маркировки карты, в которой каждая метка представляет собой прямоугольник, который можно разместить одним из трех способов относительно линии, которую он маркирует: он может иметь линию в качестве одной из своих сторон или быть центрированным на линии. Они представляют эти три положения с помощью двух двоичных переменных таким образом, что проверка существования допустимой маркировки снова сводится к задаче 2-удовлетворимости. использовать 2-удовлетворимость как часть алгоритма приближения для задачи поиска квадратных меток наибольшего возможного размера для заданного набора точек, с ограничением, что каждая метка имеет один из своих углов в точке, которую она маркирует. Чтобы найти маркировку заданного размера, они исключают квадраты, которые при удвоении перекрывали бы другую точку, и исключают точки, которые можно пометить таким образом, что они неизбежно перекрывали бы метку другой точки. Они показывают, что эти правила исключения приводят к тому, что для каждой оставшейся точки остается только два возможных положения метки, что позволяет найти допустимое размещение метки (если оно существует) как решение экземпляра 2-удовлетворимости. Поиск наибольшего размера метки, приводящего к разрешимому экземпляру 2-удовлетворимости, позволяет найти допустимое размещение меток, размер которых составляет не менее половины от оптимального решения. То есть, коэффициент приближения их алгоритма не превышает двух. Аналогично, если каждая метка прямоугольная и должна быть размещена таким образом, чтобы точка, которую она маркирует, находилась где-то на ее нижней границе, то использование 2-удовлетворимости для поиска наибольшего размера метки, для которого существует решение, в котором каждая метка имеет точку на нижнем углу, приводит к коэффициенту приближения не более двух. Аналогичные применения 2-удовлетворимости были сделаны для других геометрических задач размещения. В построении графов, если положения вершин фиксированы и каждое ребро должно быть нарисовано в виде круговой дуги с одним из двух возможных положений (например, в виде диаграммы дуг), то задача выбора, какую дугу использовать для каждого ребра, чтобы избежать пересечений, является задачей 2-удовлетворимости с переменной для каждого ребра и ограничением для каждой пары размещений, которые привели бы к пересечению. Однако в этом случае можно ускорить решение, по сравнению с алгоритмом, который строит и ищет явное представление графа импликаций, путем неявного поиска по графу. В проектировании интегральных схем (ВЛСИ), если набор модулей должен быть соединен проводами, каждый из которых может изгибаться не более одного раза, то снова существует два возможных маршрута для проводов, и задача выбора, какой из этих двух маршрутов использовать, чтобы все провода могли быть проложены в одном слое схемы, может быть решена как экземпляр 2-удовлетворимости. рассмотрим другую задачу проектирования ВЛСИ: вопрос о том, следует ли отражать каждый модуль в схеме. Это отражение не изменяет операций модуля, но изменяет порядок точек, в которых входные и выходные сигналы модуля подключаются к нему, что может повлиять на то, насколько хорошо модуль вписывается в остальную часть схемы. 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-удовлетворимости и использовать алгоритм 2-удовлетворимости, чтобы определить, может ли эта пара быть реализована кластеризацией. Для нахождения оптимальной суммы диаметров можно выполнить двоичный поиск, где каждый шаг представляет собой проверку осуществимости такого типа. Тот же подход также применим для поиска кластеризаций, оптимизирующих комбинации, отличные от суммы диаметров кластеров, и использующих произвольные меры несходства (вместо расстояний в метрическом пространстве) для измерения размера кластера. Временная сложность этого алгоритма определяется временем решения последовательности задач 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, имея в распоряжении только суммы значений в каждой строке и каждом столбце матрицы. Хотя существуют алгоритмы, работающие за полиномиальное время, для нахождения матрицы с заданными суммами строк и столбцов, решение может быть далеко не единственным: любая субматрица размером 2×2, являющаяся единичной матрицей, может быть инвертирована без изменения корректности решения. Поэтому исследователи искали ограничения на восстанавливаемую форму, которые можно использовать для сужения пространства решений. Например, можно предположить, что форма связна; однако проверка существования связного решения является NP-полной задачей. Ещё более ограниченный и простой в решении вариант заключается в том, что форма ортогонально выпукла: содержит единственный непрерывный блок квадратов в каждой строке и каждом столбце. Улучшив несколько предыдущих решений, авторы показали, как эффективно восстанавливать связные ортогонально выпуклые формы, используя 2-SAT. Идея их решения состоит в том, чтобы угадать индексы строк, содержащих самые левые и самые правые ячейки восстанавливаемой формы, а затем сформулировать задачу выполнимости 2-SAT, которая проверяет, существует ли форма, соответствующая этим предположениям и заданным суммам строк и столбцов. Они используют четыре переменные выполнимости 2-SAT для каждого квадрата, который может быть частью заданной формы, одну для указания принадлежности к каждой из четырёх возможных «угловых областей» формы, и используют ограничения, которые обеспечивают непересечение этих областей, задают желаемую форму, формируют общую форму с непрерывными строками и столбцами и обеспечивают желаемые суммы строк и столбцов. Время работы их алгоритма составляет O(m³n), где m — наименьшее из двух измерений входной формы, а n — наибольшее из двух измерений. Позднее тот же метод был расширен на ортогонально выпуклые формы, которые могут быть соединены только по диагонали, без требования ортогональной связности. В качестве части решателя полных головоломок нонограмм, авторы использовали 2-SAT для объединения информации, полученной из нескольких других эвристик. При наличии частичного решения головоломки они используют динамическое программирование в каждой строке или столбце, чтобы определить, заставляют ли ограничения этой строки или столбца какие-либо из её квадратов быть белыми или чёрными, и могут ли любые два квадрата в одной строке или столбце быть связаны отношением импликации. Они также преобразуют нонограмму в задачу цифровой томографии, заменяя последовательность длин блоков в каждой строке и столбце её суммой, и используют формулировку задачи о максимальном потоке, чтобы определить, содержит ли эта задача цифровой томографии, объединяющая все строки и столбцы, какие-либо квадраты, состояние которых можно определить, или пары квадратов, которые могут быть связаны отношением импликации. Если какая-либо из этих двух эвристик определяет значение одного из квадратов, он включается в частичное решение, и те же вычисления повторяются. Однако, если обе эвристики не могут установить значение ни одного квадрата, выводы, полученные обеими, объединяются в задачу выполнимости 2-SAT, и решатель 2-SAT используется для поиска квадратов, значение которых фиксировано задачей, после чего процедура повторяется. Эта процедура может или не может привести к нахождению решения, но гарантированно выполняется за полиномиальное время. Batenburg и Kosters сообщают, что, хотя большинство головоломок в газетах не требуют всей её мощности, как эта процедура, так и более мощная, но медленная процедура, которая сочетает в себе этот подход 2-SAT с ограниченным перебором с возвратом,

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. Если такая цепочка найдена, то экземпляр не может быть выполнимым. По теореме Иммермана — Селепчени также возможно в недетерминированном логарифмическом пространстве проверить выполнимость выполнимого экземпляра 2-удовлетворимости. 2-удовлетворимость является NL-полной, что означает, что это одна из "самых трудных" или "наиболее выразительных" задач в классе сложности NL задач, разрешимых недетерминированно в логарифмическом пространстве. Полнота в данном случае означает, что детерминированная машина Тьюринга, использующая лишь логарифмическое пространство, может преобразовать любую другую задачу из NL в эквивалентную задачу 2-удовлетворимости. Аналогично схожим результатам для более известного класса сложности NP, это преобразование вместе с теоремой Иммермана — Селепчени позволяет представить любую задачу из NL в виде формулы логики второго порядка с единственным экзистенциально квантифицированным предикатом, при этом ограничения на длину клауз ограничены значением 2. Такие формулы известны как SO Krom. Аналогично, импликативная нормальная форма может быть выражена в логике первого порядка с добавлением оператора для транзитивного замыкания. В работе [укажите ссылку на работу] описан алгоритм для эффективного перечисления всех решений для заданного экземпляра 2-удовлетворимости и для решения нескольких связанных задач. Также существуют алгоритмы для поиска двух выполнимых назначений, имеющих максимальное расстояние Хэмминга друг от друга.

Подсчитывает количество удовлетворительных заданий

#2SAT — это задача о подсчете количества выполнимых наборов значений для заданной формулы 2CNF. Эта задача подсчета является #P-полной, что означает, что она не может быть решена за полиномиальное время, если P = NP. Более того, не существует полностью полиномиальной рандомизированной схемы аппроксимации для #2SAT, если NP = RP, и это справедливо даже при ограничении входных данных монотонными формулами 2CNF, то есть формулами 2CNF, в которых каждый литераль является положительным вхождением переменной. Самый быстрый известный алгоритм для вычисления точного количества выполнимых наборов значений для формулы 2SAT работает за время .

Случайные случаи удовлетворенности двумя параметрами

Можно сформировать случайный экземпляр задачи 2-удовлетворимости для заданного числа n переменных и m дизъюнктов, выбирая каждый дизъюнкт равномерно случайным образом из множества всех возможных дизъюнктов из двух переменных. Когда m мало по отношению к n, такой экземпляр, вероятно, будет выполним, но при больших значениях m вероятность выполнимости уменьшается. Более точно, если отношение m/n фиксировано как константа α ≠ 1, вероятность выполнимости стремится к пределу при n, стремящемся к бесконечности: если α < 1, то предел равен единице, а если α > 1, то предел равен нулю. Таким образом, задача демонстрирует фазовый переход при α = 1.

Максимальная удовлетворительность

В задаче максимальной выполнимости 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-удовлетворимости (W2SAT) на вход подается экземпляр 2-SAT с переменными и целое число k, и требуется определить, существует ли такое удовлетворяющее присваивание, в котором ровно k переменных истинны. Это подразумевает, что W2SAT не является разрешимой задачей с фиксированными параметрами, если это не верно для всех задач в W[1]. Иными словами, маловероятно существование алгоритма для W2SAT, время работы которого имеет вид f(k)·n^(O(1)). Более того, W2SAT не может быть решена за время n^(o(k)), если только гипотеза об экспоненциальном времени не окажется ложной.

Количественные булевы формулы

Помимо разработки первого алгоритма полиномиального времени для задачи 2-удовлетворимости, была сформулирована задача оценки полностью квантифицированных булевых формул, в которых квантифицируемой формулой является формула 2-КНФ. Задача 2-удовлетворимости является частным случаем этой квантифицированной задачи 2-КНФ, в котором все кванторы являются экзистенциальными. Krom также разработал эффективную процедуру решения для этих формул. Было показано, что её можно решить за линейное время, используя расширение их метода сильно связных компонент и топологической сортировки.