7535. Выполнимость снова!

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

Вход. Первая строка содержит количество тестов, не большее 5. Первая строка каждого теста содержит два числа n (1 ≤ n ≤ 20) и m (1 ≤ m ≤ 100), где n – количество переменных, а m – количество правил. Каждая из следующих m строк задает одно правило. Каждое правило представляет собой дизъюнкцию литералов вида Xi или ~Xi для некоторого i (1 ≤ i ≤ n), где ~Xi обозначает отрицание литерала Xi. Оператор "or" обозначается символом v и отделяется от литералов одним пробелом.

Выход. Для каждого теста вывести в отдельной строке satisfiable если формула выполняемая и unsatisfiable иначе.

Пример входа	Пример выхода
2 3 3 X1 v X2 ~X1 ~X2 v X3 3 5 X1 v X2 v X3 X1 v ~X2 X2 v ~X3 X3 v ~X1 ~X1 v ~X2 v ~X3	satisfiable unsatisfiable

РЕШЕНИЕ

перебор

Анализ алгоритма

Количество литералов в формулах не более 20. Переберем все возможные значения Xi, которые могут принимать значения 0 или 1. Если для некоторого набора (X1, X2, …, Xn) все формулы будут выполнимы (принимать значение 1), то следует вывести satisfiable. Если выполнимого набора не существует, то выводим unsatisfiable.

Преобразуем множество правил в структуру, удобную для дальнейшей обработки. Заведем вектор v длины m, j-ый элемент которого будет вектором, содержащим набор переменных, входящих в j-ое правило. Если переменная Xi входит в правило с отрицанием, то в вектор занесем значение -i.

Например, для второго теста такая структура будет иметь вид:

Реализация алгоритма

Набор правил для каждого теста храним в массиве v.

vector<vector<int> > v;

Читаем входные данные.

scanf("%d",&tests);

while(tests--)

{

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

v.clear(); v.resize(m);

Читаем правила и преобразовываем их в удобный для дальнейшей обработки формат.

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

{

scanf("%c",&ch);

while(1)

{

if (ch == '~')

{

scanf("X%d",&val);

val = -val;

}

else

scanf("%d",&val);

v[i].push_back(val);

Читаем символ за переменной. Если это конец строки (ch = ‘\n’), то завершаем обработку текущего правила.

scanf("%c",&ch);

if(ch == '\n') break;

Читаем символ v, пробел и следующий символ (который равен ‘~’ или ‘X’).

scanf("%c%c%c",&ch,&ch,&ch);

}

}

Генерируем все кортежи (X1, X2, …, Xn) из нулей и единиц длины n. Кортежем является двоичный код числа i.

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

{

Проверяем выполнимость правил на кортеже, который задается двоичным кодом числа i.

sat = 1;

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

{

Проверяем выполнимость k-го правила.

s = 0;

for(j = 0; j < v[k].size(); j++)

{

p = v[k][j];

Правило содержит переменную X_|p|. Если p < 0, то переменная X_|p| входит в k-ое правило с отрицанием. В переменной bit вычисляем ее значение на текущем кортеже.

bit = (i & (1 << (abs(p) - 1))) > 0;

if (p < 0) bit = 1 - bit;

s |= bit;

}

Если текущее правило не выполнимо (s = 0), то проверяем следующий кортеж.

sat &= s;

if (!sat) break;

}

sat = 1, если все правила выполнимы. Завершаем перебор, нет смысла его продолжать дальше.

if (sat) break;

}

В зависимости от значения sat выводим ответ.

if (sat) puts("satisfiable");

else puts("unsatisfiable");

}