2-SAT (2-выполнимость)

2-Выполнимость (2-SAT)

   Рассмотрим булеву формулу в конъюнктивной нормальной форме, где каждый конъюнкт содержит в точности 2 дизъюнкта (2-КНФ). Например, формула

Ф(x₁, x₂, x₃, x₄, x₅) = (x₁ ν x₂) Λ (!x₂ ν x₃) Λ (!x₁ ν !x₂) Λ (x₃ ν x₄) Λ (!x₃ ν x₅)Λ (!x₄ ν !x₅) Λ (!x₃ ν x₄)

содержит 5 переменных и 7 конъюнктов.

   Задача 2-выполнимости состоит в том, чтобы присвоить переменным значения (0или 1) таким образом, чтобы формула была истинной. То есть ответить на вопрос: существует ли такой набор переменных, на котором формула принимает истинное значение?

   Задача 2-выполнимости решается за полиномиальное время.

   Приведём задачу к импликативной форме. Выражение вида a ν b эквивалентно !a  b или !b  a. Действительно, если необходимо добиться обращения выражения a b в true, то если a = false, то необходимо b = true, и наоборот, если b = false, то необходимо a = true.

   Построим теперь граф импликаций: для каждой переменной в графе будет по две вершины, обозначим их через x_i и !x_i. Рёбра в графе будут соответствовать импликативным связям.

   Если булева формула имеет n переменных и m конъюнктов, то соответствующий граф импликаций будет содержать 2n вершин и 2m ребер.

   Пример. Для 2-CNF формы Ф(a, b, c) =  (a ν b) Λ (b ν !c) граф импликаций будет содержать следующие рёбра (ориентированные): !a  b, !b  a, !b  !c, c  b. То есть для каждой импликации x  y в графе строится ориентированное ребро (x, y).

   Перенумеруем переменные и их отрицания, начиная с нуля. Переменным a и !aпоставим в соответствие вершины 0 и 1, переменным b и !b – вершины 2 и 3, переменным c и !c – вершины 4 и 5. Тогда вершины i и i XOR 1 будут соответствовать переменной и ее отрицанию.

   Булева формула Ф содержит 3 переменные (a, b, c) и 2 конъюнкта. Граф импликаций состоит из 6 вершин и 4 ребер. Свойство графа импликаций состоит в том, что с каждой импликацией x  y должна присутствовать и импликация !y !x.

   Теорема. Булева формула Ф в 2-КНФ является невыполнимой тогда и только тогда, когда существует такая переменная x, что в графе импликаций существуют пути от xдо !x и от !x до x. Существование таких путей эквивалентно тому, что x  !x и !x  x.

   Пример. Отобразим граф импликаций для формулы

Ф(x₁, x₂, x₃, x₄, x₅) = (x₁ v x₂) Λ (!x₂ v x₃) Λ (!x₁ v !x₂) Λ (x₃ v x₄) Λ (!x₃ v x₅)Λ (!x₄ v !x₅) Λ (!x₃ v x₄)

   Теорема. Булева формула Ф в 2-КНФ является невыполнимой тогда и только тогда, когда существует сильно связная компонента, содержащая одновременно некоторую переменную x и ее дополнение !x.

   Этот критерий выполнимости можно проверить за время O(n+m) с помощью алгоритма поиска сильно связных компонент.

   Рассмотрим алгоритм нахождения решения задачи 2-SAT в предположении, что решение существует.

   Несмотря на то, что решение существует, для некоторых переменных может выполняться, что из x достижимо !x, или (но не одновременно) из !x достижимо x. В таком случае выбор одного из значений переменной x будет приводить к противоречию, в то время как выбор другого не будет. Поэтому следует выбрать для xто из двух значений, которое не приведет к противоречию.

   Теорема. Пусть Color[v] обозначает номер (цвет) компоненты сильной связности, которой принадлежит вершина v. Известно, что номера вершин упорядочены в порядке топологической сортировки. Если в графе существует путь из v в w, тоColor[v] ≤ Color[w]. Тогда если Color[x] < Color[!x], то значение !x считаем истинным (то есть x будет ложно), иначе при Color[x] > Color[!x] истинным считаем x.

   Доказательство.

   а) Докажем, что если Color[x] > Color[!x], то из x не достижимо !x. Действительно, так как номер компоненты сильной связности Color[x] больше номера компонентыColor[!x], то это означает, что компонента связности, содержащая x, расположена левее компоненты связности, содержащей !x, и из первой никак не может быть достижима последняя.

   б) Докажем, что никакая вершина y, достижимая из x, не является "плохой", то есть неверно, что из y достижимо !y. Проведем доказательство от противного. Пусть из xдостижимо y, а из y достижимо !y. Поскольку из x достижимо y, то, по свойству графа импликаций, из !y будет достижимо !x. Но, по предположению, из y достижимо !y. Тогда мы получаем, что из x достижимо !x, что противоречит условию. Что и требовалось доказать.

Алгоритм решения задачи 2-выполнимости

1. Построим граф импликаций.
2. Найдём в этом графе компоненты сильной связности за время O(n+m), пустьColor[v] – это номер компоненты сильной связности, которой принадлежит вершина v.
3. Проверим, что для каждой переменной x вершины x и !x лежат в разных компонентах, то есть Color[x] ≠ Color[!x]. Если это условие не выполняется, то решения не существует.
4. Если Color[x] > Color[!x], то переменной x выбираем значение true, иначеfalse.

   Вход. Первая строка содержит количество переменных n в 2-КНФ и количество конъюнктов m. Переменные нумеруются числами от 1 до n. Если переменная x имеет номер i (1 ≤ i ≤ n), то ее отрицание (!x) будем задавать числом -i. Каждая из следующих m строк описывает один конъюнкт: она содержит номера переменных, входящих в него.

   Выход. Если задача 2-выполнимости решения не имеет, то вывести "NO SOLUTION". Иначе в одной строке следует вывести последовательность из n нулей и единиц. i-ое число последовательности задает значение, которое должна принимать переменная с номером i.

   Пояснение. В примере задается формула Ф(a, b, c) =  (a v b) Λ (b v !c). Переменные a, b, c имеют соответственно номера 1, 2, 3. Отрицание !c кодируется числом -3.

   Для хранения графа импликаций и обратного к нему графа используем вектора g иgr. Объявим рабочие массивы: Color[i] содержит номер компоненты сильной связности, в которую входит вершина i, Answer содержит результирующий набор из nнулей и единиц.

vector > g, gr;

vector used, list, Color, Answer;

   Первый поиск в глубину. Заносим вершины графа импликаций в массив list в порядке завершения их обработки.

void dfs1(int v)

{

  int i, to;

  used[v] = 1;

  for(i = 0; i < g[v].size(); i++)

  {

    to = g[v][i];

    if (!used[to]) dfs1(to);

  }

  list.push_back(v);

}

   Обход в глубину на транспонированном графе. Красим текущую вершину v цветомc. Одинаковый цвет имеют вершины, которые входят в одну компоненту сильной связности. Одновременно массив Color используется для отмечания уже пройденных вершин во время второго обхода в глубину (перед запуском процедуры dfs2 массивColor следует обнулить).

void dfs2(int v, int c)

{

  int i, to;

  Color[v] = c;

  for(i = 0; i < gr[v].size(); i++)

  {

    to = gr[v][i];

    if (Color[to] == -1) dfs2(to,c);

  }

}

   Поскольку переменные нумеруются с единицы, а вершины графа импликаций с нуля, то для удобства следует перенумеровать переменные и их отрицания. Переменной с номером i поставим в соответствие вершину графа 2*i–2. Если отрицание переменной задавалось числом i, то ей поставим в соответствие вершину 2*(- i)–1. Например, если переменная a имела номер 1, а ее отрицание !a кодировалось -1, то в графе переменной a будет соответствовать вершина 2*1–2 = 0, а ее отрицанию – вершина 2*1–1 = 1. Отметим, что нумерация вершин графа такова, что переменной и ее отрицанию всегда соответствуют вершины i и i XOR 1.

int Conv(int v)

{

  if (v >= 0) return 2 * v - 2;

  return 2 * (-v) - 1;

}

   Основная часть программы. Читаем входную формулу. Поскольку формула содержитn переменных, то в графе импликаций будет 2n вершин, пронумерованных от 0 до 2n–1 .

  scanf("%d %d",&n,&m);

  g.assign(2*n,0);gr.assign(2*n,0);

  for(i = 0; i < m; i++)

  {

   Читаем номера переменных, входящих в конъюнкт. С помощью функции Convнаходим номера вершин графа импликаций, которые будут им соответствовать.

    scanf("%d %d",&a,&b);

    a = Conv(a); b = Conv(b);

   Переводим каждый конъюнкт a Ú b в импликативную форму !a É b. С каждой импликацией !a É b заносим в граф два ребра: (!a, b) и (!b, a). Одновременно строим транспонированный граф gr.

    g[a^1].push_back(b);   g[b^1].push_back(a);

    gr[b].push_back(a^1);  gr[a].push_back(b^1);

  }

   Запускаем первый обход в глубину, в котором строим массив list.

  used.assign(2*n,0);

  for(i = 0; i < 2*n; i++)

    if (!used[i]) dfs1(i);

   Запускаем второй обход в глубину, в котором раскрашиваем вершины графа цветомс. Вершины, входящие в одну сильно связную компоненту, имеют одинаковый цвет.

  Color.assign(2*n,-1);

  for(i = 0, c = 0; i < 2*n; i++)

  {

    v = list[2*n-i-1];

    if (Color[v] == -1) dfs2(v,c++);

  }

   Поиск сильно связных компонент завершен. Если для некоторой переменной она и ее отрицание (вершины i и i XOR 1) имеют одинаковый цвет, то входная формула невыполнима.

  for (i = 0; i < 2*n; i += 2)

    if (Color[i] == Color[i^1])

    {

      printf("NO SOLUTION");

      return 0;

    }

   Если задача имеет решение, то присвоим переменным, входящим в формулу, значения (0 или 1). Если Color[x] > Color[!x], то переменной x выбираем значение 1, иначе 0.

  Answer.assign(n,0);

   Четным вершинам графа соответствуют переменные, а нечетным – их отрицания. Четной вершине i соответствует переменная с номером .

  for (i = 0; i < 2*n; i += 2)

    Answer[i/2] = (Color[i] > Color[i^1]);

   Выводим решение для задачи 2-выполнимости.

  for (i = 0; i < n; i++)

   printf("%d ",Answer[i]);

  printf("\n");

   Отобразим решение для указанного в задаче примера.

   Проверим утверждение, что если в графе есть путь из v в w, то Color[v] ≤ Color[w].

   Для ребра (3, 0): 1 = Color[3] < Color[0] = 5.      Для ребра (1, 2): 3 = Color[1] <Color[2] = 4.

   Для ребра (4, 2): 0 = Color[4] < Color[2] = 4.     Для ребра (3, 5): 1 = Color[3] <Color[5] = 2.

   Все вершины графа будут покрашены разными цветами, поэтому задача 2-выполнимости для формулы (a v b) Λ (b v !c) разрешима. Выбираем значения для переменных:

• 5 = Color[0] > Color[1] = 3, переменной a выбираем значение 1,
• 4 = Color[2] > Color[3] = 1, переменной b выбираем значение 1,
• 0 = Color[4] < Color[5] = 2, переменной c выбираем значение 0

   Пример. Рассмотрим задачу 2-выполнимости для формулы

Ф(a, b, c, d) =  (a v c) Λ (b v !c) Λ (!b v d) Λ (c v !d) Λ (!a v !d)

   Построим ребра графа:

• a v c эквивалентно !a  c, строим ребра (!a, c) и (!c, a).
• b v !c эквивалентно !b  !c, строим ребра (!b, !c) и (c, b).
• !b v d эквивалентно b  d, строим ребра (b, d) и (!d, !b).
• c v !d эквивалентно !c  !d, строим ребра (!c, !d) и (d, c).
• !a v !d эквивалентно a  !d, строим ребра (a, !d) и (d, !a).

   Граф импликаций имеет две сильно связные компоненты (вершины покрашены цветами 0 и 1). Задача 2-выполнимости имеет решение:

• 1 = Color[0] > Color[1] = 0, переменной a выбираем значение 1,
• 0 = Color[2] < Color[3] = 1, переменной b выбираем значение 0,
• 0 = Color[4] < Color[5] = 1, переменной c выбираем значение 0,
• 0 = Color[6] < Color[7] = 1, переменной d выбираем значение 0.

Литература и источники:

1. ...